cert
plain-language theorem explainer
Packages three domain-cost facts (vanishes on the diagonal, nonnegative for positive arguments, positive canonical threshold) into one certificate object. Cited by anyone assembling golden-ratio universality from J-cost in the RS foundation. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
The module develops golden-ratio universality in Recognition Science from the J-cost alone. Status is structural: zero sorry, zero axioms. The module doc stresses that $\varphi$ appears in particle masses (phi-rungs), the cosmological constant ($8\varphi^5/45$), Hubble tension, neutron lifetime, and qubit coherence ratios, all forced by J-uniqueness (forcing chain T5–T6).
GoldRatioUniv3Cert is the local certificate structure. Its three fields demand: (i) domain cost vanishes when model and experiment coincide, (ii) domain cost is nonnegative on the positive quadrant, and (iii) the canonical threshold is positive. Domain cost is the RS cost pulled back to a model/experiment pair; nonnegativity ultimately traces to Cost.Jcost_nonneg via the upstream cost_nonneg fact that every recognition event has nonnegative cost.
The canonical threshold is the positive cutoff used to separate forced self-similar fixed-point behaviour from the rest of the cost landscape.
proof idea
Pure structure inhabitant. The three fields of GoldRatioUniv3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra tactics or algebraic work; the definition is the certificate bundle itself.
why it matters
Gives a single named inhabitant that later golden-ratio universality arguments can assume or pass around, rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity each time. Sits in the foundation layer that turns J-uniqueness (T5: $J(x)=(x+x^{-1})/2-1$) into the forced self-similar fixed point $\varphi$ (T6). The module frames this as the structural backbone for $\varphi$ appearing across masses, cosmology, and coherence ratios. No downstream consumers are wired yet in the graph; the sibling cert_inhabited is the natural next step that records inhabitance of the certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.