Pith. sign in
theorem

parityCount_at_D3

proved
show as:
module
IndisputableMonolith.Foundation.GapDerivation
domain
Foundation
line
64 · github
papers citing
none yet

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.