From b65ef756ca4c86b391ba4f0f6bd6aa29cec096b6 Mon Sep 17 00:00:00 2001 From: allaun Date: Fri, 3 Jul 2026 15:19:47 -0500 Subject: [PATCH] fix(StrandCapacityBound): repair proofs + register in lakefile MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Registering required it to actually compile (it did not). Fixes: - capacity_bound_grid was FALSE at L₁=0 or L₂=0 (empty grid, nonempty image) and its `norm_num : 0 < (L₁:ℤ)` could not prove positivity of a variable. Added `0 < L₁, 0 < L₂` hypotheses; threaded through capacity_bound and chiral_capacity_bound. - mathlib name drift: emod_nonneg/emod_lt → Int.emod_nonneg (b ≠ 0) / Int.emod_lt_of_pos; Finset.card_Ico → Int.card_Ico; Finset.card_le_card_of_subset → Finset.card_le_card; Finset.image_subset → Finset.image_subset_iff.mpr. - replaced a `#eval` (broke on ℤ's noncomputable order instance) and its WRONG expected value (claimed 4 over {1..6}, actually 6) with two kernel-checked `decide` witnesses: {1,2,5,6}→4 (the Sidon set) and Ico 1 7→6. - registered CoreFormalism.StrandCapacityBound in lakefile. Verified: lake build OK (links into SilverSightFormal), #print axioms = {propext, Classical.choice, Quot.sound} (no sorryAx, no custom axiom), anti-smuggle --ci clean. Co-Authored-By: Claude Opus 4.8 --- formal/CoreFormalism/StrandCapacityBound.lean | 34 +++++++++++-------- lakefile.lean | 1 + 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/formal/CoreFormalism/StrandCapacityBound.lean b/formal/CoreFormalism/StrandCapacityBound.lean index de7eb70e..69d165de 100644 --- a/formal/CoreFormalism/StrandCapacityBound.lean +++ b/formal/CoreFormalism/StrandCapacityBound.lean @@ -43,33 +43,33 @@ Bound 2: the codomain grid has size L₁·L₂. Each residue lies in [0, L₁) resp. [0, L₂), so at most L₁ × L₂ distinct pairs are reachable regardless of |A|. -/ -theorem capacity_bound_grid (A : Finset ℤ) : +theorem capacity_bound_grid (A : Finset ℤ) (hL₁ : 0 < L₁) (hL₂ : 0 < L₂) : (A.image (strandPair L₁ L₂ S)).card ≤ (L₁ : ℕ) * L₂ := by + have hL₁' : (0 : ℤ) < (L₁ : ℤ) := by exact_mod_cast hL₁ + have hL₂' : (0 : ℤ) < (L₂ : ℤ) := by exact_mod_cast hL₂ -- The grid of possible residues let grid : Finset (ℤ × ℤ) := (Finset.Ico 0 (L₁ : ℤ)) ×ˢ (Finset.Ico 0 (L₂ : ℤ)) have hgrid : grid.card = (L₁ : ℕ) * L₂ := by - simp [grid, Finset.card_product, Finset.card_Ico, Nat.cast_inj] + simp [grid, Finset.card_product, Int.card_Ico] -- Every strand pair lands in the grid have hmem : ∀ a : ℤ, strandPair L₁ L₂ S a ∈ grid := by intro a have hx : a % (L₁ : ℤ) ∈ Finset.Ico 0 (L₁ : ℤ) := by - have hnonneg : 0 ≤ a % (L₁ : ℤ) := emod_nonneg a (by norm_num : 0 < (L₁ : ℤ)) - have hlt : a % (L₁ : ℤ) < (L₁ : ℤ) := emod_lt a (by norm_num : 0 < (L₁ : ℤ)) + have hnonneg : 0 ≤ a % (L₁ : ℤ) := Int.emod_nonneg a (ne_of_gt hL₁') + have hlt : a % (L₁ : ℤ) < (L₁ : ℤ) := Int.emod_lt_of_pos a hL₁' exact Finset.mem_Ico.mpr ⟨hnonneg, hlt⟩ have hy : ((S : ℤ) - a) % (L₂ : ℤ) ∈ Finset.Ico 0 (L₂ : ℤ) := by have hnonneg' : 0 ≤ ((S : ℤ) - a) % (L₂ : ℤ) := - emod_nonneg _ (by norm_num : 0 < (L₂ : ℤ)) + Int.emod_nonneg _ (ne_of_gt hL₂') have hlt' : ((S : ℤ) - a) % (L₂ : ℤ) < (L₂ : ℤ) := - emod_lt _ (by norm_num : 0 < (L₂ : ℤ)) + Int.emod_lt_of_pos _ hL₂' exact Finset.mem_Ico.mpr ⟨hnonneg', hlt'⟩ exact Finset.mem_product.mpr ⟨hx, hy⟩ -- Image is subset of grid, so cardinality bounded by grid cardinality calc (A.image (strandPair L₁ L₂ S)).card ≤ grid.card := - Finset.card_le_card_of_subset (Finset.image_subset _ (by - intro a ha - exact hmem a)) + Finset.card_le_card (Finset.image_subset_iff.mpr (fun a _ => hmem a)) _ = (L₁ : ℕ) * L₂ := hgrid /-- @@ -78,20 +78,24 @@ Combined bound: |F(A)| ≤ min(|A|, L₁·L₂). For a single strand with chirality (2 orientations per pair), the full capacity is min(|A|, L₁·L₂) × 2. -/ -theorem capacity_bound (A : Finset ℤ) : +theorem capacity_bound (A : Finset ℤ) (hL₁ : 0 < L₁) (hL₂ : 0 < L₂) : (A.image (strandPair L₁ L₂ S)).card ≤ min A.card ((L₁ : ℕ) * L₂) := by apply le_min · exact capacity_bound_input L₁ L₂ S A - · exact capacity_bound_grid L₁ L₂ S A + · exact capacity_bound_grid L₁ L₂ S A hL₁ hL₂ /-- With chirality: each pair can be read in 2 orders (identity, reflection) or (reflection, identity), corresponding to σᵢ vs σᵢ⁻¹ in the braid group. -/ -theorem chiral_capacity_bound (A : Finset ℤ) : +theorem chiral_capacity_bound (A : Finset ℤ) (hL₁ : 0 < L₁) (hL₂ : 0 < L₂) : (A.image (strandPair L₁ L₂ S)).card * 2 ≤ min A.card ((L₁ : ℕ) * L₂) * 2 := by - nlinarith [capacity_bound L₁ L₂ S A] + nlinarith [capacity_bound L₁ L₂ S A hL₁ hL₂] -#eval ((Finset.Ico 1 7).image (strandPair 3 4 7)).card --- Expected: 4 (Sidon example A={1,2,5,6} with moduli 3,4, S=7) +-- Sidon example A = {1,2,5,6} with moduli 3,4, S=7 → image has 4 distinct pairs: +-- 1↦(1,2), 2↦(2,1), 5↦(2,2), 6↦(0,1). Kernel-checked (`decide`, not +-- `#eval`/`native_decide`), sidestepping ℤ's noncomputable order instance. +example : (({1, 2, 5, 6} : Finset ℤ).image (strandPair 3 4 7)).card = 4 := by decide +-- Full range Ico 1 7 = {1,…,6} instead gives 6 distinct pairs (all injective here): +example : ((Finset.Ico (1 : ℤ) 7).image (strandPair 3 4 7)).card = 6 := by decide diff --git a/lakefile.lean b/lakefile.lean index f7f9b668..8182cfd1 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -44,6 +44,7 @@ lean_lib «SilverSightFormal» where `CoreFormalism.HachimojiManifoldAxiom, `CoreFormalism.ChentsovFinite, `CoreFormalism.HopfFibration, + `CoreFormalism.StrandCapacityBound, `SilverSight.AngrySphinx, `SilverSight.CollatzBraid, `SilverSight.GoldenSpiral,