cert_inhabited
plain-language theorem explainer
The module-4 forcing-chain certificate is inhabited: a single witness packs vanishing of domain cost on equal nonzero ratios, nonnegativity of domain cost on positive arguments, and positivity of the canonical threshold. Anyone assembling the structural RS forcing chain cites this to discharge Nonempty. Proof is a one-line term introducing the packaged cert witness.
Claim. The type of certificates packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) positivity of the canonical threshold, is nonempty.
background
Foundation RS Module 4 records the J-cost minimum: $J(1)=0$ at ratio one (equilibrium), and $J(\varphi)=\varphi-3/2$ at the golden ratio. Status is structural theorem (zero sorry, zero axiom).
The certificate structure bundles three facts about the local domain cost functional: cost vanishes when the two arguments are equal and nonzero; cost is nonnegative on positive measure/energy pairs; and the module's canonical threshold is strictly positive. Those three fields are exactly the content of RSForcingChain004Cert.
In the broader forcing chain, this sits with T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law, which force the equilibrium at ratio one.
proof idea
One-line term proof. Nonempty is introduced by the already-built value cert : RSForcingChain004Cert, written as the anonymous constructor ⟨cert⟩. No tactics, no further lemmas: the witness is the packaged certificate assembled earlier in the same module from domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Closes inhabitance for the module-4 structural certificate, so downstream code can treat the three cost facts as a single inhabited bundle rather than three free hypotheses. The module doc marks the whole file as a structural theorem with zero sorry and zero axiom; this declaration is the final inhabitance stamp.
It sits on the J-cost side of the forcing chain (T5 J-uniqueness, equilibrium at ratio one). No used_by edges are recorded yet, so the immediate consumer is any later forcing-chain assembler that needs Nonempty of this cert type. No open scaffold remains in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.