cert
plain-language theorem explainer
Packages three elementary cost facts into the Module-8 certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the structural phi-uniqueness theorem in this module will pull this bundle. The definition is a pure structure instance wiring three already-proved lemmas.
Claim. There is a certificate recording that (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; and (iii) the canonical threshold is strictly positive.
background
Module 8 of the RS forcing chain treats $\varphi=(1+\sqrt{5})/2$ as the unique fixed point of recognition recursion, and is marked as a structural theorem (zero sorry, zero axiom).
The certificate structure bundles three domain-cost hypotheses used throughout that argument: diagonal vanishing of the domain cost, nonnegativity of the domain cost on the positive quadrant, and positivity of a canonical threshold. Domain cost is the local cost functional on pairs of positive reals that the module uses in place of the global $J$-cost when comparing recognition ratios.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: any recognition event has cost $\ge 0$, via nonnegativity of $J$. The three field proofs domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos are sibling lemmas in this same module.
proof idea
One-line structure instance. Each of the three certificate fields is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further reasoning occurs at this declaration.
why it matters
This certificate is the packaged hypothesis bundle for Foundation Module 8, whose stated goal is RS $\varphi$-uniqueness: $\varphi=(1+\sqrt{5})/2$ is the unique fixed point of recognition recursion. In the global forcing chain that is landmark T6 ($\varphi$ forced as the self-similar fixed point), sitting after T5 $J$-uniqueness.
No downstream consumers are recorded yet in the graph, but the sibling cert_inhabited and the module's structural theorem status indicate this def is the inhabited witness that the cost/threshold side conditions hold, so later uniqueness arguments can cite a single object rather than three separate lemmas. It does not itself prove uniqueness of $\varphi$; it only certifies the cost setup those proofs rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.