From 95077cb0d08756f15e07649338178f6d5b7d74f4 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Wed, 17 Jun 2026 02:57:13 -0500
Subject: [PATCH] feat: upgrade 2 axioms to full theorems

- exists_covered_ge: proved (construct (a,b)=(n+1,1) with obstruction 7n+8)
- unbounded_iff_infinite: proved (via Set.Finite.exists_finset)
- Added Fintype deriving to SheetSignature
- goormaghtigh_boundedness remains the single axiom (open conjecture)

Build: 8317 jobs, 0 errors.
---
 .../Semantics/SpherionTwinPrime.lean          | 78 +++++++++++++++++--
 1 file changed, 73 insertions(+), 5 deletions(-)

diff --git a/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean b/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean
index 2cef601a..729b182a 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/SpherionTwinPrime.lean
@@ -39,7 +39,7 @@ inductive SheetSignature : Type where
   | pm : SheetSignature  -- (+,-): 6ab + a - b
   | mp : SheetSignature  -- (-,+): 6ab - a + b
   | mm : SheetSignature  -- (-,-): 6ab - a - b
-deriving DecidableEq, Repr
+deriving DecidableEq, Repr, Fintype
 
 instance : Fintype SheetSignature :=
   { elems := {.pp, .pm, .mp, .mm}
@@ -201,9 +201,43 @@ def tunedWitnessRegion (polarity : Q16_16) : Set ℕ :=
     The merged, deduplicated sequence of all obstruction values is the algorithmic
     core of the sieve. -/
 
-/-- Axiom: every integer n has some covered integer ≥ n (the 4 sheets produce
-    infinitely many distinct values). -/
-axiom exists_covered_ge (n : ℕ) : ∃ k ≥ n, coverageDensity k > 0
+/-- Every integer n has some covered integer ≥ n (the 4 sheets produce
+    infinitely many distinct values). Proof: (a,b) = (n+1,1) on sheet (+,+)
+    gives obstruction 6·(n+1)·1 + (n+1) + 1 = 7n + 8, which is ≥ n and covered. -/
+lemma exists_covered_ge (n : ℕ) : ∃ k ≥ n, coverageDensity k > 0 := by
+  set k := 7*n + 8 with hk
+  have hk_ge_n : k ≥ n := by omega
+  have h_covered : coverageDensity k > 0 := by
+    unfold coverageDensity
+    -- (a,b) = (n+1,1) on SheetSignature.pp gives obstruction = 6·(n+1)·1 + (n+1) + 1 = 7n + 8 = k
+    set a := n + 1 with ha
+    have ha1 : a ≥ 1 := by omega
+    have ha_k1 : a ≤ k + 1 := by
+      have : 7*n + 8 ≥ n + 1 := by omega
+      omega
+    have h_obstruction : obstruction a 1 SheetSignature.pp = k := by
+      unfold obstruction; dsimp [a, k]; ring
+    -- Use nested Finset.product for the 3D search space
+    let sheetSet : Finset SheetSignature := {SheetSignature.pp, SheetSignature.pm, SheetSignature.mp, SheetSignature.mm}
+    let searchSpace : Finset (ℕ × ℕ × SheetSignature) :=
+      (Finset.Icc 1 (k+1)).product ((Finset.Icc 1 (k+1)).product sheetSet)
+    have h_mem : (a, 1, SheetSignature.pp) ∈ searchSpace := by
+      dsimp [searchSpace, sheetSet]
+      refine Finset.mem_product.mpr ⟨Finset.mem_Icc.mpr ⟨ha1, ha_k1⟩, ?_⟩
+      have h1_ge_1 : (1 : ℕ) ≥ 1 := by omega
+      have h1_le_k1 : (1 : ℕ) ≤ k + 1 := by
+        dsimp [k]
+        omega
+      refine Finset.mem_product.mpr ⟨Finset.mem_Icc.mpr ⟨h1_ge_1, h1_le_k1⟩, ?_⟩
+      simp
+    have h_filter : (a, 1, SheetSignature.pp) ∈
+      Finset.filter (fun ((a',b',s) : ℕ × ℕ × SheetSignature) => obstruction a' b' s = k) searchSpace :=
+      Finset.mem_filter.mpr ⟨h_mem, h_obstruction⟩
+    have h_card_pos : (Finset.filter (fun ((a',b',s) : ℕ × ℕ × SheetSignature) => obstruction a' b' s = k)
+      searchSpace).card > 0 :=
+      Finset.card_pos.mpr ⟨(a,1,SheetSignature.pp), h_filter⟩
+    exact h_card_pos
+  exact ⟨k, hk_ge_n, h_covered⟩
 
 /--
   The merged obstruction sequence: all covered integers in increasing order,
@@ -382,7 +416,41 @@ theorem covered_8 : (8 : ℕ) ∉ witnessRegion := by
 
   Unbounded witnesses is equivalent to infinitely many witnesses.
 -/
-axiom unbounded_iff_infinite : unboundedWitnesses ↔ Set.Infinite witnessRegion
+lemma unbounded_iff_infinite : unboundedWitnesses ↔ Set.Infinite witnessRegion := by
+  constructor
+  · intro hunb
+    intro hfin
+    have ⟨fs, hfs⟩ := hfin.exists_finset
+    -- fs : Finset ℕ, hfs : ∀ a, a ∈ fs ↔ a ∈ witnessRegion
+    have hmax : ∃ (M : ℕ), ∀ w, w ∈ witnessRegion → w ≤ M := by
+      by_cases h_empty : fs = ∅
+      · refine ⟨0, λ w hw => ?_⟩
+        have : w ∈ fs := (hfs w).mpr hw
+        rw [h_empty] at this
+        simp at this
+      · have h_nonempty : fs.Nonempty := Finset.nonempty_iff_ne_empty.mpr h_empty
+        refine ⟨fs.max' h_nonempty, λ w hw => ?_⟩
+        have hw_fs : w ∈ fs := (hfs w).mpr hw
+        exact Finset.le_max' fs w hw_fs
+    rcases hmax with ⟨M, hM⟩
+    rcases hunb M with ⟨w, hw, hw_gt⟩
+    have hw_le_M := hM w hw
+    omega
+  · intro hinf
+    intro N
+    by_cases h : ∀ w, w ∈ witnessRegion → w ≤ N
+    · have h_finite : Set.Finite witnessRegion := by
+        have h_sub : witnessRegion ⊆ (Finset.range (N+1) : Set ℕ) :=
+          λ w hw => Finset.mem_coe.mpr (Finset.mem_range.mpr (by
+            have hw_le_N := h w hw
+            omega))
+        have h_fin_range : Set.Finite (Finset.range (N+1) : Set ℕ) :=
+          Finset.finite_toSet _
+        exact Set.Finite.subset h_fin_range h_sub
+      exact absurd h_finite hinf
+    · push_neg at h
+      rcases h with ⟨w, hw, hw_gt⟩
+      exact ⟨w, hw, hw_gt⟩
 
 /-! ## 10. Goormaghtigh Exponential Sheets