StringLengthCert
plain-language theorem explainer
Certificate structure bundling three analytic conditions on the domain cost and the canonical compactification threshold for the φ-ladder string-length derivation. Anyone citing the inhabited certificate for R_comp = ℓ_Pl φ^{-k} references this bundle. Pure structure definition: no proof body; fields are discharged by sibling lemmas on vanishing, nonnegativity, and positivity.
Claim. A string-length certificate is a triple of properties: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical compactification threshold is strictly positive.
background
The module derives the string compactification radius from the Recognition Science φ-ladder: $R_{\mathrm{comp}}=\ell_{\mathrm{Pl}},\varphi^{-k}$. Planck-scale compactification is the $k=0$ rung; electroweak-scale radii sit near $k\approx\log(M_{\mathrm{Pl}}/M_{\mathrm{EW}})/\log\varphi\approx 106$.
The domain cost $C(m,e)$ is the local mismatch functional between a mass-like and an energy-like scale on that ladder. It is required to vanish when the two arguments coincide and to stay nonnegative for positive inputs, mirroring the global J-cost nonnegativity of recognition events. The canonical threshold is the positive cutoff that normalizes the length formula.
Upstream, ObserverForcing records that every recognition-event cost is nonnegative because $J$ itself is nonnegative on the positive reals.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is supplied downstream by wiring the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into the three slots. The structure itself only names the interface.
why it matters
Gives the typed interface that cert and cert_inhabited discharge, closing the structural theorem for string length from the φ-ladder (module status: 0 sorry, 0 axiom). Downstream cert is the concrete witness; cert_inhabited packages Nonempty for later physics lemmas that need a certificate in hand.
In the broader framework this sits on the φ-ladder mass/length bookkeeping (T6 forces φ as the self-similar fixed point; the mass formula uses yardstick × φ^{rung-8+gap(Z)}). The certificate isolates exactly the cost and threshold positivity needed before one may quote $R_{\mathrm{comp}}=\ell_{\mathrm{Pl}}\varphi^{-k}$ as a derived length rather than an ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.