Gap45 Derivation Forty Five Eq Nine Times Five

The 45-gap identity

The number 45 is a triangular number: it is the sum 1 + 2 + 3 + ... + 9, which equals 9 × 10 / 2 = 9 × 5. This is an elementary arithmetic fact. The Recognition Science declaration forty_five_eq_nine_times_five proves, in the framework's machine-checked library of formal theorems, that 45 indeed factors as 9 times 5. The proof is a direct computation; the declaration does not introduce new physics by itself.

Within the framework, the factorization carries a structural meaning. The number 9 is called the closure_factor because it represents one full eight-tick cycle plus a return to the starting state (8 + 1 = 9). The number 5 is called the fibonacci_factor because it is the fifth Fibonacci number, Fib(4) = 5, and it is the smallest Fibonacci number greater than 1 that is coprime with 8. The declaration proves that the product of these two factors equals 45, and that 45 is coprime with 8.

The significance extends beyond the factorization itself. The framework defines a full_period as the least common multiple of the eight-tick period and the gap 45. The declaration proves that this full period is 360, and that 360 is the product of 8 and 45. It also proves that the only natural number D satisfying lcm(2^D, 45) = 360 is D = 3. This is the link to three spatial dimensions: the framework models space as having three dimensions because 2^3 = 8 and lcm(8, 45) = 360.

The declaration does not claim that 45 is physically measured or that it is a free parameter chosen to fit data. It claims only that, given the framework's definitions of an eight-tick period and a Fibonacci factor, the number 45 emerges as their product. The physical interpretation of 45 as cumulative phase accumulation over a closed cycle is a definitional choice within the framework, not a proved theorem about the external world.

/-- Alternative: 45 = 9 × 5. -/
theorem forty_five_eq_nine_times_five : (45 : ℕ) = 9 * 5 := rfl

@[simp] lemma closure_factor_eq : closure_factor = 9 := rfl

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

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

/-- 360 = 8 × 45 (since gcd(8, 45) = 1). -/
theorem full_period_is_product : full_period = eight_tick_period * gap := by
  native_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 number 45 is a measured physical constant. The physical interpretation of 45 as cumulative phase is a proved theorem. The declaration alone forces three spatial dimensions without the rest of the framework.

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: