RSMTHStructural002Cert
plain-language theorem explainer
Certificate structure bundling three structural facts about domain cost and a positive threshold: diagonal vanishing, nonnegativity on positive pairs, and a strictly positive canonical threshold. Anyone citing the module's inhabited certificate or the golden-ratio J-cost package uses this type. It is a pure definitional record with no proof body; the fields are discharged by sibling lemmas when the certificate is built.
Claim. A certificate record asserting three claims: (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
This module packages structural facts about the Recognition Science J-cost near the golden ratio. The module doc states the target identity $J(\varphi)=\varphi-3/2\approx 0.11803$, the recognition cost of $\varphi$ itself. In the forcing chain, T5 fixes $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), uniquely among admissible costs.
Here domainCost is the two-argument cost used on positive reals in this structural layer; the diagonal condition says matched measure/expectation pairs carry zero cost. The nonnegativity field mirrors the upstream recognition-event fact that every event cost is nonnegative (via $J$-cost nonnegativity on positive states). canonicalThreshold is the positive cutoff used later in the same module.
The local status line is STRUCTURAL THEOREM: zero sorry, zero axioms. The structure itself only names the three propositions that a complete certificate must supply.
proof idea
No proof body: this is a structure definition whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Upstream, nonnegativity of recognition-event cost is already available as cost_nonneg from ObserverForcing (via Jcost_nonneg on positive state). The present declaration only records the interface those lemmas must satisfy.
why it matters
This record is the typed interface for Mathematics RS Structural Module 2, the golden-ratio J-cost package. Downstream, cert builds a concrete inhabitant and cert_inhabited proves Nonempty of the certificate type, closing the module's structural claim with no axioms.
In the broader framework it sits under T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point): the diagonal-zero and nonnegativity fields are the minimal analytic hygiene needed before quoting $J(\varphi)=\varphi-3/2$ as a genuine cost minimum rather than a formal identity. Consumers that need a single object asserting "domain cost is a nonnegative cost vanishing on matched pairs, with a positive threshold" depend on this type rather than on the three lemmas separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.