pith. machine review for the scientific record. sign in
def definition def or abbrev high

D

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  40def D : ℕ := 3

proof body

Definition body.

  41
  42/-- The configuration dimension of a recognition event:
  43    `D` spatial degrees of freedom + 1 temporal + 1 ledger balance. -/

depends on (5)

Lean names referenced from this declaration's body.