gap
plain-language theorem explainer
The gap is defined as the product of the closure factor (eight-tick period plus one) and the Fibonacci factor (5). Researchers deriving the 45-gap from the eight-tick octave and phi-ladder in Recognition Science cite this definition to link T8 to cumulative phase. The definition is a direct algebraic product of the two upstream factor definitions.
Claim. Define the gap to be the product of the closure factor and the Fibonacci factor, where the closure factor equals the eight-tick period plus one and the Fibonacci factor equals 5.
background
The Gap45.Derivation module shows that 45 emerges from the eight-tick structure (T8) combined with the Fibonacci sequence related to phi. The closure factor is defined as eight_tick_period + 1, representing one full cycle plus return. The Fibonacci factor is defined as 5, the smallest Fibonacci number greater than 1 that is coprime with 8.
proof idea
This is a direct definition that multiplies the closure_factor and fibonacci_factor. It follows immediately from the upstream factor definitions without additional lemmas or tactics.
why it matters
This definition supplies the numerical value 45 that feeds downstream certificates such as visualBeautyCert and potterySerialCert. It fills the key result of the 45-Gap Derivation module, where 45 = T(9) from the eight-tick period and closure principle. In the framework it supports forcing D = 3 via lcm(8, 45) = 360.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.