cmbCert
plain-language theorem explainer
cmbCert assembles the Recognition Science predictions for cosmic microwave background acoustic peaks into one verified certificate record. Cosmologists using RS models cite it to confirm the first peak multipole equals 220 exactly and the second-to-first ratio lies inside (2.3, 2.4). The definition is a direct record constructor that assigns three prior theorems to the structure fields.
Claim. The certificate asserts that the first acoustic peak multipole satisfies $ℓ_1 = 220$, that this value equals the Planck measurement, that the ratio of the second to first peak obeys $2.3 < ℓ_2/ℓ_1 < 2.4$, and that $ℓ_1$ decomposes exactly as the product of the baryon rung and the configuration dimension.
background
The module derives CMB acoustic peaks from Recognition Science by setting the first peak at multipole 220 via the exact product of baryon rung and configuration dimension. The CMBCert structure collects four properties: equality of the computed first peak to 220, agreement with the Planck value, confinement of the second-peak ratio to the open interval (2.3, 2.4), and the decomposition identity. Upstream theorems establish these facts separately: firstPeak_eq proves the numerical equality by decision, firstPeak_matches_planck confirms the Planck match by decision, and secondPeakRatio_band proves the ratio bounds by unfolding the ratio definition followed by numerical normalization.
proof idea
The definition is a one-line wrapper that populates the CMBCert record by direct field assignment: first_peak receives firstPeak_eq, matches_planck receives firstPeak_matches_planck, second_ratio_band receives secondPeakRatio_band, and decomposition receives reflexivity.
why it matters
cmbCert supplies the terminal certificate for the RS CMB peak predictions, closing the module-level claim that the first peak arises exactly as baryon rung times configuration dimension. It supports the broader Recognition Science derivation of cosmology from the forcing chain and the phi-ladder mass formula. No downstream results are recorded, so the certificate stands as a self-contained, fully proved statement with zero axioms or open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.