cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single certificate for RS forcing-chain module 11 (phi-rung spacing). Anyone citing the structural status of consecutive rungs separated by factor φ uses this bundle. The definition is a pure structure inhabitant: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; and (iii) the canonical threshold is strictly positive.
background
Module 11 of the RS forcing chain treats rung spacing on the φ-ladder: consecutive recognition rungs are separated by the golden ratio φ ≈ 1.618. The module is marked structural (zero sorry, zero axiom).
The certificate structure demands three properties of a domain cost functional and a threshold constant. Domain cost is the local cost comparing a mass-like and an energy-like coordinate; it is required to vanish when the two arguments coincide (off zero) and to stay nonnegative in the positive orthant. The canonical threshold is the positive cutoff used to separate on-rung from off-rung configurations.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via the J-cost minimum: "The cost of any recognition event is non-negative," proved from Jcost_nonneg at positive state.
proof idea
One-line structure inhabitant. Each field of RSForcingChain011Cert is filled by the corresponding sibling lemma already proved in this module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No further tactic work.
why it matters
Gives the module a single named certificate object that asserts the cost and threshold hygiene needed for φ-rung spacing. In the broader forcing chain this sits under the T6 landmark (φ forced as the self-similar fixed point) and supports the mass-ladder yardstick picture where consecutive rungs differ by factor φ. No downstream consumers are recorded yet; the sibling cert_inhabited is the natural next wrapper. The declaration itself is pure packaging, not a new physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.