cycles_of_eight
plain-language theorem explainer
The ratio of the full period to the eight-tick period equals the gap factor. Researchers closing the T8 step of the forcing chain cite this when showing how the eight-tick octave produces the integer 45. The proof is a direct native_decide evaluation that computes the division from the module definitions of full_period and eight_tick_period.
Claim. $P / T_8 = g$, where $P$ is the full period length, $T_8$ is the eight-tick period, and $g$ is the gap factor (the 9th triangular number).
background
The Gap45.Derivation module derives the integer 45 from the eight-tick structure forced by T8 together with the Fibonacci sequence. The eight_tick_period is defined as the integer 8, the content of T7: the period equals $2^D$ for $D=3$ spatial dimensions, requiring eight distinct states in a non-degenerate cycle. The full_period is the encompassing period whose ratio to eight_tick_period yields the gap; the module states that this gap equals $(8+1)×5$, equivalently the triangular number $T(9)=45$ that accumulates phase over one closed eight-tick cycle plus return.
proof idea
The proof is a term-mode one-liner that applies the native_decide tactic. This evaluates the arithmetic expression full_period / eight_tick_period directly against the gap constant using the concrete definitions supplied in the module and its eight_tick_period import.
why it matters
The declaration supplies the algebraic closure for the gap factor 45 inside the Gap45 derivation. It feeds the module's claim that 45 arises as closure_factor × fibonacci_factor and, via lcm(8,45)=360, forces $D=3$. The result sits at the T8 landmark of the unified forcing chain and supports the physical reading of 45 as cumulative phase accumulation over the ledger cycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.