IndisputableMonolith.Verification.DimensionCRT

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Bands
   3
   4/-(
   5Dimension forcing via CRT logic (8↔45 hinge)
   6
   7Reframe: the minimal period 2^D co‑synchronizes with the 45‑fold structure
   8only at 360. Conclude the only D with lcm(2^D, 45) = 360 (respecting atomic
   9ledger periods) is D = 3.
  10)-/
  11
  12namespace IndisputableMonolith
  13namespace Verification
  14namespace DimensionCRT
  15
  16open Nat
  17
  18/-- Synchronization period used in dimensional rigidity arithmetic: `S(D) = lcm(2^D,45)`. -/
  19def syncPeriod (D : ℕ) : ℕ := Nat.lcm (2 ^ D) 45
  20
  21/-- Closed form of the synchronization period: since `45` is odd, `gcd(2^D,45)=1`. -/
  22theorem syncPeriod_eq_mul (D : ℕ) : syncPeriod D = (2 ^ D) * 45 := by
  23  unfold syncPeriod
  24  have h2 : Nat.Coprime 2 45 := by decide
  25  have h : Nat.Coprime (2 ^ D) 45 := h2.pow_left D
  26  simpa using h.lcm_eq_mul
  27
  28/-- Unique minimization statement for synchronization:
  29among all `D ≥ 3`, `S(D)` is minimized at `D = 3`. -/
  30theorem syncPeriod_minimized_at_three {D : ℕ} (hD : 3 ≤ D) :
  31    syncPeriod 3 ≤ syncPeriod D ∧ (syncPeriod D = syncPeriod 3 → D = 3) := by
  32  constructor
  33  · have h3 : syncPeriod 3 = (2 ^ 3) * 45 := syncPeriod_eq_mul 3
  34    have hD' : syncPeriod D = (2 ^ D) * 45 := syncPeriod_eq_mul D
  35    rcases Nat.exists_eq_add_of_le hD with ⟨k, rfl⟩
  36    have hk : 1 ≤ 2 ^ k := Nat.one_le_pow k 2 (by norm_num)
  37    have hpow : 2 ^ 3 ≤ 2 ^ (3 + k) := by
  38      calc
  39        2 ^ 3 = 2 ^ 3 * 1 := by ring
  40        _ ≤ 2 ^ 3 * 2 ^ k := Nat.mul_le_mul_left (2 ^ 3) hk
  41        _ = 2 ^ (3 + k) := by simp [Nat.pow_add]
  42    have hmul : (2 ^ 3) * 45 ≤ (2 ^ (3 + k)) * 45 := by
  43      have : 45 * (2 ^ 3) ≤ 45 * (2 ^ (3 + k)) := Nat.mul_le_mul_left 45 hpow
  44      simpa [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using this
  45    simpa [h3, hD', Nat.add_assoc] using hmul
  46  · intro heq
  47    rcases Nat.exists_eq_add_of_le hD with ⟨k, rfl⟩
  48    cases k with
  49    | zero =>
  50        simp
  51    | succ k =>
  52        have hlt : 3 < 3 + Nat.succ k := Nat.lt_add_of_pos_right (Nat.succ_pos _)
  53        have hpowlt : 2 ^ 3 < 2 ^ (3 + Nat.succ k) :=
  54          Nat.pow_lt_pow_right (by decide : 1 < (2 : Nat)) hlt
  55        have h3 : syncPeriod 3 = (2 ^ 3) * 45 := syncPeriod_eq_mul 3
  56        have hD' : syncPeriod (3 + Nat.succ k) = (2 ^ (3 + Nat.succ k)) * 45 :=
  57          syncPeriod_eq_mul (3 + Nat.succ k)
  58        have hmul : syncPeriod 3 < syncPeriod (3 + Nat.succ k) := by
  59          have : 45 * (2 ^ 3) < 45 * (2 ^ (3 + Nat.succ k)) :=
  60            (Nat.mul_lt_mul_left (by decide : 0 < 45)).2 hpowlt
  61          have : (2 ^ 3) * 45 < (2 ^ (3 + Nat.succ k)) * 45 := by
  62            simpa [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using this
  63          simpa [h3, hD'] using this
  64        exfalso
  65        exact (Nat.ne_of_lt hmul) (heq.symm)
  66
  67/-- Numeric witness for the synchronization minimum. -/
  68theorem syncPeriod_3_eq_360 : syncPeriod 3 = 360 := by
  69  native_decide
  70
  71/-- Chinese‑remainder style dimension forcing: only D=3 satisfies
  72    lcm(2^D, 45) = 360. This packages the 8↔45 hinge as an arithmetic lemma. -/
  73theorem lcm_pow2_45_forces_D3 (D : ℕ)
  74    (h : Nat.lcm (2 ^ D) 45 = 360) : D = 3 := by
  75  -- Reuse the canonical equivalence provided by the RS stack.
  76  exact (IndisputableMonolith.RecogSpec.lcm_pow2_45_eq_iff D).mp h
  77
  78/-- Equivalence form convenient for automation. -/
  79theorem lcm_pow2_45_eq_360_iff (D : ℕ) :
  80    Nat.lcm (2 ^ D) 45 = 360 ↔ D = 3 :=
  81  IndisputableMonolith.RecogSpec.lcm_pow2_45_eq_iff D
  82
  83end DimensionCRT
  84end Verification
  85end IndisputableMonolith
  86