RSForcingChain001Cert
plain-language theorem explainer
A certificate structure packaging three elementary cost axioms for Foundation Module 1 of the RS forcing chain: diagonal vanishing of the domain cost, non-negativity for positive arguments, and positivity of the canonical threshold. Downstream code cites it to inhabit the module certificate and prove Nonempty. The declaration is pure data; no proof lives here.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{cost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Foundation Module 1 sits at the base of the RS recognition lattice. All physical predictions in the monolith are meant to derive from the unique cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$), with zero sorry and zero axioms in this layer.
The domain cost is the real-valued cost assigned to a pair of positive scale parameters (measure and expectation). Diagonal vanishing says matched scales incur zero cost; non-negativity is the elementary positivity of $J$ away from the identity. The canonical threshold is the positive cutoff used later to separate trivial from nontrivial recognition events.
Upstream, ObserverForcing already records that every recognition event has non-negative cost via Jcost_nonneg at positive state. This structure re-packages the corresponding domain-level statements plus threshold positivity as a single inhabitability witness for the module.
proof idea
No proof body: the declaration is a structure (record type) with three propositional fields. Inhabitation is deferred to the sibling definition cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then wraps that value as Nonempty.
why it matters
Module 1 is the structural entry point of the RS forcing chain: it freezes the cost axioms that later steps (T5 J-uniqueness, T6 $\varphi$ fixed point, T7 eight-tick octave, T8 $D=3$) build on. Packaging the three facts as a named certificate lets the module export a single Nonempty witness (cert_inhabited) rather than three loose lemmas.
Parents in this file are exactly cert and cert_inhabited. The module header claims STRUCTURAL THEOREM status (0 sorry, 0 axiom); this structure is the type those claims inhabit. It does not itself force $J$ or $\varphi$; it only records the cost-floor and threshold positivity that any such forcing must respect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.