RSSTDStructural002Cert
plain-language theorem explainer
A certificate packing three structural facts about the domain recognition cost: vanishing on the diagonal, nonnegativity for positive arguments, and positivity of the canonical threshold. Standard-model structural proofs cite it to discharge the RS_STD_002 interface in one place. It is a plain structure definition; inhabitants are built by wiring the three sibling lemmas.
Claim. A certificate consists of three properties of the domain cost $C$ and canonical threshold $\tau$: (i) $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
Module RS_STD_Structural_002 records the golden-ratio recognition cost: the J-cost minimum at $\varphi$ satisfies $J(\varphi)=\varphi-3/2\approx 0.11803$. Status is structural (no sorry, no axioms).
The domain cost $C(m,e)$ is the local cost functional on positive mass/energy-type arguments used in this Standard Model layer. The canonical threshold $\tau$ is the positive cutoff against which that cost is compared. Upstream, ObserverForcing already has nonnegativity of recognition-event cost via $J$-cost nonnegativity on positive states.
This structure does not prove those facts; it packages the three Prop fields that a complete certificate must supply.
proof idea
No proof body: this is a structure declaration. The three fields are pure propositions. Downstream, cert is a one-shot inhabitant that assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields; cert_inhabited then wraps that inhabitant as Nonempty.
why it matters
Gives a single typed handle for the three structural obligations of RS Standard Model structural module 2 (J-cost geometry at $\varphi$). Downstream cert and cert_inhabited close the module by exhibiting a concrete inhabitant, so later Standard Model layers can assume the bundle rather than re-prove diagonal vanishing, cost nonnegativity, and threshold positivity separately.
Ties to the Recognition forcing chain through the J-cost (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) and the forced self-similar fixed point $\varphi$ (T6). The module headline value $J(\varphi)=\varphi-3/2$ is the numerical landmark this certificate supports structurally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.