parityCount
plain-language theorem explainer
Independent ledger parities in spatial dimension d number d². Gap-45 and η_B rung derivations cite it as the parity factor in the product D²(D+2). The body is the pure power d^2; at d=3 it equals both 9 and the NineParities enumeration.
Claim. For any natural number $d$, the number of independent ledger parities is $d^{2}$. At spatial dimension $D=3$ this coincides with the linear count $3D$ and equals $9$.
background
Module GapDerivation closes boundary item B-22: a recognition event has configuration dimension $D+2$ ($D$ spatial from T8, one temporal tick from T2, one ledger-balance degree from T3), so the coherence energy is $\varphi^{-(D+2)}$. At the forced $D=3$ this is $\varphi^{-5}$, matching Constants.E_coh.
The gap itself is the product of two factors: the parity count and the configuration dimension. Sibling D is fixed at 3 by T8. The doc-comment notes that the linear formula $3D$ agrees with $D^{2}$ only at $D=0$ and $D=3$, so the quadratic form is the dimension-general definition while still recovering the familiar nine parities in three-space.
Upstream dimension abbreviations (Constants, DimensionForcing, SubstrateAxioms) all treat spatial dimension as a natural number forced to 3; this definition is the parity-side counterpart used when the gap is written parametrically in $d$.
proof idea
Pure definitional abbreviation: parityCount d unfolds to d ^ 2. No lemmas, tactics, or hypotheses. Downstream equalities such as parityCount_at_D3 discharge the $d=3$ case by native_decide.
why it matters
Supplies the first factor of dimensionGap d := parityCount d * configDim d, which at $D=3$ is $9\times 5=45$ (gap_at_D3). That identity is the arithmetic content of B-22 and of the Gap45Cert bundle (parity_count, parity_matches, gap, coprime).
Downstream, parityCount_matches_enumeration ties the parametric $D^{2}$ to Fintype.card NineParities.ParityIndex, and eta_B_rung_from_dimension_factored rewrites the baryon asymmetry rung as $A$ minus the product of parity count and configuration dimension. Framework landmarks: T8 forces $D=3$; the eight-tick octave and ledger neutrality fix the $+2$ in the coherence exponent; gap-45 then follows from dimension alone once coprimality selects odd $D$ and Alexander duality pins $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.