firstPeak_eq
plain-language theorem explainer
Recognition Science cosmology derives the first CMB acoustic peak multipole exactly as 220 from the product of the baryon rung and configuration dimension. This supplies the numerical anchor for matching Planck observations within the F4 cosmology module. The proof is a direct decision procedure that evaluates the arithmetic definition of the peak.
Claim. The first acoustic peak multipole satisfies $ℓ_1 = 220$, where $ℓ_1$ is the product of the baryon rung and the configuration dimension.
background
The module derives CMB acoustic peaks from the Recognition Science phi-ladder in the F4 cosmology depth. The first peak multipole is defined as the product of the baryon rung (44) and configuration dimension (5), yielding exactly 220. The module doc states that RS predicts this equality exactly, with Lean status zero sorry and zero axiom.
proof idea
The proof is a term-mode wrapper that applies the decide tactic to the definition of the first peak as the product of the baryon rung and configuration dimension, confirming the numerical equality to 220 by direct computation.
why it matters
This theorem supplies the first peak value to the cmbCert certificate, which bundles the Planck match, second peak ratio band, and decomposition. It realizes the RS prediction that the first acoustic peak equals the product of baryon rung and configuration dimension, linking the phi-ladder to observed cosmology. It touches the T8 forcing of three spatial dimensions through the configuration dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.