RSFDNStructural006Cert
plain-language theorem explainer
Certificate structure bundling three structural facts for the phi-uniqueness module: domain cost vanishes on equal nonzero arguments, is nonnegative for positive measure and energy, and the canonical threshold is strictly positive. Anyone citing the module's inhabited certificate or the T6 self-similar fixed-point package will pull this bundle. It is a pure structure definition; inhabitants are assembled from three sibling lemmas with no proof body here.
Claim. A structural certificate comprises three properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all reals $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module is Foundation RS Structural Module 6, whose stated subject is RS phi uniqueness: phi as the self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$. The module is marked structural theorem status (zero sorry, zero axiom).
Domain cost is the real-valued cost on pairs of reals (measure/energy style arguments) used in the local recognition setting. The upstream ObserverForcing lemma records that "the cost of any recognition event is non-negative," obtained from nonnegativity of the J-cost on positive states. The canonical threshold is the positive cutoff paired with that cost in the structural comparison that forces phi.
The three fields of this structure are exactly the side conditions sibling lemmas already prove about domain cost on the diagonal, domain-cost nonnegativity, and positivity of that threshold.
proof idea
Pure structure definition: no tactics and no proof term. It only declares the three fields an inhabitant must supply (diagonal vanishing of domain cost, nonnegativity for positive arguments, and positivity of the canonical threshold). The concrete inhabitant in the same module fills those fields by direct assignment from the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Upstream cost_nonneg from ObserverForcing is the conceptual ancestor of the nonnegativity field, via J-cost nonnegativity.
why it matters
Packages the cost and threshold side conditions required by the phi-uniqueness structural theorem, i.e. forcing-chain step T6 (phi forced as the self-similar fixed point of the continued reciprocal). Downstream, the module's cert builds one concrete inhabitant, and cert_inhabited shows the certificate type is nonempty, which is the discharge step for Structural Module 6.
In the broader Recognition framework this sits under the J-cost / Recognition Composition Law layer: nonnegativity and the zero-on-identity behaviour are the structural shadows of $J(x)=(x+x^{-1})/2-1$ minimized at $x=1$. It does not itself derive phi or the eight-tick octave; it only certifies the local cost/threshold hypotheses those later steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.