From 1946c1d1e7b00de3987d0ceb4cc89223883c3261 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 06:46:03 +0000 Subject: [PATCH] =?UTF-8?q?refactor(lean):=20ProductSidon=20=E2=80=94=20sn?= =?UTF-8?q?ake=5Fcase=20names,=20remove=20redundant=20heq',=20congrArg?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per Gemini review: - productSidon_injective → product_sidon_injective - isProductSidon_iff_crossDiffDisjoint → is_product_sidon_iff_cross_diff_disjoint - sidonPartition_implies_productSidon → sidon_partition_implies_product_sidon - isProductSidon_symm → is_product_sidon_symm - Drop redundant `heq'` in product_sidon_injective and sidon_partition_implies_product_sidon - Replace `congr_arg` with idiomatic Lean 4 `congrArg` Co-Authored-By: Claude Sonnet 4.6 Claude-Session: https://claude.ai/code/session_01Xrttjg3619VRrMjxqUPUkL --- .../Semantics/Semantics/ProductSidon.lean | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean index da0c283d..66076c3e 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/ProductSidon.lean @@ -39,9 +39,9 @@ as each other. The Sidon uniqueness condition *is* the decentralization invarian ## Relation to existing infrastructure - `sidon_diff_injective` (E8Sidon §8): differences within a *single* Sidon set are - injective. `productSidon_injective` extends this to *cross*-differences between + injective. `product_sidon_injective` extends this to *cross*-differences between two sets. -- `sidonPartition_implies_productSidon`: if a Sidon set is partitioned into two +- `sidon_partition_implies_product_sidon`: if a Sidon set is partitioned into two disjoint blocks used as encoding ranges, the cross-difference condition holds automatically. -/ @@ -73,13 +73,12 @@ def CrossDiffDisjoint (α : X → ℤ) (β : Y → ℤ) : Prop := This is the key equation: `α(x₁) + β(y₁) = α(x₂) + β(y₂)` implies `x₁ = x₂` and `y₁ = y₂`. -/ -theorem productSidon_injective +theorem product_sidon_injective (α : X → ℤ) (β : Y → ℤ) (hα : Function.Injective α) (hβ : Function.Injective β) (hdisj : CrossDiffDisjoint α β) : IsProductSidon α β := by intro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩ heq - have heq' : α x₁ + β y₁ = α x₂ + β y₂ := heq have hdiff : α x₁ - α x₂ = β y₂ - β y₁ := by linarith have hαeq : α x₁ = α x₂ := hdisj x₁ x₂ y₁ y₂ hdiff have hβeq : β y₁ = β y₂ := by linarith @@ -87,7 +86,7 @@ theorem productSidon_injective /-- The equivalence: `IsProductSidon` iff `CrossDiffDisjoint` (given injective encodings). -/ -theorem isProductSidon_iff_crossDiffDisjoint +theorem is_product_sidon_iff_cross_diff_disjoint (α : X → ℤ) (β : Y → ℤ) (hα : Function.Injective α) (hβ : Function.Injective β) : IsProductSidon α β ↔ CrossDiffDisjoint α β := by @@ -95,8 +94,8 @@ theorem isProductSidon_iff_crossDiffDisjoint · intro hinj x₁ x₂ y₁ y₂ hdiff have heq : α x₁ + β y₁ = α x₂ + β y₂ := by linarith have hpair : (x₁, y₁) = (x₂, y₂) := hinj heq - exact congr_arg α (Prod.ext_iff.mp hpair).1 - · exact productSidon_injective α β hα hβ + exact congrArg α (Prod.ext_iff.mp hpair).1 + · exact product_sidon_injective α β hα hβ /-! ## Bridge from Sidon sets -/ @@ -107,7 +106,7 @@ theorem isProductSidon_iff_crossDiffDisjoint *Proof*: Sidon says `α(x₁) + β(y₁) = α(x₂) + β(y₂)` implies `{α(x₁), β(y₁)} = {α(x₂), β(y₂)}`. Since `A ∩ B = ∅`, we cannot have `α(x₁) = β(y₂)` (different parts), so `α(x₁) = α(x₂)` and `β(y₁) = β(y₂)`. -/ -theorem sidonPartition_implies_productSidon +theorem sidon_partition_implies_product_sidon (S A B : Finset ℤ) (hS : IsSidonSet S) (hAB_union : A ∪ B = S) @@ -119,14 +118,13 @@ theorem sidonPartition_implies_productSidon (hβ_inj : Function.Injective β) : IsProductSidon α β := by intro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩ heq - have heq' : α x₁ + β y₁ = α x₂ + β y₂ := heq -- All four values lie in S have hαx₁S : α x₁ ∈ S := hAB_union ▸ Finset.mem_union_left B (hα_range x₁) have hβy₁S : β y₁ ∈ S := hAB_union ▸ Finset.mem_union_right A (hβ_range y₁) have hαx₂S : α x₂ ∈ S := hAB_union ▸ Finset.mem_union_left B (hα_range x₂) have hβy₂S : β y₂ ∈ S := hAB_union ▸ Finset.mem_union_right A (hβ_range y₂) -- Apply the Sidon property - rcases hS (α x₁) hαx₁S (β y₁) hβy₁S (α x₂) hαx₂S (β y₂) hβy₂S heq' with + rcases hS (α x₁) hαx₁S (β y₁) hβy₁S (α x₂) hαx₂S (β y₂) hβy₂S heq with (⟨h1, h2⟩ | ⟨h1, h2⟩) · -- Case 1: α x₁ = α x₂ ∧ β y₁ = β y₂ → done by injectivity exact Prod.ext (hα_inj h1) (hβ_inj h2) @@ -183,7 +181,7 @@ theorem atmosphere_app_eq /-- Product-Sidon is symmetric: if `(α, β)` is product-Sidon, then so is `(β, α)`. (Swapping host and app roles doesn't break injectivity.) -/ -theorem isProductSidon_symm (α : X → ℤ) (β : Y → ℤ) +theorem is_product_sidon_symm (α : X → ℤ) (β : Y → ℤ) (h : IsProductSidon α β) : IsProductSidon β α := by intro ⟨y₁, x₁⟩ ⟨y₂, x₂⟩ heq have heq' : α x₁ + β y₁ = α x₂ + β y₂ := by linarith