IndisputableMonolith.Physics.WEndoForcing

   1import Mathlib
   2import IndisputableMonolith.Constants.AlphaDerivation
   3
   4/-!
   5# W_endo Forcing: W = E_pass + F = 17 if and only if D = 3
   6
   7The endogenous wallpaper count W_endo(D) = passive_field_edges(D) + cube_faces(D)
   8equals 17 if and only if D = 3. This is the paper's Tr7 argument.
   9
  10## The Proof
  11
  12W_endo(D) = (D · 2^(D-1) - 1) + 2D = D · 2^(D-1) + 2D - 1
  13
  14- D = 1: W_endo = 1·1 + 2 - 1 = 2 ≠ 17
  15- D = 2: W_endo = 2·2 + 4 - 1 = 7 ≠ 17
  16- D = 3: W_endo = 3·4 + 6 - 1 = 17 ✓
  17- D ≥ 4: W_endo ≥ 4·8 + 8 - 1 = 39 > 17
  18
  19This is pure arithmetic, fully decidable by case analysis.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Physics
  24namespace WEndoForcing
  25
  26open Constants.AlphaDerivation
  27
  28/-- The endogenous wallpaper count: E_passive + F for a D-cube. -/
  29def W_endo (d : ℕ) : ℕ := passive_field_edges d + cube_faces d
  30
  31/-- At D = 3: W_endo = 11 + 6 = 17. -/
  32theorem W_endo_at_3 : W_endo 3 = 17 := by native_decide
  33
  34/-- W_endo(3) matches the wallpaper groups constant. -/
  35theorem W_endo_eq_wallpaper : W_endo 3 = wallpaper_groups := by native_decide
  36
  37/-- W_endo(1) = 2 ≠ 17. -/
  38theorem W_endo_at_1 : W_endo 1 = 2 := by native_decide
  39
  40/-- W_endo(2) = 7 ≠ 17. -/
  41theorem W_endo_at_2 : W_endo 2 = 7 := by native_decide
  42
  43/-- For D = 4: W_endo = 39. -/
  44theorem W_endo_at_4 : W_endo 4 = 39 := by native_decide
  45
  46/-- For D = 5: W_endo = 89. -/
  47theorem W_endo_at_5 : W_endo 5 = 89 := by native_decide
  48
  49/-- For D ≥ 4, W_endo(D) > 17. Proved by showing W_endo(4) = 39 > 17
  50    and W_endo is increasing (since D·2^(D-1) dominates). -/
  51theorem W_endo_gt_17_of_ge_4 (d : ℕ) (hd : 4 ≤ d) : 17 < W_endo d := by
  52  have h4 : W_endo 4 = 39 := W_endo_at_4
  53  suffices W_endo 4 ≤ W_endo d by linarith
  54  unfold W_endo passive_field_edges cube_edges active_edges_per_tick cube_faces
  55  have hpow : 2 ^ 3 ≤ 2 ^ (d - 1) := Nat.pow_le_pow_right (by norm_num) (by omega)
  56  have hmul : 4 * 2 ^ 3 ≤ d * 2 ^ (d - 1) := by
  57    calc 4 * 2 ^ 3 ≤ d * 2 ^ 3 := by nlinarith
  58      _ ≤ d * 2 ^ (d - 1) := Nat.mul_le_mul_left d hpow
  59  omega
  60
  61/-- **THE KEY THEOREM**: W_endo(D) = 17 if and only if D = 3.
  62    This is the paper's Tr7 — dimension selection via the cube sum. -/
  63theorem W_endo_eq_17_iff (d : ℕ) (hd : 1 ≤ d) : W_endo d = 17 ↔ d = 3 := by
  64  constructor
  65  · intro h
  66    match d, hd with
  67    | 1, _ => simp [W_endo_at_1] at h
  68    | 2, _ => simp [W_endo_at_2] at h
  69    | 3, _ => rfl
  70    | 4, _ => simp [W_endo_at_4] at h
  71    | d + 5, _ =>
  72      have : 4 ≤ d + 5 := by omega
  73      have := W_endo_gt_17_of_ge_4 (d + 5) this
  74      omega
  75  · intro h; subst h; exact W_endo_at_3
  76
  77/-- Uniqueness: D = 3 is the unique positive dimension with W_endo = 17. -/
  78theorem dimension_unique_from_W_endo :
  79    ∃! d : ℕ, 1 ≤ d ∧ W_endo d = 17 := by
  80  use 3
  81  constructor
  82  · exact ⟨by norm_num, W_endo_at_3⟩
  83  · intro d ⟨hd, hw⟩
  84    exact (W_endo_eq_17_iff d hd).mp hw
  85
  86/-- The decomposition: W = E_pass + F at D = 3. -/
  87theorem W_decomposition :
  88    W_endo 3 = passive_field_edges 3 + cube_faces 3 := rfl
  89
  90/-- Verify the components. -/
  91theorem components_at_D3 :
  92    passive_field_edges 3 = 11 ∧ cube_faces 3 = 6 := by
  93  constructor <;> native_decide
  94
  95end WEndoForcing
  96end Physics
  97end IndisputableMonolith
  98