RSMTHStructural007Cert
plain-language theorem explainer
Certificate structure bundling three arithmetic facts about the domain recognition cost: it vanishes on equal positive ratios, stays non-negative off the diagonal, and the module's canonical threshold is strictly positive. Anyone citing the RS structural claim that recognition cost is ratio-symmetric (J(x)=J(1/x)) uses this bundle as the formal witness type. It is a pure structure definition; inhabitants are supplied by the sibling `cert` construction.
Claim. A certificate is a triple of statements: (1) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (2) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (3) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_007 records the structural fact that the RS J-cost is ratio-symmetric: $J(x)=J(1/x)$. In the Recognition framework the cost functional is the unique continuous solution of the Recognition Composition Law forced at T5, namely $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), which is minimized at $x=1$ and invariant under $x\mapsto 1/x$.
Here domainCost is the two-argument specialization of that cost to a measured ratio pair $(m,e)$. The diagonal identity domainCost r r = 0 is the statement that equal measure and expectation sit at the J-minimum. Non-negativity for positive arguments is the real-arithmetic shadow of the upstream theorem that every recognition event has nonnegative cost (cost_nonneg in ObserverForcing, via Jcost_nonneg).
canonicalThreshold is the module's fixed positive cutoff used to separate trivial from nontrivial cost comparisons; positivity is part of the certificate so downstream consumers need not re-prove it.
proof idea
No proof body: the declaration is a structure (record type) whose three fields are propositions. Inhabitation is deferred to the sibling definition cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields, and to cert_inhabited, which packages that assignment as Nonempty.
why it matters
Gives the Mathematics layer a named, reusable witness type for the structural theorem "recognition cost is ratio-symmetric" (module status: 0 sorry, 0 axiom). Downstream, cert is the canonical inhabitant and cert_inhabited exposes non-emptiness for any consumer that only needs existence. The three packed facts are exactly the arithmetic content needed to treat $J(x)=J(1/x)$ as a certified structural lemma rather than an ad-hoc rewrite. In the forcing chain this sits under T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which already forces the reciprocal symmetry used here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.