Gap45 Derivation Fibonacci Factor Coprime With 8

The coprime factor

The Fibonacci sequence begins 1, 1, 2, 3, 5, 8, 13, where each term is the sum of the two before it. The number 5 is the fourth term in this sequence, and the number 8 is the fifth. Two numbers are coprime when their greatest common divisor is 1, meaning they share no prime factors. The number 5 is coprime with 8 because 5 is prime and 8 is a power of 2.

The declaration fibonacci_factor_coprime_with_8 establishes exactly this fact in a machine-checked library of formal theorems. It proves that the greatest common divisor of the Fibonacci factor, defined as 5, and the number 8 is 1. This is a simple, exact statement verified by direct computation, not a conjecture or an approximation.

Within the Recognition Science framework, this coprime relationship is a small but necessary piece of a larger argument. The framework models a recognition cycle with eight ticks, and it defines a gap value as the product of a closure factor (8 plus 1, or 9) and the Fibonacci factor (5). The product is 45. The proof that 5 and 8 are coprime helps show that the least common multiple of 8 and 45 is 360, a full synchronization period. This period, in turn, is used in the framework's derivation of three spatial dimensions.

The theorem does not claim that the number 5 is the only Fibonacci number coprime with 8, nor does it claim that the Fibonacci factor is uniquely determined by this property. It also does not assert that the number 45 is physically meaningful outside the framework's own model. The proof is a statement about the arithmetic of two specific integers, and its role in the wider derivation is an interpretation within the framework, not a theorem about the physical world.

/-- 5 is coprime with 8. -/
theorem fibonacci_factor_coprime_with_8 : Nat.gcd fibonacci_factor 8 = 1 := by
  simp [fibonacci_factor]

/-- The gap is forced by eight-tick and Fibonacci structure. -/
theorem gap_forced_from_eight_tick_and_fibonacci :
    gap = closure_factor * fibonacci_factor ∧
    closure_factor = eight_tick_period + 1 ∧
    fibonacci_factor = fib 4 := by
  exact ⟨rfl, rfl, rfl⟩

/-- **Main Theorem**: The gap equals 45. -/
@[simp] theorem gap_eq_45 : gap = 45 := rfl

/-- **Key Result**: lcm(8, 45) = 360. -/
@[simp] theorem full_period_eq_360 : full_period = 360 := by
  simp [full_period, eight_tick_period, gap]
  decide

/-- lcm(2^D, 45) = 360 only when D = 3. -/
theorem lcm_360_forces_D_eq_3 :
    ∀ D : ℕ, Nat.lcm (2^D) 45 = 360 ↔ D = 3 := by
  intro D
  constructor
  · intro h
    have hgcd : Nat.gcd (2 ^ D) 45 = 1 := by
      have hcop : Nat.Coprime 2 45 := by native_decide
      exact Nat.Coprime.pow_left D hcop
    have hlcm : Nat.lcm (2 ^ D) 45 = 2 ^ D * 45 / Nat.gcd (2 ^ D) 45 :=
      Nat.lcm_eq_mul_div (2 ^ D) 45
    have hlcm' : Nat.lcm (2 ^ D) 45 = 2 ^ D * 45 := by
      simpa [hgcd] using hlcm
    have hmul : 2 ^ D * 45 = 360 := by
      simpa [hlcm'] using h
    have h360 : (360 : ℕ) = 8 * 45 := by norm_num
    have h8eq : 2 ^ D = 8 := by
      apply Nat.mul_right_cancel (by norm_num : 0 < 45)
      simpa [h360] using hmul
    have hpow : 2 ^ D = 2 ^ 3 := by
      have h8 : (2 ^ 3 : ℕ) = 8 := by norm_num
      simpa [h8] using h8eq
    exact Nat.pow_right_injective (by norm_num : 1 < 2) hpow
  · intro hD
    subst hD
    native_decide

What this page does not claim

The theorem does not claim that 5 is the only Fibonacci number coprime with 8. The theorem does not claim that the Fibonacci factor is uniquely determined by its coprime property. The theorem does not assert that the number 45 is physically meaningful outside the framework's own model.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gap45/Derivation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: