AllPhysics5Cert
plain-language theorem explainer
A certificate structure packaging three elementary properties of the AllPhysics5 domain cost and threshold: diagonal vanishing, non-negativity on positive arguments, and positivity of the canonical threshold. Downstream code cites it to inhabit a single Nonempty witness that the session's cost layer is well-formed. There is no proof body; the fields are Prop-typed requirements filled by sibling lemmas.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost of $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The AllPhysics5 module is the structural end-session claim that the full physics stack (gravity, EM, weak, strong, Higgs, matter masses, cosmology) is forced from the single J-cost $J(x)=(x+x^{-1})/2-1$, with zero free parameters and no axioms or sorries.
Domain cost is the session's real-valued cost on pairs $(m,e)$; the diagonal identity domainCost r r = 0 for $r\neq 0$ encodes perfect self-match, while non-negativity on positive arguments is the cost-layer analogue of the upstream recognition-event fact that every event cost is nonnegative (via Jcost_nonneg). The canonical threshold is the positive cutoff used to separate admissible recognition regimes.
The structure itself carries no computational content: it is a Prop-bundle that later cert and cert_inhabited discharge with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
proof idea
No proof body: this is a structure declaration whose three fields are propositions. Inhabitation is deferred to the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos fieldwise, and to cert_inhabited, which wraps that assignment as Nonempty AllPhysics5Cert.
why it matters
Inside AllPhysics5 this is the typed interface that the session's cost layer must satisfy before the broader "all of physics from $J(x)$" claim is treated as structurally closed. The parent objects are cert (the concrete witness) and cert_inhabited (the Nonempty theorem). It sits at the foundation layer that underwrites the forcing chain's cost uniqueness (T5 J-uniqueness and the Recognition Composition Law), without itself deriving masses, couplings, or cosmological parameters. Its role is bookkeeping: one place to name the three cost/threshold obligations the rest of the module relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.