cert
plain-language theorem explainer
Packages three elementary facts about the domain cost into a single certificate for the phi-uniqueness structural module: the cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the module's structural theorem uses this bundle rather than the three lemmas separately. The definition is a pure structure inhabitant that wires three sibling proofs into the certificate fields.
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 RS_MTH_Structural_006 treats the Recognition Science claim that $\varphi$ is the unique self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$, recorded as a structural theorem with no sorry and no extra axioms. That claim sits at forcing step T6 in the unified chain.
The certificate structure collects three cost-side side conditions used in that argument. Domain cost is the local cost functional on pairs of positive reals (imported from the Cost layer and tied to the J-cost $J(x)=(x+x^{-1})/2-1$). The first field says cost is zero when the two arguments coincide and are nonzero; the second says cost is nonnegative on the positive quadrant; the third asserts that a fixed positive threshold (the module's canonical cutoff) is strictly above zero.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," proved via $J$-cost nonnegativity on positive states. The present fields are the analogous statements specialized to the domain-cost wrapper used here.
proof idea
One-line structure inhabitant. Each field is filled by the corresponding sibling lemma already proved in the same module: domainCost_at_eq supplies diagonal vanishing, domainCost_nonneg supplies nonnegativity on positive pairs, and canonicalThreshold_pos supplies positivity of the threshold. No extra tactics or algebraic work occur at this site.
why it matters
Gives a single named witness that the cost hypotheses required by the phi-uniqueness structural theorem are inhabited. In the Recognition forcing chain this supports T6 (phi forced as the self-similar fixed point). Downstream use count is currently zero in the mirror graph, so the certificate is a local packaging step rather than a widely re-used lemma; the sibling cert_inhabited is the natural next consumer. It does not itself derive uniqueness of $\varphi$ or the Recognition Composition Law; it only certifies the cost side-conditions the uniqueness argument is allowed to assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.