parityCount_at_D3
plain-language theorem explainer
At spatial dimension three the independent ledger-parity count is nine. Gap-45 derivations and the NineParities bridge cite this equality. The proof is a one-line native decision that $3^2=9$.
Claim. Let the spatial dimension be $D=3$. Then the parity count $D^2$ equals $9$.
background
The module derives the coherence-energy gap exponent 45 from spatial dimension alone, closing boundary item B-22. A recognition event carries $D+2$ configuration degrees of freedom ($D$ spatial from T8, one temporal tick, one ledger-balance), so $E_{\mathrm{coh}}=\varphi^{-(D+2)}$. At $D=3$ this recovers $\varphi^{-5}$.
Spatial dimension is fixed by the constant $D:=3$ (T8). The parity count is the quadratic $d\mapsto d^2$: the number of independent ledger parities. The doc-comment notes that at $D=3$ the linear formula $3D$ coincides with $D^2$. The full gap is then the product $D^2(D+2)$.
Upstream, the same $D=3$ appears in AlphaDerivation and the FermionDOF gap bridge; the present lemma only evaluates the quadratic at that forced value.
proof idea
One-line term proof by native_decide. After unfolding parityCount d := d^2 and D := 3, the goal is the ground arithmetic fact $3^2=9$, which the kernel decides by computation. No lemmas are invoked.
why it matters
This is the parity half of the gap-45 factorization $D^2(D+2)=9\times 5=45$ at the T8 value $D=3$. Downstream, gap45_cert packages it as the parity_count field of the certificate, and parityCount_matches_enumeration rewrites through it to identify the parametric count with Fintype.card NineParities.ParityIndex (the explicit nine-parity enumeration).
Together with the dual-route identity $2^D-D=D+2$ (which holds only at $D=0,3$) and the coprimality results that force odd $D$, the lemma lets gap-45 follow from spatial dimension alone once Alexander duality has selected $D=3$. It is a tiny computational pin, but every later gap-45 claim depends on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.