phasePeriod_odd_9
The theorem establishes that the phase period for dimension 9 is odd. Researchers working on dimensional rigidity and synchronization minimization in Recognition Science cite it to confirm coprimality of T(81) with 2^9 in the lcm calculation. The result supports the claim that only odd D yields full period separation. The proof proceeds by direct evaluation of the triangular number via native_decide.
claim$¬ 2 ∣ T(81)$, where $T(n) = n(n+1)/2$ denotes the nth triangular number.
background
The 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²)). For dimension D the 8-tick period generalizes to 2^D while the parity matrix of the hypercube Q_D has D² entries, so the cumulative phase is the triangular number T(D²). phasePeriod D is defined as T(D * D). For odd D, T(D²) is odd, ensuring gcd(2^D, T(D²)) = 1.
proof idea
The proof is a direct computation that evaluates phasePeriod 9 = T(81) and checks divisibility by 2 using native_decide.
why it matters in Recognition Science
This declaration verifies the oddness of T(81) for D=9, which is required to show that only odd dimensions produce full coprimality and that D=3 yields the minimal sync period of 360. It fills the concrete check inside the uniqueness argument for D=3 among odd dimensions and connects to the eight-tick octave (T8) and D=3 spatial dimensions in the forcing chain. No downstream uses are recorded yet.
scope and limits
- Does not prove that T(D²) is odd for every odd D.
- Does not compute the lcm or the full synchronization period value.
- Does not compare minimization across even dimensions.
- Does not address the general case for arbitrary D.
formal statement (Lean)
72theorem phasePeriod_odd_9 : ¬ 2 ∣ phasePeriod 9 := by native_decide