cert
plain-language theorem explainer
Packages three domain-cost facts into one certificate: the cost vanishes on the diagonal, is nonnegative for positive measured/expected values, and the canonical threshold is positive. Cited by anyone assembling the φ-ladder compactification-radius story. The body is a structure instance that wires three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats string compactification radii forced by the Recognition Science φ-ladder: extra dimensions sit at $R_{\mathrm{comp}}=\ell_{\mathrm{Pl}}\cdot\varphi^{-k}$. Near the Planck scale one takes $k=0$; the electroweak scale needs roughly $k\approx\log(M_{\mathrm{Pl}}/M_{\mathrm{EW}})/\log\varphi\approx 106$ rungs. Status is structural (zero sorry, zero axiom).
The certificate structure packages three properties of a domain cost functional on pairs of positive reals (measured vs expected scale). Diagonal vanishing says equal scales cost nothing; nonnegativity is the usual J-cost lower bound; the canonical threshold is a positive cutoff used to decide when a compactification radius is recognized.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: any event cost is $\ge 0$ because it is an instance of the J-cost, which is nonnegative for positive arguments.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed here.
why it matters
Gives a single named inhabitant of the string-length certificate so downstream physics lemmas can assume the cost package without re-proving the three facts. It sits inside the structural theorem that compactification radii are φ-ladder rungs ($R_{\mathrm{comp}}=\ell_{\mathrm{Pl}}\varphi^{-k}$), tying the cost language of Recognition Science (J-cost nonnegativity, identity at $x=1$) to the string-scale story. No used-by edges are recorded yet; the sibling cert_inhabited is the natural consumer. Framework landmarks in play are the φ fixed point (T6) and the mass/length ladder built from it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.