Verification Dimension Crt

Dimension arithmetic

The Chinese remainder theorem is a classical tool for solving systems of modular congruences. In this framework, a related arithmetic idea appears under the name verification dimension crt: it packages the counting of dimensions into a single least-common-multiple calculation. The module defines a synchronization period S(D) = lcm(2^D, 45), where lcm is the least common multiple of two numbers. For a given dimension D, this period records how often two counting cycles, one based on powers of two and one based on 45, come back into step.

The classical Chinese remainder theorem, known since Sunzi in the third century, guarantees a unique solution to certain modular systems when the moduli are coprime. Here the same idea applies to the numbers 2^D and 45. Because 45 is odd, it shares no factor with any power of two, so the least common multiple is simply their product: S(D) = (2^D) * 45. That closed form is proved directly in the machine-checked library of formal theorems.

The key result is a minimization. Among all dimensions D at least 3, the synchronization period S(D) is smallest when D = 3, and no other dimension ties it. At D = 3 the period equals 360, since 2^3 = 8 and 8 * 45 = 360. The module proves this uniqueness in two ways: a general inequality showing S(3) is the minimum, and a numeric witness confirming the value 360. The arithmetic then forces the dimension: if lcm(2^D, 45) = 360, then D must be 3.

In Recognition Science, this lemma acts as a hinge. It connects the framework's eight-tick recognition cycle, which supplies the factor 8, to the number 45 that appears elsewhere in the forcing chain. The result is that the same arithmetic that governs synchronization also selects three spatial dimensions. The module does not itself derive the eight-tick cycle or the factor 45; it takes those as inputs and shows that their least common multiple pins the dimension uniquely. The physical bridge from recognition to spatial geometry remains a separate open target.

The consequence is compact and checkable: a single number, 360, encodes the dimensional choice. A reader who wants to verify the framework's claim about three dimensions can inspect this arithmetic directly, without tracing the longer forcing chain. The lemma reduces a structural claim to a computation any student of number theory can repeat by hand.

/-- Closed form of the synchronization period: since `45` is odd, `gcd(2^D,45)=1`. -/
theorem syncPeriod_eq_mul (D : ℕ) : syncPeriod D = (2 ^ D) * 45 := by
  unfold syncPeriod
  have h2 : Nat.Coprime 2 45 := by decide
  have h : Nat.Coprime (2 ^ D) 45 := h2.pow_left D
  simpa using h.lcm_eq_mul

/-- Unique minimization statement for synchronization:
among all `D ≥ 3`, `S(D)` is minimized at `D = 3`. -/
theorem syncPeriod_minimized_at_three {D : ℕ} (hD : 3 ≤ D) :
    syncPeriod 3 ≤ syncPeriod D ∧ (syncPeriod D = syncPeriod 3 → D = 3) := by
  constructor
  · have h3 : syncPeriod 3 = (2 ^ 3) * 45 := syncPeriod_eq_mul 3
    have hD' : syncPeriod D = (2 ^ D) * 45 := syncPeriod_eq_mul D
    rcases Nat.exists_eq_add_of_le hD with ⟨k, rfl⟩
    have hk : 1 ≤ 2 ^ k := Nat.one_le_pow k 2 (by norm_num)
    have hpow : 2 ^ 3 ≤ 2 ^ (3 + k) := by
      calc
        2 ^ 3 = 2 ^ 3 * 1 := by ring
        _ ≤ 2 ^ 3 * 2 ^ k := Nat.mul_le_mul_left (2 ^ 3) hk
        _ = 2 ^ (3 + k) := by simp [Nat.pow_add]
    have hmul : (2 ^ 3) * 45 ≤ (2 ^ (3 + k)) * 45 := by
      have : 45 * (2 ^ 3) ≤ 45 * (2 ^ (3 + k)) := Nat.mul_le_mul_left 45 hpow
      simpa [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using this
    simpa [h3, hD', Nat.add_assoc] using hmul
  · intro heq
    rcases Nat.exists_eq_add_of_le hD with ⟨k, rfl⟩
    cases k with
    | zero =>
        simp
    | succ k =>
        have hlt : 3 < 3 + Nat.succ k := Nat.lt_add_of_pos_right (Nat.succ_pos _)
        have hpowlt : 2 ^ 3 < 2 ^ (3 + Nat.succ k) :=
          Nat.pow_lt_pow_right (by decide : 1 < (2 : Nat)) hlt
        have h3 : syncPeriod 3 = (2 ^ 3) * 45 := syncPeriod_eq_mul 3
        have hD' : syncPeriod (3 + Nat.succ k) = (2 ^ (3 + Nat.succ k)) * 45 :=
          syncPeriod_eq_mul (3 + Nat.succ k)
        have hmul : syncPeriod 3 < syncPeriod (3 + Nat.succ k) := by
          have : 45 * (2 ^ 3) < 45 * (2 ^ (3 + Nat.succ k)) :=
            (Nat.mul_lt_mul_left (by decide : 0 < 45)).2 hpowlt
          have : (2 ^ 3) * 45 < (2 ^ (3 + Nat.succ k)) * 45 := by
            simpa [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using this
          simpa [h3, hD'] using this
        exfalso
        exact (Nat.ne_of_lt hmul) (heq.symm)

/-- Numeric witness for the synchronization minimum. -/
theorem syncPeriod_3_eq_360 : syncPeriod 3 = 360 := by
  native_decide

/-- Chinese‑remainder style dimension forcing: only D=3 satisfies
    lcm(2^D, 45) = 360. This packages the 8↔45 hinge as an arithmetic lemma. -/
theorem lcm_pow2_45_forces_D3 (D : ℕ)
    (h : Nat.lcm (2 ^ D) 45 = 360) : D = 3 := by
  -- Reuse the canonical equivalence provided by the RS stack.
  exact (IndisputableMonolith.RecogSpec.lcm_pow2_45_eq_iff D).mp h

What this page does not claim

This module derives the eight-tick cycle or the factor 45 from first principles. The physical recognition-to-linking bridge for three spatial dimensions is proved here. The Chinese remainder theorem itself is introduced or proved in this module.

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/Verification/DimensionCRT.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: