cert
plain-language theorem explainer
Packages three structural facts for RS Standard Model module 2 into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy, and the canonical threshold is positive. Cited by anyone assembling the golden-ratio J-cost minimum package (J(φ)=φ−3/2). Construction is a structure instance wiring three already-proved sibling lemmas.
Claim. There is a structural certificate asserting: (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; (iii) the canonical threshold is strictly positive.
background
Module 2 of the RS Standard Model structural layer records the golden-ratio recognition cost: the J-cost minimum sits at $\phi$ with $J(\phi)=\phi-3/2\approx 0.11803$. The module is marked structural (zero sorry, zero axiom).
The certificate structure bundles three Prop fields. Domain cost is the local cost functional on mass/energy pairs used in this layer; its diagonal vanishing and nonnegativity are the cost axioms needed before any threshold comparison. The canonical threshold is the positive cutoff against which that cost is later compared.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative cost, via Jcost_nonneg). The present certificate specializes that idea to the domain-cost signature of this module.
proof idea
Definitional structure instance, not a tactic proof. The three fields of RSSTDStructural002Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the module-2 structural certificate so downstream Standard Model arguments can assume diagonal vanishing, cost nonnegativity, and a positive threshold in one hypothesis. Fits the forcing-chain cost layer: T5 fixes $J(x)=(x+x^{-1})/2-1$, and the golden-ratio fixed point (T6) is the self-similar minimum whose numerical value the module advertises.
No used_by edges are recorded yet; the immediate consumer is the sibling inhabitance fact and any later SM structural theorems that import this certificate rather than re-proving the three fields. Closes the packaging step for a zero-sorry structural block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.