StructPhysicsM26Cert
plain-language theorem explainer
A certificate structure packaging three structural physics claims at recognition rung 26: the domain cost vanishes on the diagonal, is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. As a pure structure definition there is no proof body; the fields are Prop-valued obligations filled by sibling lemmas.
Claim. A structural physics certificate at rung 26 is a record of three facts: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e>0$, $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Module Structural_Physics_mod26 states a structural RS prediction for the Physics domain at recognition rung 26 (Plan v7, 120th pass). Status is structural theorem: zero sorry, zero axiom.
The domain cost $C(m,e)$ is the local cost functional on mass/energy-like arguments used in this certificate; sibling lemmas assert it vanishes when both arguments equal a nonzero $r$ and is nonnegative for positive inputs. The canonical threshold is the positive cutoff against which that cost is compared in the structural prediction.
Upstream, ObserverForcing records that every recognition event has nonnegative cost via the J-cost nonnegativity law ($J(x)=(x+x^{-1})/2-1$ for $x>0$), which is the same nonnegativity pattern the second field of this certificate reuses at the domain level.
proof idea
No proof body: this is a structure definition whose three fields are propositions. Inhabitation is deferred to the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields, and to cert_inhabited, which wraps that value as Nonempty.
why it matters
The certificate is the typed interface for the rung-26 structural physics claim in the RS forcing stack. Downstream, cert supplies a concrete record and cert_inhabited proves the type is nonempty, closing the module's structural theorem with no sorry.
In the broader framework this sits under the cost layer tied to T5 J-uniqueness and the Recognition Composition Law: diagonal vanishing and nonnegativity are the minimal structural properties a domain cost must inherit from $J$ before rung-specific physics predictions (mass ladder, thresholds near $\varphi$-powers) can be stated. It does not itself derive $D=3$ or the eight-tick octave; it packages the cost/threshold obligations those later physics modules assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.