Gap45 Derivation Full Period Is Product

The synchronization period

The number 360 is familiar from degrees in a circle, but it also appears as the smallest number that two other counting cycles can both divide evenly. If one cycle repeats every 8 steps and another every 45 steps, the two realign only after 360 steps, since 360 is the least common multiple of 8 and 45. The theorem full_period_is_product in the framework's machine-checked library of formal theorems states this fact in a compact form: the full period equals the product of the two cycle lengths, so 360 = 8 × 45.

The statement is a pure arithmetic identity, and it is proved by direct computation. The framework defines an eight-step period, a gap of 45, and a full period as their least common multiple. The theorem then verifies that this least common multiple is exactly the product, which holds because 8 and 45 share no common factor greater than 1. A companion theorem confirms the same relationship from the other direction: dividing the full period by the gap gives the eight-step period, and dividing by the eight-step period gives the gap.

In Recognition Science, this identity is not an isolated curiosity. The framework derives the eight-step period from its earlier results, and it derives the gap of 45 from that period together with a Fibonacci factor. The number 45 itself factors as (8 + 1) × 5, where the 9 represents one full eight-step cycle plus a return to the starting state, and the 5 is the fourth Fibonacci number. The product identity then ties these two derived quantities into a single synchronization period of 360.

The theorem does not claim that 360 has any physical meaning on its own. It establishes only the arithmetic relationship between the three defined quantities. The framework does use the number 360 in a further step: it shows that the equation lcm(2^D, 45) = 360 has exactly one solution for a natural number D, namely D = 3. That step connects the arithmetic to the framework's account of three spatial dimensions, but it is a separate theorem with its own conditions.

/-- 360 = 8 × 45 (since gcd(8, 45) = 1). -/
theorem full_period_is_product : full_period = eight_tick_period * gap := by
  native_decide

/-- The full synchronization period. -/
def full_period : ℕ := Nat.lcm eight_tick_period gap

/-- 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 theorem does not assign any physical meaning to the number 360 by itself. The theorem does not prove that three spatial dimensions exist; that is a separate theorem with its own conditions. The theorem does not claim that the Fibonacci factor 5 is the only possible choice for the gap's second factor.

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: