dimension_forcing
plain-language theorem explainer
The theorem verifies that the three-dimensional octave period of 8 ticks shares a least common multiple of 360 with the 45-tick triangular closure. Researchers closing the dimension-forcing argument in Recognition Science would cite this arithmetic synchronization when linking the eight-tick structure to cumulative phase neutrality. The proof is a one-line term-mode wrapper that splits the conjunction and delegates both equalities to native_decide.
Claim. $2^3 = 8$ and the least common multiple of the 8-tick octave period with the 45-tick triangular number equals 360.
background
The module supplies the physical motivation for the 45 appearing in the dimension-forcing chain. It treats 45 as the ninth triangular number T(9) = 9(10)/2, obtained by summing the first nine positive integers. This sum arises once the 8-tick cycle (the fundamental evolution period from 2^D) is closed by one additional step, giving nine positions in total. The upstream tick definition supplies the RS-native time quantum whose multiples generate both the octave and the cumulative phase ledger.
proof idea
The proof is a term-mode one-line wrapper. Constructor splits the conjunction into two goals; native_decide then reduces both 2^3 = 8 and Nat.lcm 8 45 = 360 to decidable arithmetic and discharges them.
why it matters
The result supplies the arithmetic closure required by the Gap45 synchronization argument that forces D = 3. It sits inside the T7–T8 segment of the unified forcing chain, where the eight-tick octave must share a common period with the triangular cumulative phase before spatial dimensionality is fixed. The declaration therefore discharges the concrete numerical claim left open by the paper’s remark on the physically unmotivated 45-tick step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.