closure_factor_eq
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not prove the physical motivation that 45 equals the ninth triangular number.
- Does not derive or verify the Fibonacci factor of 5.
- Does not compute lcm(8, 45) or the forcing of three dimensions.
- Does not address coprimality conditions with the eight-tick period.
formal statement (Lean)
83@[simp] lemma closure_factor_eq : closure_factor = 9 := rfl
proof body
Term-mode proof.
84
85/-- The Fibonacci factor: smallest Fibonacci > 1 coprime with 8. -/