RSMTHStructural009Cert
plain-language theorem explainer
Certificate structure bundling three structural facts about domain cost and the canonical threshold: diagonal vanishing, non-negativity on positive arguments, and strict positivity of the threshold. Downstream code cites the inhabited instance to discharge the module's structural claim. Pure packaging: field types only, 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,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_009 sits in the mathematics layer of the Recognition Science forcing chain (T5 J-uniqueness through T8, $D=3$). It packages cost and threshold facts used as structural hypotheses rather than deriving new physics.
Domain cost is the real-valued comparison cost on a pair of positive scales (model versus evidence, or two ladder coordinates). It is built from the Recognition J-cost $J(x)=(x+x^{-1})/2-1$, which vanishes only at $x=1$ and is nonnegative elsewhere. The diagonal identity (equal arguments) therefore forces cost zero, matching the J-minimum.
Upstream, ObserverForcing already records that every recognition event has nonnegative cost via Cost.Jcost_nonneg. The canonical threshold is the positive cutoff used to separate admissible from inadmissible domain comparisons in this structural module.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is supplied separately by the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named bundle for the three structural obligations of module 9 so downstream code can demand Nonempty rather than three loose lemmas. The sibling cert builds an inhabitant; cert_inhabited records that the type is nonempty, closing the module's "STRUCTURAL THEOREM (0 sorry, 0 axiom)" claim.
In the forcing chain this is bookkeeping under T5–T8: J-cost nonnegativity and the unique minimum at identity are already forced; the certificate only freezes the domain-cost and threshold consequences needed by later mathematics modules. It does not advance a new forcing step; it stabilizes the cost interface those steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.