phasePeriod_odd_5
The declaration shows that the phase period for dimension 5 is odd. Researchers verifying the dimensional rigidity constraint would cite it to confirm coprimality between the power-of-two octave and the triangular number T(D²) when D is odd. The argument reduces to a single native computation that evaluates T(25) and checks divisibility by 2.
claim$2$ does not divide the triangular number $T(25)$, where $T(n)=n(n+1)/2$.
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²)). Here phasePeriod D is defined as the triangular number T(D²). The upstream definition phasePeriod supplies the map D ↦ T(D²) used throughout the module. For odd D the triangular number T(D²) is itself odd, which forces gcd(2^D, T(D²)) = 1 and therefore full coprimality of the two periods.
proof idea
The proof is a one-line wrapper that invokes native_decide to evaluate phasePeriod 5 directly and confirm the result is not divisible by 2.
why it matters in Recognition Science
The result supplies the concrete oddness check for D = 5 that the module uses to contrast with the minimal case D = 3 (where T(9) = 45). It therefore supports the claim that only odd dimensions produce the full coprimality required by the synchronization-minimization argument, with D = 3 yielding the smallest lcm value of 360. The declaration aligns with the eight-tick octave generalization (T7) in the Recognition Science forcing chain.
scope and limits
- Does not prove the general statement that T(D²) is odd for every odd D.
- Does not compute the numerical value of the synchronization period lcm(2^D, T(D²)).
- Does not address even dimensions or the partial alignment that occurs when T(D²) is even.
formal statement (Lean)
70theorem phasePeriod_odd_5 : ¬ 2 ∣ phasePeriod 5 := by native_decide