RSFDNStructural001Cert
plain-language theorem explainer
Certificate structure bundling three structural properties of the RS foundation cost: diagonal vanishing, non-negativity on positives, and positivity of the canonical threshold. Anyone citing the inhabited structural package (cert / cert_inhabited) depends on this shape. It is a pure structure definition with no proof body; inhabitants discharge the three fields separately.
Claim. A structural certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (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_FDN_Structural_001 packages the first structural prediction of Recognition Science: the cost takes the forced J-shape $J(x)=\frac12(x+1/x)-1$, with $\varphi$ the golden ratio and $D=3$ forced downstream. Status is structural theorem (zero sorry, zero axiom).
The domain cost is the real-valued cost assigned to a pair of positive scales (measure vs expectation, or more generally two nonzero reals). Its diagonal vanishing and non-negativity are the elementary positivity axioms that any admissible cost must satisfy before uniqueness (T5) is invoked. The canonical threshold is the positive cutoff used later as a recognition or creation barrier.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost non-negativity. The present structure lifts that idea to an explicit three-field certificate on the domain-cost interface used in this module.
proof idea
No proof: this is a structure declaration whose three fields are propositions. An inhabitant must supply proofs of diagonal vanishing of domain cost, non-negativity of domain cost on positive arguments, and positivity of the canonical threshold. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are the intended fillers; the def cert wires them in, and cert_inhabited packages Nonempty of the structure.
why it matters
This certificate is the typed interface for Structural Module 1. Downstream, cert builds a concrete inhabitant and cert_inhabited proves the type is nonempty, so later foundation code can assume the three properties by projecting fields rather than re-proving them.
In the forcing chain, these are the elementary cost axioms that sit under T5 J-uniqueness ($J(x)=\cosh(\log x)-1$), T6 $\varphi$ as self-similar fixed point, and T8 $D=3$. They do not themselves force the closed form of $J$, but they are the minimal positivity package any RS cost must carry before the Recognition Composition Law and uniqueness arguments apply. Closing this inhabited certificate is what lets the module claim structural-theorem status with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.