phasePeriod_odd_5
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.