coprime_7
The coprimality of 128 and the triangular number T(49) is asserted to confirm that the synchronization period for dimension 7 does not collapse. Researchers formalizing dimensional rigidity would cite it when comparing odd D values to isolate the D=3 minimum. The proof reduces to direct native computation of the gcd.
claim$gcd(2^7, T(49)) = 1$ where $T(n) = n(n+1)/2$ is the triangular number.
background
phasePeriod D computes the triangular number T(D²) with T(n) = n(n+1)/2. The module develops the synchronization period as lcm(2^D, phasePeriod D) and shows this quantity is minimized at D=3 among odd dimensions D ≥ 3 because T(D²) remains odd precisely when D is odd, yielding full coprimality with 2^D.
proof idea
A one-line wrapper applies the native_decide tactic to evaluate the coprimality predicate by direct computation of the gcd of 128 and 1225.
why it matters in Recognition Science
The declaration supports the argument that only odd dimensions preserve coprime periods under the generalization of the eight-tick octave to 2^D, reinforcing why D=3 uniquely minimizes the synchronization period to 360. It supplies the D=7 case in the explicit comparison of odd dimensions given in the module documentation. No downstream theorems depend on it.
scope and limits
- Does not prove coprimality for arbitrary odd dimensions.
- Does not compute the lcm or the minimal synchronization period.
- Does not address even dimensions or connect to the J-cost or phi-ladder.
formal statement (Lean)
79theorem coprime_7 : Nat.Coprime (2^7) (phasePeriod 7) := by native_decide