CMBCert
plain-language theorem explainer
CMBCert bundles four properties that certify the RS-derived first CMB acoustic peak equals 220 and lies inside the Planck band while the second-to-first ratio sits in (2.3, 2.4). Cosmologists working inside the Recognition Science phi-ladder framework would cite the structure to connect the baryon rung of 44 directly to the observed multipole. The record is assembled from sibling definitions of the rung and dimension together with reflexivity on their product.
Claim. The structure certifies that the first acoustic peak satisfies $ℓ_1 = 220$, that this value equals the Planck reference, that the ratio of the second to first peak lies in the open interval $(2.3, 2.4)$, and that $ℓ_1$ equals the product of the baryon rung (equal to 44) and the configuration dimension (equal to 5).
background
In CosmicMicrowaveBackgroundFromRS the first acoustic peak is defined by firstPeak := baryonRung * configDim. The baryon rung is imported as the constant 44 from the phi-ladder treatment of baryon asymmetry, while configDim is fixed at 5. The Planck reference is the constant 220 and the second-peak ratio is the rational 507/220, which the module places inside (2.3, 2.4). The module documentation states that RS yields $ℓ_1 = 44 × 5 = 220$ exactly under this decomposition.
proof idea
The declaration is a structure whose fields are populated by direct references to the sibling definitions firstPeak, firstPeakPlanck, secondPeakRatio and the decomposition equality. No tactics appear inside the structure; the downstream construction supplies the concrete values via reflexivity on the product and a norm_num lemma for the ratio band.
why it matters
CMBCert is instantiated by cmbCert, thereby closing the link from the phi-ladder baryon rung through the configuration dimension to the observed CMB peaks. It realizes the module claim that the first peak equals 220 exactly, connecting to the eight-tick octave and D = 3 via configDim. The structure touches the open question of whether the full acoustic spectrum follows from the same ladder parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.