RSCOSStructural006Cert
plain-language theorem explainer
Certificate bundling three structural obligations for the cosmology module on phi uniqueness (self-similar fixed point): diagonal vanishing of the domain cost, nonnegativity of that cost on the positive quadrant, and positivity of the canonical threshold. Cosmology and forcing-chain auditors cite it when discharging RS structural module 6. Pure structure definition; a separate inhabitant supplies the three proofs.
Claim. A structural certificate is a triple of facts: (1) for every real $r \neq 0$, the domain cost satisfies $C(r,r)=0$; (2) for all $m,e>0$, $C(m,e)\ge 0$; (3) the canonical threshold $T$ obeys $T>0$.
background
Module RS_COS_Structural_006 packages the cosmology side of RS phi uniqueness: phi as the self-similar continued-fraction fixed point $1+1/(1+1/(1+\cdots))$. Status is structural (zero sorry, zero axiom).
The certificate talks about a real bivariate domain cost $C(m,e)$ used in this module, together with a canonical threshold $T>0$. The diagonal clause $C(r,r)=0$ for $r\neq 0$ is the cost-minimum identity along equal arguments; nonnegativity on the positive quadrant is the local cost axiom.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via the J-cost minimum at $x=1$. The present fields are the cosmology-facing restatement of that nonnegativity plus the diagonal and threshold obligations needed for the phi fixed-point story.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is deferred. Downstream, the definition cert fills the fields by the sibling lemmas that prove diagonal vanishing, domain-cost nonnegativity, and threshold positivity; cert_inhabited then wraps that inhabitant as Nonempty.
why it matters
Gives a single named bundle for the three structural checks of cosmology module 6 (phi uniqueness / self-similar fixed point), aligning with forcing-chain landmark T6. Downstream cert is the concrete witness and cert_inhabited records that the certificate type is nonempty, so later cosmology developments can assume the package rather than re-prove the three clauses. Keeps the module's structural theorem status (0 sorry, 0 axiom) auditable at one declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.