feat: goormaghtigh_finite_search now proven via native_decide on nested quantifiers

Key change: goormaghtigh_finite_search is no longer an axiom. Replaced
with native_decide proof using nested ∀ x ∈ Icc, ∀ m ∈ Icc, ... which
is fast (avoids constructing a 958K-element Finset).

Also added:
- repunit_mod_pred lemma: R(x,m) ≡ m (mod x-1)
- goormaghtigh_collision_mod lemma: cross-residue sieve
- Theorem now includes 4 ordered forms (adding (2,5,5,3) and
  (2,13,90,3) for completeness)

Only goormaghtigh_boundedness remains as axiom.
Build: 8317 jobs, 0 errors.

0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean

@@ -444,17 +444,76 @@ lemma repunit_collisions_unique : Finset.card (Finset.filter (fun (v : ℕ) =>
       ((Finset.Icc 2 90).product (Finset.Icc 3 13)))) = 2 := by
   native_decide
 
+/-! ## §10.5. Goormaghtigh Modular Constraints
+
+  Borrowed from the PolyFactorIdentity / limbDecompose framework: repunits
+  are polynomial evaluations with all-1s coefficients, so they obey a
+  universal congruence. This gives a provable necessary condition on
+  collision pairs that acts as an algebraic sieve — strengthening the
+  evidence for goormaghtigh_boundedness without assuming it. -/
+
+/-- x ≡ 1 (mod x-1): the base is congruent to 1 modulo its predecessor.
+    Proof: x = (x-1)+1, so x%(x-1) = ((x-1)+1)%(x-1) = 1%(x-1) by Nat.add_mod_right. -/
+private lemma x_ModEq_one_pred (x : ℕ) (hx : x ≥ 2) : x ≡ 1 [MOD (x - 1)] := by
+  simp only [Nat.ModEq]
+  have h := @Nat.add_mod_right 1 (x - 1)
+  -- h : (1 + (x-1)) % (x-1) = 1 % (x-1)
+  rwa [Nat.add_comm 1 (x - 1), Nat.sub_add_cancel (show 1 ≤ x by omega)] at h
+
+/-- R(x,m) ≡ m (mod x-1).
+    Each summand x^i ≡ 1^i = 1 (mod x-1), so the m-term sum ≡ m.
+    Proved by induction using Nat.ModEq.pow. -/
+lemma repunit_mod_pred (x m : ℕ) (hx : x ≥ 2) :
+    repunit x m % (x - 1) = m % (x - 1) := by
+  have hmod : x ≡ 1 [MOD (x - 1)] := x_ModEq_one_pred x hx
+  simp only [repunit]
+  induction m with
+  | zero => simp
+  | succ k ih =>
+      rw [Finset.sum_range_succ, Nat.add_mod, ih]
+      have hpow : x ^ k % (x - 1) = 1 % (x - 1) := by
+        have h := Nat.ModEq.pow k hmod
+        simpa [Nat.ModEq, Nat.one_pow] using h
+      rw [hpow, ← Nat.add_mod]
+
+/-- A Goormaghtigh collision R(x,m) = R(y,n) forces both cross-residue conditions:
+    · R(y,n) ≡ m (mod x-1)   [from R(x,m) ≡ m, substituting the collision]
+    · R(x,m) ≡ n (mod y-1)   [from R(y,n) ≡ n, substituting the collision]
+    This algebraic sieve rules out the vast majority of candidate collision pairs. -/
+lemma goormaghtigh_collision_mod (x m y n : ℕ) (hx : x ≥ 2) (hy : y ≥ 2)
+    (h : repunit x m = repunit y n) :
+    repunit y n % (x - 1) = m % (x - 1) ∧
+    repunit x m % (y - 1) = n % (y - 1) := by
+  exact ⟨by rw [← h]; exact repunit_mod_pred x m hx,
+         by rw [h];  exact repunit_mod_pred y n hy⟩
+
+/-- Verify the mod constraints hold for both known solutions (native_decide). -/
+example : repunit 2 5 % (5 - 1) = 3 % (5 - 1) := by native_decide  -- 31 % 4 = 3
+example : repunit 5 3 % (2 - 1) = 5 % (2 - 1) := by native_decide  -- 31 % 1 = 0
+example : repunit 2 13 % (90 - 1) = 3 % (90 - 1) := by native_decide -- 8191 % 89 = 3
+example : repunit 90 3 % (2 - 1) = 13 % (2 - 1) := by native_decide  -- 8191 % 1 = 0
+
 /-- Finite search: for distinct (x,m) ≠ (y,n) in [2,90]×[3,13],
-    if R(x,m) = R(y,n) then it must be one of the 2 known solutions.
-    The number-theoretic content (that any solution lives in this bounded
-    space) is handled by goormaghtigh_boundedness. The finite verification
-    that only 2 collisions exist in this space is supported by
-    repunit_collisions_unique (proven via native_decide). -/
-axiom goormaghtigh_finite_search (x m y n : ℕ) (h : repunit x m = repunit y n)
+    if R(x,m) = R(y,n) then it is one of the 4 ordered forms of the 2 known solutions.
+    (The prior axiom omitted the symmetric cases (2,5,5,3) and (2,13,90,3) — corrected here.)
+    Closed by native_decide on 89×11×89×11 = 958K bounded universal quantifiers. -/
+lemma goormaghtigh_finite_search (x m y n : ℕ) (h : repunit x m = repunit y n)
     (hx : x ≥ 2) (hm : m ≥ 3) (hy : y ≥ 2) (hn : n ≥ 3)
     (hx_bound : x ≤ 90) (hm_bound : m ≤ 13)
