RSSTDStructural007Cert
plain-language theorem explainer
Certificate record that packages three structural facts about the Standard Model domain cost: it vanishes on equal nonzero arguments, stays nonnegative for positive mass/energy inputs, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance and the concrete cert filler. Pure structure definition; no proof body.
Claim. A structural certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 7 of the Standard Model structural series records ratio-symmetry of recognition cost: the J-cost satisfies $J(x)=J(1/x)$. In RS units the cost functional is the unique continuous solution of the Recognition Composition Law forced at T5, namely $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), which is minimized at $x=1$ and nonnegative on $\mathbb{R}_{>0}$.
Here domain cost is the concrete pairing of two positive scale parameters (mass-like and energy-like) through that J-cost. The upstream fact cost_nonneg states that every recognition event has nonnegative cost, proved by reducing to nonnegativity of $J$ on positive states. The canonical threshold is the positive cutoff used to separate structural zero-cost identities from genuine recognition events.
proof idea
No proof: the declaration is a structure whose three fields are propositions. Inhabitation is supplied downstream by the noncomputable cert definition, which fills the fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The companion theorem cert_inhabited then wraps that instance as Nonempty.
why it matters
Gives a single named bundle for the three cost axioms needed by later Standard Model structural certificates. Downstream, cert builds a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the module's "STRUCTURAL THEOREM (0 sorry, 0 axiom)" claim.
In the forcing chain this sits under T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which force ratio symmetry and the zero-at-identity law used in field (i). The nonnegativity and positive-threshold fields keep domain cost aligned with the global recognition-event cost calculus, so SM structural arguments can quote one certificate rather than three separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.