RSForcingChain004Cert
plain-language theorem explainer
Certificate bundle for Foundation module 4: the domain cost vanishes on the diagonal (equal nonzero arguments), stays nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Downstream code cites it to inhabit the module certificate and lock the J-cost minimum at equilibrium ratio 1. The structure is pure data; witnesses are supplied by sibling lemmas.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost at equal arguments satisfies $C(r,r)=0$; (ii) for all positive $m,e>0$, $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module 4 of the RS forcing chain records the J-cost minimum: equilibrium at ratio 1 with $J(1)=0$, and the golden-ratio evaluation $J(\varphi)=\varphi-3/2$. Status is structural (no sorry, no axioms).
The domain cost $C(m,e)$ is the module-local cost on positive mass/energy-style arguments; on the diagonal it encodes the recognition equilibrium. The canonical threshold is the positive cutoff used later in the chain. Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states.
This structure packages exactly those three Prop fields so a single inhabited certificate can be passed downstream without re-proving the arithmetic each time.
proof idea
No proof body: this is a structure declaration (three fields, no constructors beyond the record). Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas do the real work (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the threshold).
why it matters
Gives Module 4 a single named certificate type for the J-cost minimum and threshold positivity, matching the module claim that equilibrium sits at ratio 1 with $J(1)=0$. Downstream, cert builds a concrete value and cert_inhabited proves Nonempty of the certificate, so later forcing-chain steps can assume the package rather than three separate lemmas.
In the broader RS chain this is the structural bookkeeping around T5 (unique $J(x)=(x+x^{-1})/2-1$, minimum at $x=1$) before phi-forcing and the eight-tick octave. It does not itself force $\varphi$ or dimension; it only certifies the cost-floor facts this module owns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.