cert
plain-language theorem explainer
Packages three structural facts about the domain cost used for CMB reionization optical depth into a single certificate: diagonal vanishing, non-negativity on positive arguments, and a strictly positive canonical threshold. Cosmologists working the RS optical-depth match (tau near Planck 0.054 via J(phi)) would cite it. Construction is pure field assignment from three sibling lemmas.
Claim. There exists a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats CMB reionization optical depth in Recognition Science units. Planck 2018 reports $\tau \approx 0.054$; the RS sketch is $\tau \approx J(\varphi)/2 \approx 0.059$ (within about 10%), with $J$ the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$.
domainCost is the local cost functional on mass/energy-like pairs; the certificate structure CMBOptDepth3Cert records the three properties needed before any threshold comparison: vanishing on the diagonal (zero defect when the two arguments agree), non-negativity for positive inputs, and positivity of canonicalThreshold. Upstream, non-negativity of recognition cost is the standard fact that $J\ge 0$ on positive reals (ObserverForcing / Cost).
proof idea
Definitional structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work.
why it matters
Closes the structural side of the CMB-optical-depth-from-J-cost session (module status: 0 sorry, 0 axiom). It is the packaged witness that the domain cost behaves like a genuine J-style cost before one compares against the canonical threshold that is meant to underwrite the $\tau\sim J(\varphi)/2$ numerics. No downstream consumers are wired yet in the graph; the natural parent is any theorem that turns this certificate into a quantitative optical-depth bound. Lands in the cosmology layer that sits on T5 J-uniqueness and the $\varphi$ fixed point (T6), not on the forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.