phasePeriod_odd_11
phasePeriod_odd_11 establishes that the phase period at dimension 11 is odd. Researchers formalizing the dimensional rigidity argument in Recognition Science cite it to confirm that T(D²) remains odd for odd D, preserving coprimality with 2^D. The proof is a one-line native computation that directly evaluates T(121) and checks its parity.
claimThe triangular number $T(121)$ is odd, i.e., $2$ does not divide $T(121)$.
background
In this module the synchronization period for dimension D is defined as lcm(2^D, T(D²)), where T(n) denotes the nth triangular number. The upstream definition phasePeriod(D) := T(D * D) supplies the second argument of the lcm. For odd D the triangular number T(D²) is itself odd, so gcd(2^D, T(D²)) = 1 and the periods remain fully coprime. The module uses this fact to compare sync periods across odd dimensions and isolate D = 3 as the unique minimizer.
proof idea
The proof is a one-line native_decide wrapper. It evaluates the concrete value of phasePeriod 11 = T(121) = 7381 and confirms that the result is odd by direct arithmetic reduction.
why it matters in Recognition Science
The declaration supplies a concrete data point for the coprimality claim that underpins the selection of 45 as the minimal sync period in the Dimensional Rigidity paper. It verifies the odd-D parity pattern for D = 11, consistent with the general argument that only odd dimensions keep T(D²) coprime with the 8-tick octave. No downstream theorems yet invoke this specific instance.
scope and limits
- Does not prove the general statement that T(D²) is odd for every odd D.
- Does not compute or compare the full lcm synchronization periods.
- Does not reference J-cost, defect distance, or the phi-ladder.
- Does not address even dimensions or the reduction in gcd for even D.
formal statement (Lean)
73theorem phasePeriod_odd_11 : ¬ 2 ∣ phasePeriod 11 := by native_decide
proof body
Term-mode proof.
74
75/-! ## Coprimality with 2^D -/
76