full_period
plain-language theorem explainer
The full period is defined as the least common multiple of the eight-tick period and the gap. Researchers tracing the Recognition Science derivation of spatial dimensions from the T7-T8 forcing chain cite this as the synchronization interval that closes the structure. The definition applies Nat.lcm directly to the two upstream periods.
Claim. Let $P$ denote the full synchronization period, defined by $P = {lcm}(T_8, G)$ where $T_8 = 8$ is the eight-tick period and $G = 45$ is the gap obtained as the product of the closure factor and the Fibonacci factor.
background
In the Gap45.Derivation module the eight-tick period is fixed at 8, matching the period forced by T7 (eight-tick octave) for three spatial dimensions. The gap is defined as the product of the closure factor (one full cycle plus return) and the Fibonacci factor (Fibonacci(5)), yielding 45. The module derives this gap from the eight-tick structure combined with the Fibonacci sequence tied to phi. Upstream results establish eight_tick_period = 8 in StillnessGenerative and Gravity.EightTickResonance, confirming the equality to 2^3.
proof idea
This is a one-line definition that applies the Nat.lcm operation to eight_tick_period and gap. No tactics or lemmas are invoked inside the declaration itself; the numerical identity lcm(8,45)=360 is recorded in the attached comment and discharged in downstream theorems.
why it matters
The definition supplies the full period used by cycles_of_eight, cycles_of_gap, full_period_eq_360, and D_3_forced_from_structure. It completes the chain that produces the 360-day synchronization interval from the eight-tick period (T7) and the 45-gap (T8), thereby forcing D=3. The construction touches the open question of how the phi-ladder and Fibonacci sequence together enforce the dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.