cert
plain-language theorem explainer
Packages three structural facts about the Module-12 domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the RS dimensionless identity J(φ)=φ−3/2 would reach for this bundle. The definition is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
Module 12 of the RS forcing chain records the dimensionless identity $J(\varphi)=\varphi-3/2\approx 0.11803$, i.e. the J-cost of the golden ratio equals the golden ratio minus three-halves. The module is marked structural: zero sorry, zero axioms.
The certificate structure bundles three elementary properties of the local domain cost. Domain cost is the Module-12 specialization of the recognition cost; its diagonal vanishing says equal measure and excess incur zero cost, while nonnegativity is the usual J-cost lower bound. The canonical threshold is the positive cutoff used to separate trivial from nontrivial recognition events in this module.
Upstream, nonnegativity of recognition-event cost is already established in ObserverForcing via Cost.Jcost_nonneg on positive states. The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are the in-module witnesses that fill the certificate.
proof idea
One-line structure instance. The three fields of RSForcingChain012Cert are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or algebraic reduction occurs here.
why it matters
This certificate is the export surface of Foundation Module 12. Downstream consumers that need the dimensionless identity $J(\varphi)=\varphi-3/2$ can depend on a single inhabited certificate rather than three separate lemmas. In the broader forcing chain (T0–T8), Module 12 sits after J-uniqueness (T5) and the forcing of $\varphi$ as self-similar fixed point (T6); the identity $J(\varphi)=\varphi-3/2$ is the concrete numerical anchor that later mass-ladder and fine-structure work cite. No open scaffolding remains: the module status is structural with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.