phasePeriod_odd_7
plain-language theorem explainer
The declaration establishes that the phase period for dimension 7 is odd. Researchers verifying coprimality in the synchronization-period minimization for odd spatial dimensions would cite this instance when checking the general pattern for D greater than or equal to 3. The proof proceeds by direct native computation of the triangular number T(49).
Claim. The triangular number $T(49)$ is odd: $2$ does not divide $T(49)$.
background
phasePeriod(D) is defined as the triangular number T(D²). 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 odd D the quantity T(D²) is itself odd, guaranteeing coprimality with the power-of-two factor 2^D. The upstream definition phasePeriod computes T(D * D) for any natural number D.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate phasePeriod 7 directly and confirm the result is not divisible by 2.
why it matters
This instance supports the broader claim that odd D yields full coprimality between 2^D and T(D²), which is required for the unique minimization at D = 3 (sync period 360). It instantiates the eight-tick octave generalization to 2^D within the Recognition Science forcing chain. The parent argument is the Dimensional Rigidity paper (Washburn/Zlatanović/Allahyarov, 2026).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.