RSPHYStructural001Cert
plain-language theorem explainer
Certificate structure bundling three structural properties of the RS domain cost: it vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure structure definition with no proof body.
Claim. A structural certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module packages the first RS structural physics prediction: the cost functional is the unique $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 structural theorem (zero sorry, zero axiom).
The certificate refers to a domain-level cost domainCost on pairs of reals (mass and energy style arguments) and a fixed positive canonicalThreshold. Nonnegativity of recognition cost is the upstream fact from ObserverForcing: every recognition event has cost $\ge 0$, proved by reducing to $J$-cost nonnegativity on positive states. The diagonal-vanishing and threshold-positivity siblings live in the same module and supply the field witnesses.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the structural cost/threshold package that the module advertises (J-form, $\varphi$, $D=3$). Downstream, cert builds a concrete value and cert_inhabited proves Nonempty, so later physics layers can assume the certificate rather than restate the three lemmas. Sits at the physics face of the forcing chain landmarks T5 (J-uniqueness) and the nonnegativity of recognition cost from ObserverForcing. Does not itself force $\varphi$ or $D=3$; it only certifies the cost/threshold side conditions used in that structural story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.