cert
plain-language theorem explainer
Packages three elementary domain-cost facts into one certificate for the phi-uniqueness structural module: cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the module-6 structural theorem uses this bundle rather than the three lemmas separately. The definition is a pure structure inhabitant that wires already-proved sibling lemmas.
Claim. There is a certificate recording that (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; and (iii) the canonical threshold is strictly positive.
background
Module 6 of the StandardModel structural series treats RS phi uniqueness: $\varphi$ as the self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$. The module is marked structural (zero sorry, zero axiom).
The certificate structure bundles three properties of a domain-level cost functional. Domain cost is the local cost comparison used in this module; its diagonal vanishing and nonnegativity mirror the global J-cost facts from the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$, minimized at $x=1$). Upstream, cost_nonneg in ObserverForcing states that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states.
The third field asserts positivity of a canonical threshold used as a cutoff in the same structural argument.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work occurs. The nonnegativity field is the domain-level analogue of the upstream ObserverForcing cost nonnegativity theorem.
why it matters
Gives a single named certificate object for Structural Module 6 (phi uniqueness / self-similar fixed point), aligning with forcing-chain landmark T6. Downstream consumers can depend on one inhabitant rather than three separate lemmas. The module claims structural status with zero sorry and zero axiom; this definition is the packaged evidence of that claim for the cost-and-threshold fragment. No further used-by edges are recorded yet, so the certificate is presently a terminal packaging node inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.