Gap45 Derivation Forty Five Factorization

The 45 factorization

The number 45 is a common sight in geometry: a quarter of a half-turn, or one eighth of a full 360 degree rotation. Its prime factorization is 45 = 3 × 3 × 5, or 3² × 5. This is an elementary fact of arithmetic, true for any integer, and it is the starting point for a specific claim in the Recognition Science framework.

Within that framework, the number 45 is not just a geometric convenience. The framework's machine-checked library of formal theorems contains a declaration named forty_five_factorization, which proves exactly this arithmetic identity: 45 equals 3 squared times 5. The proof is a direct computation, verified by the library's checker. This is the full extent of what that single declaration establishes: a factorization of the integer 45.

The framework does not stop at the bare factorization. Other declarations in the same module build on it. They define a gap as the product of a closure factor (8 plus 1, or 9) and a Fibonacci factor (5), so the gap equals 45. They show that 45 is the ninth triangular number, the sum 1 + 2 + ... + 9, which represents cumulative phase over a closed cycle. They also prove that the least common multiple of 8 and 45 is 360, and that this equation forces the dimension D to be 3, since 2³ equals 8.

These surrounding results are separate theorems with their own proofs. The declaration forty_five_factorization itself establishes only the arithmetic fact. It does not, by itself, assert that 45 has any physical meaning, nor that it emerges from any deeper principle. The connection to eight-tick cycles, Fibonacci numbers, and three spatial dimensions is made by other declarations in the module, each with its own grounding.

What the reader can take away is a clear division of labor. The factorization is a proved, machine-checked statement about integers. The interpretation of that factorization within the framework is a separate, larger claim, built from additional theorems. The single declaration is a small, precise building block, not the whole story.

/-- 45's prime factorization: 3² × 5. -/
theorem forty_five_factorization : (45 : ℕ) = 3^2 * 5 := by 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⟩

/-- 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 declaration does not assert that 45 has any physical meaning on its own. The declaration does not prove that the factorization is unique or that 45 is special among integers. The connection to three spatial dimensions is established by other theorems, not by this single declaration.

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: