phasePeriod_even_10
Researchers on dimensional rigidity cite this to confirm that even D yields an even T(D²), allowing partial alignment between the 2^D and triangular periods. It supplies one concrete data point in the argument that only odd dimensions achieve full coprimality and that D=3 therefore minimizes the synchronization period. The proof is a one-line native decision that evaluates the triangular number directly.
claimThe triangular number $T(100)$ is even, i.e., $2$ divides $T(100)$ where $T(n) = n(n+1)/2$.
background
The SyncMinimization module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D=3 uniquely minimizes lcm(2^D, T(D²)). For even D the periods partially align because T(D²) is even; only odd D produces coprimality. The triangular number is defined locally by T(n) := n(n+1)/2 and the phase period by phasePeriod(D) := T(D*D). Upstream results supply the period concept via the T abbreviation in Breath1024 and the concrete phasePeriod definition in the same module.
proof idea
The proof is a one-line term that invokes native_decide on the predicate 2 ∣ phasePeriod 10.
why it matters in Recognition Science
This instance illustrates the even-D case that reduces the uncomputability barrier via gcd(2^D, T(D²)) > 1. It feeds the parent claim that D=3 alone minimizes the sync period at 360 among odd dimensions. The module connects directly to the eight-tick octave generalized to 2^D and the selection of D=3 as the unique minimizer.
scope and limits
- Does not prove the general parity claim for arbitrary even D.
- Does not compute the lcm synchronization period itself.
- Does not address uniqueness among odd dimensions.
- Does not supply a closed-form formula for T(D²) parity.
formal statement (Lean)
66theorem phasePeriod_even_10 : 2 ∣ phasePeriod 10 := by native_decide
proof body
Term-mode proof.
67
68/-- For odd D, T(D²) is odd. -/