RSFDNStructural007Cert
plain-language theorem explainer
Certificate structure packaging three structural facts about domain recognition cost: it vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Consumers of Foundation structural module 7 (J-cost ratio symmetry) cite the inhabited instance. Pure definitional packaging of Prop fields; no proof body.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Foundation structural module 7 records RS J-cost symmetry: $J(x)=J(1/x)$, so recognition cost is ratio-symmetric. Status is a structural theorem (zero sorry, zero axiom). The module works with a domain cost on pairs of reals (sibling domainCost), together with a positive canonical threshold used as a comparison scale.
Upstream, ObserverForcing already has nonnegativity of recognition-event cost: any event cost is $\ge 0$ because $J$-cost is nonnegative on positive states. The present structure lifts the same nonnegativity idea to the two-argument domain cost, and adds diagonal vanishing and threshold positivity as the certificate interface.
Sibling lemmas supply the three field proofs separately (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos); this declaration only names the bundle.
proof idea
No proof: this is a structure definition whose three fields are propositions. Inhabitation is deferred to the downstream cert value, which fills the fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for RS structural item 007 (J-cost ratio symmetry). Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of the certificate, so later foundation code can depend on one named bundle rather than three loose lemmas.
In the Recognition forcing chain this sits under T5 J-uniqueness: $J(x)=(x+x^{-1})/2-1$ is forced and is automatically ratio-symmetric, which is exactly the structural content the module advertises. The certificate does not itself derive $J$ from the RCL; it freezes the cost-level consequences (diagonal zero, nonnegativity, positive threshold) that symmetry consumers need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.