cert
plain-language theorem explainer
Packages three elementary domain-cost facts into the structural certificate for cosmology module 6 (phi as self-similar fixed point). Anyone citing the module's zero-sorry structural claim uses this bundle. The definition is a pure structure inhabitant: it wires already-proved diagonal vanishing, nonnegativity, and positive threshold lemmas into the certificate fields.
Claim. There is a structural certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of the 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 6 sits in the cosmology structural layer and records the Recognition Science claim that $\varphi$ is forced as the self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$, matching forcing-chain step T6. Status is structural theorem: zero sorry, zero axioms.
The certificate structure collects three analytic side-conditions on a real bivariate domainCost and a positive real canonicalThreshold. Domain cost is the local cost functional used in this module (imported from the global cost layer); its nonnegativity is the continuum shadow of the foundation fact that every recognition event has nonnegative $J$-cost, $J(x)=(x+x^{-1})/2-1$.
Upstream, ObserverForcing.cost_nonneg states that the cost of any recognition event is nonnegative via Jcost_nonneg at positive state. The in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that picture to the cosmology domain-cost and threshold symbols.
proof idea
One-line structure construction. The three certificate fields are filled by direct assignment of the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra algebra or tactics: the definition is the inhabitant that witnesses the structure is nonempty once those three facts are available.
why it matters
Gives a single named certificate object for RS cosmology structural module 6, so downstream cosmology developments can depend on one package rather than three scattered lemmas. The module doc frames the content as the structural theorem for phi uniqueness (self-similar fixed point), i.e. forcing-chain landmark T6. No used_by edges are recorded yet; the certificate is the export surface of the module. It does not itself derive $\varphi= (1+\sqrt{5})/2$ from the Recognition Composition Law; it only certifies the cost/threshold side-conditions that the structural story assumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.