gap_45_as_sum
plain-language theorem explainer
The declaration verifies that the sum of integers from 1 to 9 equals 45, supplying a direct numerical check for the ninth triangular number in the 45-tick synchronization argument. Researchers closing the physical motivation gap for the dimension-forcing chain would cite it when equating cumulative phase to the closure of an 8-tick cycle. The proof is a one-line wrapper that applies native_decide to evaluate the list sum directly.
Claim. $1 + 2 + 3 + 4 + 5 + 6 + 7 + 8 + 9 = 45$
background
The module supplies a physically grounded derivation of the number 45 for the dimension-forcing argument. It treats 45 as the ninth triangular number T(9), defined by the upstream result T(n) = n(n+1)/2. In the 8-tick framework the cycle is not closed by itself; a closure step yields nine steps total, so cumulative phase over the closed cycle equals the triangular sum T(9).
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the sum of List.range 10 minus zero.
why it matters
It supplies the numerical identity that anchors the cumulative-phase step in the Gap45 physical-motivation module, directly addressing the paper's noted gap for the 45-tick synchronization. The result sits inside the eight-tick octave (T8) and the D=3 forcing chain, where the closure from 8 to 9 ticks produces the triangular accumulation. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.