parityCount_at_D3
plain-language theorem explainer
The declaration establishes that the parity count equals nine at the forced spatial dimension of three. Researchers assembling the integration gap certificate in Recognition Science would cite this when confirming the combinatorial structure of D squared times (D plus two) at the selected dimension. The proof is a one-line native decision that evaluates the squaring definition directly.
Claim. At the forced spatial dimension $D=3$, the parity count $D^2$ equals 9.
background
The IntegrationGap module defines the integration gap as the integer $D^2(D+2)$, called the consciousness gap in companion modeling work but treated here as a purely combinatorial quantity. At $D=3$ this evaluates to $9$ times $5$ equals 45. The parity count is introduced as the square of the dimension and counts the independent ledger parities. The upstream definition states: 'The parity count (number of independent ledger parities): $D^2$. At $D=3$, this equals 9.' D itself is fixed at 3 by the linking argument in Foundation.DimensionForcing.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate parityCount D directly from its definition as $d^2$.
why it matters
This supplies the parity_count component of the integrationGapCert record, which bundles the configuration dimension, parity count, gap value, and coprimality facts at D equals 3. It closes the combinatorial side of the integration gap once the forcing chain has selected D equals 3 among odd dimensions consistent with non-trivial linking. The result aligns with the eight-tick octave and spatial dimension selection in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.