cert
plain-language theorem explainer
Packages three elementary properties of the domain cost and the canonical threshold into a single recombination certificate. Cosmologists working the RS derivation of z_rec ~ 1100 from the J-cost ladder would cite it as the structural witness. The body is a pure structure instance that wires three sibling lemmas; no new arithmetic is done.
Claim. There is a recombination certificate consisting of: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
The module treats recombination redshift as a J-cost structural fact. In RS units the observed $z_{\mathrm{rec}}\approx 1100$ is required to sit on the $\varphi$-ladder: $\log 1100/\log\varphi\approx 14.7$, so $z_{\mathrm{rec}}$ lies between $\varphi^{14}\approx 843$ and $\varphi^{15}\approx 1364$. The local cost is the standard Recognition J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), pulled back to a two-argument domain cost on mass and energy scales.
Recombin3Cert is the bundle of three positivity/vanishing facts needed before any threshold comparison: diagonal vanishing, nonnegativity for positive arguments, and a strictly positive canonical threshold. Upstream, the foundation lemma cost_nonneg already records that every recognition event has nonnegative J-cost; the domain-cost siblings specialize that fact to the cosmology setting.
proof idea
One-line structure instance. The three fields of Recombin3Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No tactics and no new calculation.
why it matters
Gives the inhabited certificate that the recombination-from-J-cost module advertises as a structural theorem (0 sorry, 0 axiom). The module status line ties $z_{\mathrm{rec}}=1100$ to the $\varphi$-ladder between rungs 14 and 15, consistent with the forcing-chain landmarks T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point). No downstream consumers are recorded yet; the certificate is the export surface for later redshift-band or threshold-crossing arguments in the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.