cert_inhabited
plain-language theorem explainer
The string-length certificate type is inhabited: there is a concrete witness that domain cost vanishes on the diagonal, stays nonnegative for positive masses and energies, and that the canonical threshold is positive. Anyone assembling the φ-ladder compactification radius package cites this existence fact. The proof is a one-line term that packages the already-built certificate instance.
Claim. The type of string-length certificates is nonempty: there exists a witness $C$ such that (i) the domain cost satisfies $\mathrm{cost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
The module fixes extra-dimension compactification radii on the φ-ladder: $R_{\mathrm{comp}}=\ell_{\mathrm{Pl}},\varphi^{-k}$. Planck-scale compactification is $k=0$; 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).
A string-length certificate packages three elementary cost facts used downstream of that ladder: the domain cost vanishes when mass equals energy (diagonal identity), is nonnegative for positive arguments, and the canonical threshold used to cut the ladder is positive. Domain cost itself is the local cost functional on mass/energy pairs imported from the Cost layer; the threshold is the module's fixed positive cutoff.
proof idea
One-line term proof. The module already constructs a concrete certificate instance cert whose three fields discharge the structure obligations. The theorem simply wraps that instance in the Nonempty constructor, so existence follows by exhibition rather than by any further algebraic work.
why it matters
Closes the existence side of the structural string-length package in the φ-ladder compactification story (Plan v7). Without an inhabited certificate, later physics lemmas cannot assume the cost diagonal, nonnegativity, and positive threshold as a single bundled hypothesis. No downstream consumers are wired yet in the graph; the declaration is the terminal existence stamp for this module. It sits under the broader Recognition ladder (φ forced at T6, eight-tick and $D=3$ at T7–T8) only as infrastructure for the compactification-radius claim, not as a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.