RSGRVStructural009Cert
plain-language theorem explainer
Packages three structural side-conditions used by Gravity RS module 9: the domain cost vanishes on the diagonal, is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Gravity and RS-forcing readers cite it as the typed witness that those inequalities are available. It is a pure structure declaration; inhabitants are built by filling the three fields from sibling lemmas.
Claim. A certificate is a triple of facts: (i) for every real $r \neq 0$, the domain cost satisfies $\mathrm{domainCost}(r,r)=0$; (ii) for all $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Gravity RS Structural Module 9 sits on the RS forcing chain after T5 (J-uniqueness), T6 ($\varphi$ forced), T7 (eight-tick octave), and T8 ($D=3$). The module is marked structural: zero sorry, zero axioms.
The domain cost is the local cost functional on mass/energy-type reals used in this gravity layer; its diagonal vanishing and nonnegativity mirror the global recognition cost. Upstream, cost_nonneg in ObserverForcing states that every recognition event has nonnegative cost, via nonnegativity of the J-cost on positive states. The canonical threshold is the positive cutoff against which that cost is compared in the structural claims of the module.
proof idea
No proof body: this is a structure with three propositional fields. Inhabitation is deferred to the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields, and to cert_inhabited, which wraps that witness as Nonempty.
why it matters
Gives a single named type for the three inequalities the rest of RS_GRV_Structural_009 needs, so downstream code can depend on one certificate rather than three free-floating lemmas. Immediate consumers are cert (the concrete inhabitant) and cert_inhabited (nonemptiness). In the broader framework it records that the gravity-layer cost still obeys the J-cost minimum-at-identity and nonnegativity pattern forced at T5, with a positive threshold available for structural comparisons. It does not itself advance a new forcing step; it freezes the local hypotheses those steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.