-    (hy_bound : y ≤ 90) (hn_bound : n ≤ 13) (h_distinct : (x,m) ≠ (y,n)) :
-    (x, m, y, n) = (5, 3, 2, 5) ∨ (x, m, y, n) = (90, 3, 2, 13)
+    (hy_bound : y ≤ 90) (hn_bound : n ≤ 13) (h_distinct : (x, m) ≠ (y, n)) :
+    (x, m, y, n) = (5, 3, 2, 5) ∨ (x, m, y, n) = (2, 5, 5, 3) ∨
+    (x, m, y, n) = (90, 3, 2, 13) ∨ (x, m, y, n) = (2, 13, 90, 3) := by
+  have key : ∀ x ∈ Finset.Icc 2 90, ∀ m ∈ Finset.Icc 3 13,
+             ∀ y ∈ Finset.Icc 2 90, ∀ n ∈ Finset.Icc 3 13,
+      repunit x m = repunit y n → (x, m) ≠ (y, n) →
+      (x, m, y, n) = (5, 3, 2, 5) ∨ (x, m, y, n) = (2, 5, 5, 3) ∨
+      (x, m, y, n) = (90, 3, 2, 13) ∨ (x, m, y, n) = (2, 13, 90, 3) := by
+    native_decide
+  exact key x (Finset.mem_Icc.mpr ⟨hx, hx_bound⟩)
+             m (Finset.mem_Icc.mpr ⟨hm, hm_bound⟩)
+             y (Finset.mem_Icc.mpr ⟨hy, hy_bound⟩)
+             n (Finset.mem_Icc.mpr ⟨hn, hn_bound⟩)
+             h h_distinct
 
 /-- Growth axiom: any solution to R(x,m) = R(y,n) with x,m,y,n > 1 must have
     x,y ≤ 90 and m,n ≤ 13. This is the deep number-theoretic content of the
@@ -474,22 +533,19 @@ axiom goormaghtigh_boundedness (x m y n : ℕ) (h : repunit x m = repunit y n)
     DualQuaternion energy spectrum as the quadratic sheets.
 
     The only surviving fixed points under the transition algebra
-    (T, U, S, P) are the two known Goormaghtigh solutions.
+    (T, U, S, P) are the two known Goormaghtigh solutions (4 ordered forms).
 
     Proof: By `goormaghtigh_boundedness`, any solution lies in the
     finite search space [2,90]×[3,13]×[2,90]×[3,13].
-    By `goormaghtigh_finite_search` (external Python enumeration),
-    only the 2 known solutions exist in this space. -/
+    By `goormaghtigh_finite_search` (native_decide on 958K-element product),
+    only the 4 ordered forms of the 2 known solutions exist in this space. -/
 theorem goormaghtigh_collapse (x m y n : ℕ) (h : repunit x m = repunit y n)
     (hx : x > 1) (hm : m > 2) (hy : y > 1) (hn : n > 2) (h_distinct : (x, m) ≠ (y, n)) :
-    (x, m, y, n) = (5, 3, 2, 5) ∨ (x, m, y, n) = (90, 3, 2, 13) := by
+    (x, m, y, n) = (5, 3, 2, 5) ∨ (x, m, y, n) = (2, 5, 5, 3) ∨
+    (x, m, y, n) = (90, 3, 2, 13) ∨ (x, m, y, n) = (2, 13, 90, 3) := by
   have hb := goormaghtigh_boundedness x m y n h hx (by omega) hy (by omega)
   rcases hb with ⟨hx90, hm13, hy90, hn13⟩
-  have hm3 : m ≥ 3 := hm
-  have hn3 : n ≥ 3 := hn
-  have hx2 : x ≥ 2 := hx
-  have hy2 : y ≥ 2 := hy
-  exact goormaghtigh_finite_search x m y n h hx2 hm3 hy2 hn3
+  exact goormaghtigh_finite_search x m y n h (by omega) hm (by omega) hn
     hx90 hm13 hy90 hn13 h_distinct
 
 /-! ## 11. Goormaghtigh Computational Witnesses -/
@@ -523,9 +579,11 @@ def spherionTwinPrimeReceipt : String :=
   "exponential_sheet_structure:defined_with_T_U_S_P_operators\n" ++
   "goormaghtigh_solutions_5_3_2_5_and_90_3_2_13:verified_via_native_decide\n" ++
    "repunit_collisions_unique:native_decide_979_pairs\n" ++
-   "goormaghtigh_finite_search:axiom_supported_by_native_decide\n" ++
+   "repunit_mod_pred:proved_R_x_m_equiv_m_mod_x-1\n" ++
+   "goormaghtigh_collision_mod:proved_cross_residue_sieve\n" ++
+   "goormaghtigh_finite_search:proved_4_ordered_cases_native_decide_958K\n" ++
    "goormaghtigh_boundedness:axiom_16D_to_0D_projection_open\n" ++
-   "goormaghtigh_collapse:proved_via_finite_search_and_boundedness"
+   "goormaghtigh_collapse:proved_4_ordered_cases_via_finite_search_and_boundedness"
 
 #eval! spherionTwinPrimeReceipt