cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the structural certificate for Foundation module 6 (phi as self-similar fixed point). Anyone citing the module's zero-sorry structural status uses this bundle. The definition is a pure structure inhabitant: it wires three already-proved field lemmas and adds no new argument.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of $(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
Module 6 of the Foundation structural series targets RS phi uniqueness: $\varphi$ as the self-similar continued-fraction fixed point $\varphi=1+1/(1+1/(1+\cdots))$, status STRUCTURAL THEOREM (0 sorry, 0 axiom). That is the T6 landmark in the forcing chain.
The certificate structure demands three properties of a real bivariate domain cost and a positive scalar threshold. Domain cost is the local cost functional on measure/expectation pairs; the diagonal vanishing clause says matched pairs carry zero cost, and nonnegativity is the usual J-cost lower bound transferred to that domain. Upstream, ObserverForcing already records that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states.
Siblings in the file supply the three field proofs (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos) and the threshold constant itself.
proof idea
One-line structure inhabitant. Each field is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and positivity of the threshold by canonicalThreshold_pos. No further rewriting or case analysis.
why it matters
Gives a single named witness that the cost/threshold interface required by structural module 6 is inhabited. Downstream consumers of the module can quote this certificate rather than reassemble the three lemmas. In the RS forcing chain this sits under T6 (phi forced as the self-similar fixed point); the cost side is the same J-family fixed at T5 by the Recognition Composition Law. No used_by edges are recorded yet, so the immediate role is module-level packaging and the companion cert_inhabited fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.