phasePeriod_11
plain-language theorem explainer
The theorem states that phasePeriod at dimension 11 equals 7381. Researchers verifying the growth of synchronization costs for odd dimensions beyond 3 would cite this explicit value when tabulating lcm(2^D, T(D²)). The proof is a direct native computation of the triangular number T(121).
Claim. $T(11^2) = 7381$, where $T(n) = n(n+1)/2$ is the nth triangular number and phasePeriod$(D) := T(D^2)$.
background
The SyncMinimization module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). Here phasePeriod D is defined as T(D²) with T the triangular-number function. Upstream, T appears as the fundamental period in Breath1024, while phasePeriod itself is the local definition T(D * D). For odd D the value T(D²) remains odd, guaranteeing coprimality with the power-of-two period 2^D.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of phasePeriod at input 11.
why it matters
This evaluation supplies the concrete phasePeriod value for D = 11 in the sequence used to demonstrate that D = 3 yields the global minimum sync period (360 versus 7381 for D = 11). It supports the paper's claim that the eight-tick octave 2^D combined with the triangular number T(D²) selects D = 3. No downstream theorems depend on this specific instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.