phasePeriod_3
plain-language theorem explainer
The declaration shows that the phase period function evaluates to 45 at dimension 3. Researchers studying synchronization minimization among odd spatial dimensions would cite this to anchor the base case for the minimal period. The proof applies a native decision procedure to the triangular number definition.
Claim. $T(9) = 45$, where $T(n) = n(n+1)/2$ is the $n$th triangular number and the phase period at dimension $D$ is defined as $T(D^2)$.
background
The phase period function computes the triangular number of $D$ squared for a given dimension $D$. This module formalizes constraint (S) from the Dimensional Rigidity paper, showing that $D=3$ minimizes the synchronization period lcm($2^D$, $T(D^2)$) among odd $D$ ≥ 3. The upstream definition supplies phasePeriod (D : ℕ) : ℕ := T (D * D), with T the triangular number.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate the equality directly from the triangular number definition.
why it matters
This anchors the specific value for $D=3$ in the argument that odd dimensions yield coprime periods and $D=3$ minimizes the sync cost. It ties to the eight-tick octave (period $2^3$) in the Recognition Science forcing chain. The result supports the selection of 45 as the phase period at the dimension minimizing synchronization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.