parityCount_matches_enumeration
plain-language theorem explainer
At spatial dimension D = 3 the parametric parity count D² equals the cardinality of the nine enumerated ledger parities. Anyone assembling the gap-45 certificate or linking the D² formula to the concrete ParityIndex type cites this. The proof is a two-step rewrite: both sides reduce to 9.
Claim. With spatial dimension $D = 3$, the parametric parity count satisfies $\mathrm{parityCount}(D) = |\mathrm{ParityIndex}|$, i.e. $D^2$ equals the number of enumerated ledger parity indices.
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 balance from ledger neutrality $J(x)=J(x^{-1})$ at T3), so the coherence energy is $E_{\mathrm{coh}}=\varphi^{-(D+2)}$. At $D=3$ this is $\varphi^{-5}$.
The parity count is defined parametrically by $\mathrm{parityCount}(d)=d^2$, the number of independent ledger parities. At $D=3$ the linear formula $3D$ coincides with $D^2$. Separately, NineParities enumerates nine concrete indices (charge-parity, $B-L$, hypercharge, tick reversal, color Cartan generators, and so on) as the inductive type ParityIndex, with $\mathrm{Fintype.card},\mathrm{ParityIndex}=9$.
Upstream, parityCount_at_D3 records $\mathrm{parityCount},D=9$ by native decision, and parity_count_eq_nine records the enumeration cardinality.
proof idea
Term-mode proof by two rewrites. First apply parityCount_at_D3 to replace the left-hand side $\mathrm{parityCount},D$ by $9$. Then apply NineParities.parity_count_eq_nine to replace the right-hand side $\mathrm{Fintype.card},\mathrm{ParityIndex}$ by $9$. Both sides match, so the equality holds. No case analysis or induction.
why it matters
This is the bridge between the parametric $D^2$ formula and the concrete nine-parity enumeration used elsewhere in the foundation. Downstream it is a field of gap45_cert, which packages config dimension, parity count, the match proved here, the gap identity $D^2(D+2)=45$, and coprimality at $D=3$.
In the Recognition chain the gap $45$ is the coherence-energy exponent product that yields the matter-coherence link $\varphi^{1-\mathrm{gap}}\times\varphi^{\mathrm{gap}}=\varphi$. Matching the abstract count to ParityIndex ensures the gap derivation is not floating free of the enumerated ledger structure. Combined with T8 forcing $D=3$ and the coprimality argument that $D$ must be odd, gap-45 follows from dimension alone. Status in-module: 0 sorry, 0 axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.