CMBOptDepth3Cert
plain-language theorem explainer
Certificate structure bundling three properties used for the RS CMB optical-depth claim: diagonal vanishing of the domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold. Cosmology pages that inhabit or discharge the optical-depth certificate cite it. Pure structure definition; no proof body.
Claim. A CMB optical-depth certificate is a triple of properties: (i) $\mathrm{domainCost}(r,r)=0$ for every real $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats reionization optical depth $\tau$ as a structural consequence of J-cost. Planck 2018 gives $\tau\approx 0.054$; the RS sketch is $\tau=J(\varphi)/2\approx 0.059$ (within $\sim 10%$), with an alternate form $J(\varphi)^2(\varphi-1)$ noted as weaker.
J-cost is the unique nonnegative recognition cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law (T5). The local domainCost is the two-argument cost used on mass/energy-like coordinates in this cosmology layer; the certificate demands it vanish on the diagonal and stay nonnegative off it. canonicalThreshold is the positive cutoff against which the optical-depth construction is compared.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The certificate rephrases that discipline at the domain-cost interface used by the CMB argument.
proof idea
No proof: this is a structure whose three fields are propositions. Downstream cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. cert_inhabited then packages ⟨cert⟩ as Nonempty.
why it matters
Gives a single named interface for the three algebraic side-conditions the CMB-from-J-cost story needs before quoting a numerical $\tau$. Downstream cert and cert_inhabited inhabit it, closing the module's structural claim (0 sorry, 0 axiom).
In the broader RS chain this sits under T5 J-uniqueness and the forced $\varphi$ fixed point (T6): optical depth is read off J-evaluations at $\varphi$, not fitted. It does not itself compute the Planck match; it only certifies the cost/threshold hygiene the match depends on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.