RSForcingChain008Cert
plain-language theorem explainer
Certificate structure bundling three side conditions on a domain cost and a positive threshold for the phi-uniqueness forcing module. Cited by anyone who needs an inhabited witness that module-8 cost and threshold facts hold. Pure structure definition: no proof body; fields are discharged later by named lemmas.
Claim. A certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the diagonal pair $(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 8 of the RS forcing chain is the structural theorem that $\varphi=(1+\sqrt{5})/2$ is the unique fixed point of recognition recursion (zero sorry, zero axiom). The local cost object is a real-valued domain cost on pairs $(m,e)$; the diagonal vanishing and nonnegativity fields package the minimum-at-identity and positivity properties expected of a J-type cost.
Upstream, recognition-event cost is already known to be nonnegative: any recognition event $e$ satisfies $0\le e.\mathrm{cost}$ by nonnegativity of the J-cost on positive states. The third field requires a strictly positive canonical threshold used as a cutoff in the uniqueness argument.
The structure itself carries no computational content; it only names the three propositions that a later certificate instance must supply.
proof idea
No proof: this is a structure declaration. The three fields are bare propositions. Downstream, a single noncomputable instance fills them by applying the sibling lemmas that establish diagonal vanishing of domain cost, nonnegativity of domain cost on positive pairs, and positivity of the canonical threshold. Inhabitation is then the trivial constructor application of that instance.
why it matters
This certificate is the typed interface for Foundation module 8 (phi uniqueness). It is inhabited by the module's cert definition and exposed as nonempty by cert_inhabited, so any later forcing step that needs the cost-minimum, cost-nonnegativity, and positive-threshold package can depend on a single inhabited type rather than three separate lemmas.
In the broader chain this sits under T6: $\varphi$ forced as the self-similar fixed point of recognition recursion. The cost fields echo the J-cost minimum at the identity (T5 lineage) without re-proving J-uniqueness. The structure closes no open sorry; it only packages already-proved sibling facts for clean downstream consumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.