configDim
plain-language theorem explainer
The configuration dimension augments a spatial dimension d by two units to incorporate one temporal coordinate and one ledger-balance coordinate in each recognition event. Cosmologists deriving the first CMB acoustic peak at 220 and baryon asymmetry trajectories cite this definition to obtain the factor five at D equals three. It is realized by a direct arithmetic definition with no lemmas or tactics.
Claim. For spatial dimension $D$, the configuration dimension is $D + 2$, accounting for the $D$ spatial degrees of freedom together with one temporal and one ledger-balance coordinate.
background
The Integration Gap module defines the integration gap as $D^2(D + 2)$, which equals 45 when $D = 3$. Here $D^2$ is the parity count of independent ledger parities and $D + 2$ is the configuration dimension. The sibling definition sets $D := 3$, the value selected by the linking argument in Foundation.DimensionForcing.
proof idea
The declaration is a direct definition that sets configDim d to d plus 2. No upstream lemmas are applied and no tactics are used; the body consists solely of the arithmetic expression.
why it matters
This supplies the numerical factor five that multiplies the baryon rung to produce the first acoustic peak position 220 in CMBCert and firstPeak. It enters the etaB rung derivations for counterfactual dimensions D1, D2, D5 and the twelve-is-D-4 cardinality spectrum result. The definition realizes the addition of temporal and ledger coordinates to the three spatial dimensions forced at T8, consistent with the eight-tick octave period and the Recognition Composition Law. It closes the combinatorial specification of the integration gap at D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.