closure_factor_eq
plain-language theorem explainer
The lemma establishes that the closure factor equals nine, obtained directly as the eight-tick period plus one for return to the initial state. Researchers deriving the 45-gap from the eight-tick structure and Fibonacci sequence in Recognition Science reference this equality to factor the triangular number T(9). The proof is a one-line reflexivity that holds once the definition is substituted.
Claim. Let the closure factor be the eight-tick period plus one. Then the closure factor equals 9.
background
The Gap45.Derivation module shows that 45 arises from the eight-tick structure (T8) combined with the Fibonacci sequence tied to phi. The closure factor is introduced as eight_tick_period + 1, standing for one full cycle plus return. Its upstream definition states: 'The closure factor: one full cycle plus return.' This sits inside the forcing chain where T7 fixes the eight-tick octave of period 8 and T8 forces three spatial dimensions.
proof idea
The proof is a term-mode reflexivity. After the definition closure_factor := eight_tick_period + 1 is substituted, the right-hand side evaluates to 9 by direct computation.
why it matters
This equality supplies the factor 9 in the module's key identity 45 = closure_factor times fibonacci_factor, which links the eight-tick period to cumulative phase accumulation T(9). It supports the later claim that lcm(8, 45) = 360 forces D = 3. The result fills the algebraic step connecting T8 to the triangular-number representation of closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.