RSCOSStructural004Cert
plain-language theorem explainer
Packages three structural side-conditions for the RS gap-45 cosmology certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Cosmology and ladder auditors cite it as the interface that the concrete certificate must inhabit. It is a pure structure (no proof body); inhabitance is discharged by the sibling certificate constructor.
Claim. A certificate for RS structural cosmology module 4 consists of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(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
Module RS_COS_Structural_004 is the structural half of the RS gap-45 story: at spatial dimension $D=3$ one has $D^2(D+2)=9\cdot 5=45$, read as the minimum rung for stable self-reference. Status is structural theorem (zero sorry, zero axiom).
Domain cost is the local cost functional on pairs of positive reals (mass-like and energy-like arguments) used in this cosmology layer; the diagonal identity says matched arguments carry zero cost. The canonical threshold is the positive cutoff against which that cost is compared when certifying the gap-45 bound.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The present structure lifts that style of positivity and diagonal vanishing into the cosmology certificate interface.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity of domain cost on the positive orthant, positivity of the canonical threshold). Inhabitation is supplied separately by the sibling definition cert, which wires in domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and by cert_inhabited, which packages that witness as Nonempty.
why it matters
This structure is the typed contract for RS cosmology structural module 4. Downstream, cert builds an explicit inhabitant and cert_inhabited records that the type is nonempty, closing the structural half of the gap-45 claim (minimum rung for stable self-reference at $D=3$).
In the broader Recognition chain this sits under the $D=3$ forcing (T8) and the eight-tick / rung arithmetic that produces gap 45 as $D^2(D+2)$. It does not itself compute masses or run the phi-ladder; it only freezes the cost and threshold side-conditions those later steps rely on. Parent consumers are the local certificate constructor and the nonempty witness in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.