phasePeriod_11
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 in Recognition Science
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.
scope and limits
- Does not derive a closed-form expression for phasePeriod at arbitrary D.
- Does not compute the full synchronization period lcm(2^11, 7381).
- Does not compare phase periods across a range of dimensions.
- Does not address physical or empirical realizability for D = 11.
formal statement (Lean)
59@[simp] theorem phasePeriod_11 : phasePeriod 11 = 7381 := by native_decide
proof body
Term-mode proof.
60
61/-- For even D, T(D²) is even: no coprimality with 2^D. Verified for D ∈ {2,4,6,8,10}. -/