D
plain-language theorem explainer
D is defined as the integer 3, the spatial dimension selected by the linking argument in Foundation.DimensionForcing. Researchers studying the integration gap D²(D+2) and its coprimality with recognition periods cite this constant when restricting dimensions to odd values consistent with orderly cycles. The declaration is a direct constant assignment with no computation or lemmas.
Claim. Let $D$ denote the spatial dimension forced by linking. Then $D = 3$.
background
The IntegrationGap module examines the integer $D^2(D+2)$, called the integration gap. At $D=3$ this equals 45, with $D^2=9$ as the parity count and $D+2=5$ as the configuration dimension. The module proves that gcd$(2^D, D^2(D+2))=1$ if and only if $D$ is odd, which combines with the linking argument to restrict $D$ to 3 among odd candidates. Upstream structures include SpectralEmergence, which derives exactly three particle generations and 24 chiral fermions from $D=3$, and PhiForcingDerived, which supplies the J-cost minimization underlying the dimension selection.
proof idea
The declaration is a direct constant definition assigning the natural number 3. No lemmas or tactics are invoked; it functions as the base value for sibling definitions such as configDim_at_D3 and integrationGap_at_D3.
why it matters
This supplies the concrete value required by the linking argument in Foundation.DimensionForcing and by the coprimality result that selects D=3 among odd dimensions. It aligns with framework landmarks including the eight-tick octave (period $2^3$), the emergence of SU(3)×SU(2)×U(1) gauge content, and the restriction to three spatial dimensions. The definition closes the combinatorial foundation for the integration gap calculations in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.