phasePeriod_9
The phase period for dimension nine equals the triangular number T(81) which evaluates to 3321. Researchers comparing synchronization costs lcm(2^D, T(D²)) across odd dimensions D ≥ 3 would cite this concrete value when checking the D=9 case against the D=3 minimum. The proof is a direct numerical evaluation of the definition via native computation.
claimphasePeriod(9) = T(81) = 3321 where T(n) = n(n+1)/2 is the nth triangular number and phasePeriod(D) := T(D²).
background
The Gap45 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²)). phasePeriod is defined upstream as phasePeriod(D) := T(D * D), with T the triangular number. For D=9 this yields T(81), and the module lists the resulting sync periods: 360 for D=3, 10400 for D=5, and 156800 for D=7.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate phasePeriod 9 directly from its definition.
why it matters in Recognition Science
This supplies the explicit T(81)=3321 needed to obtain the D=9 sync period in the minimization argument of the module. It supports the claim that D=3 yields the smallest period of 360, thereby explaining why T(9)=45 is selected. The result sits inside the eight-tick octave generalization to 2^D and the coprimality argument for odd D.
scope and limits
- Does not prove a closed-form expression for phasePeriod(D) at arbitrary D.
- Does not compute or compare the lcm synchronization periods themselves.
- Does not address even dimensions or the general coprimality claim.
formal statement (Lean)
58@[simp] theorem phasePeriod_9 : phasePeriod 9 = 3321 := by native_decide