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

phasePeriod

show as:
view Lean formalization →

The definition computes the phase period for a given spatial dimension as the triangular number of its square. Researchers working on synchronization minimization in the Dimensional Rigidity paper cite it to show that D equals 3 yields the shortest period among odd dimensions. It is implemented as a direct one-line application of the triangular number function.

claimFor a spatial dimension $D$, the phase period is $T(D^2)$, where $T(n) = n(n+1)/2$.

background

The module formalizes constraint (S) from the Dimensional Rigidity paper, showing that among odd dimensions $D$ at least 3, $D$ equals 3 uniquely minimizes the synchronization period given by the least common multiple of $2^D$ and the phase period. The triangular number $T(n)$ equals $n$ times $(n+1)$ divided by 2, arising as the cumulative phase from the $D^2$ entries in the parity matrix of the hypercube $Q_D$ (module doc). Upstream, the triangular number definition in the same module specializes the fundamental periods abbrev from Breath1024.

proof idea

The definition is a one-line wrapper that applies the triangular number function $T$ to the square of the input dimension.

why it matters in Recognition Science

This definition supplies the phase period value used in the ConstraintS_Cert structure that packages the full certificate for constraint (S), including the phase value 45 at $D$ equals 3 and the coprimality conditions for odd dimensions. It supports the paper claim that $D$ equals 3 gives the minimal sync period of 360. In the Recognition Science framework it connects to the generalization of the eight-tick octave to period $2^D$ and the forcing of $D$ equals 3 spatial dimensions.

scope and limits

formal statement (Lean)

  53def phasePeriod (D : ℕ) : ℕ := T (D * D)

proof body

Definition body.

  54

used by (24)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.