cert
plain-language theorem explainer
Packages three structural facts for RS Standard Model module 1 into a single certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cited by anyone who needs the structural package rather than the individual lemmas. Construction is a pure structure instance that wires three already-proved sibling lemmas.
Claim. There is a structural certificate asserting: (i) for every real $r \neq 0$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module records the first RS structural package for the Standard Model layer: the cost is the classical J-cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$), with $\varphi$ the golden ratio and spatial dimension $D=3$ forced. Status is a structural theorem block with zero sorry and zero axioms.
The certificate structure bundles three properties of a domain-level cost: vanishing on the equal-argument diagonal, nonnegativity for positive mass/energy-style arguments, and positivity of a canonical threshold. Upstream, cost_nonneg in ObserverForcing states that the cost of any recognition event is nonnegative, via Jcost_nonneg on a positive state; the identity event sits at the J-cost minimum $x=1$.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields; this definition only assembles them.
proof idea
Pure structure-instance construction, not a tactic proof. The three fields of RSSTDStructural001Cert are filled by direct assignment: diagonal vanishing from domainCost_at_eq, nonnegativity from domainCost_nonneg, and threshold positivity from canonicalThreshold_pos. No further rewriting or case analysis occurs at this site.
why it matters
Gives a single named inhabitant of the module-1 structural certificate so downstream Standard Model material can depend on one object rather than three separate lemmas. Aligns with the forcing-chain landmarks T5 (J-uniqueness of $J(x)=\frac12(x+x^{-1})-1$) and the module claim that $\varphi$ and $D=3$ are forced, though those forcings are not re-proved here.
No used_by edges are recorded yet; the immediate consumer in-module is the inhabitedness wrapper around this certificate. The declaration closes the packaging step for a zero-sorry structural block rather than advancing a new physical identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.