configDim
plain-language theorem explainer
The definition fixes the configuration dimension at 5 for RS cosmology calculations. Researchers deriving the first CMB acoustic peak multipole would cite it to obtain ℓ₁ = 44 × 5 = 220 exactly. It is a direct numerical assignment with no lemmas or computation.
Claim. The configuration dimension is defined as the constant 5.
background
In the RS framework the configuration dimension counts the total degrees of freedom in a recognition event: D spatial dimensions plus one temporal dimension plus one ledger-balance dimension. For the standard D = 3 case this yields exactly 5. The present module uses this value to express the first acoustic peak as the product of the baryon rung (44) and configDim. Upstream, the same identifier appears in IntegrationGap as d + 2 and in CoalitionSizeFromConfigDim as the base for 2^D - 1 coalition types.
proof idea
Direct constant definition; no tactics or upstream lemmas are invoked.
why it matters
This supplies the numerical factor required by the CMBCert structure and the firstPeak definition to certify ℓ₁ = 220 and the second-peak ratio band. It realizes the T8 step of the forcing chain by embedding D = 3 spatial dimensions into the cosmology module. The value propagates into etaB_pos and the counterfactual rung derivations in EtaBExactRungDerivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.