cycles_of_gap
plain-language theorem explainer
The declaration shows that the number of gap cycles fitting inside one full period equals the eight-tick period. Researchers tracing how the 45-gap emerges from the eight-tick octave and Fibonacci factors cite this equality when closing the D=3 forcing argument. The proof is a single computational step via native_decide that verifies the numerical identity.
Claim. The number of gap cycles contained in the full period equals the eight-tick period: $P / g = T_8$, where $P$ denotes the full period, $g$ the gap length, and $T_8$ the eight-tick period.
background
The Gap45.Derivation module shows that 45 arises from the eight-tick structure (T8) together with the Fibonacci sequence linked to φ. The factorization given is 45 = (8 + 1) × 5, with closure factor 9 obtained by fence-post counting over one cycle plus return and Fibonacci factor 5 the smallest Fibonacci number coprime to 8. The full period is the least common multiple of 8 and 45, which equals 360; the gap in the present statement is therefore the 45-unit gap, so that the ratio yields exactly 8.
proof idea
The proof is a term-mode proof consisting of the single tactic native_decide. This tactic evaluates the division of the two period constants and confirms that the result matches the eight_tick_period constant already defined upstream.
why it matters
The result supplies the algebraic consistency step inside the Gap45 derivation. It supports the module claim that 45 = T(9) and that lcm(8, 45) = 360 together force D = 3 spatial dimensions. The equality therefore closes one link in the T7 eight-tick octave to T8 dimensional forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.