From 7518de684905bdc14e37cb5643a04defe65b5127 Mon Sep 17 00:00:00 2001 From: allaun Date: Wed, 17 Jun 2026 02:41:10 -0500 Subject: [PATCH] feat: goormaghtigh_finite_search now proven via native_decide on nested quantifiers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .../Semantics/SpherionTwinPrime.lean | 96 +++++++++++++++---- 1 file changed, 77 insertions(+), 19 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean b/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean index 290f23af..2cef601a 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean +++ b/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