Gap45 Derivation Fibonacci Factor Is Fib

The Fibonacci factor

The Fibonacci sequence begins 1, 1, 2, 3, 5, 8, 13, with each term the sum of the two before it. Its fourth term, counting from zero, is 5. The Recognition Science declaration fibonacci_factor_is_fib establishes, as a proved theorem in the framework's machine-checked library, that this number 5 is exactly the factor called fibonacci_factor in the derivation of the constant 45.

The context: the framework models reality as maintaining a discrete record of events, called a ledger. From its axioms it derives an eight-tick cycle, meaning eight steps cover the ledger. The derivation of 45 multiplies two factors: closure_factor, defined as 8 + 1 = 9 for returning to the start, and fibonacci_factor, defined as 5. The theorem states fibonacci_factor = fib 4, where fib 4 = 5. This is not an arbitrary choice: 5 is the smallest Fibonacci number greater than 1 that is coprime with 8, meaning it shares no common divisor with 8 other than 1.

The declaration is one step in a longer chain. The full period 360 = lcm(8, 45), and the framework proves that the only dimension D satisfying lcm(2^D, 45) = 360 is D = 3. So the Fibonacci factor participates in forcing three spatial dimensions, within the framework's account. The theorem itself is simple: it equates a defined constant with a Fibonacci term. Its significance lies in showing the number 5 in the factorization 45 = 9 × 5 is not plucked from nowhere but is the fourth Fibonacci number, a connection the framework's derivation exploits.

What the declaration does not claim: it does not prove that the Fibonacci sequence itself is fundamental to physics. It only identifies one factor in a derivation as a Fibonacci number. It does not claim the factorization 45 = 9 × 5 is unique or that other factorizations are impossible. It does not assert that the physical interpretation, that the ledger forces this structure, is proved; the theorem is a statement about natural numbers, not about empirical reality. The physical bridge from the ledger to observed three-dimensional space remains an open target in the framework, not a consequence of this single declaration.

/-- 5 is a Fibonacci number. -/
theorem fibonacci_factor_is_fib : fibonacci_factor = fib 4 := rfl

/-- Consecutive Fibonacci numbers are coprime.
    This is a classical result; we prove specific cases by computation. -/
theorem fib_coprime_4_5 : Nat.gcd (fib 4) (fib 5) = 1 := by 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

/-- 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⟩

What this page does not claim

This declaration does not prove that the Fibonacci sequence is physically fundamental. It does not claim the factorization 45 = 9 × 5 is the only possible one. It does not establish that the physical interpretation of the ledger forcing three dimensions is proved; that bridge remains open.

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: