refactor(lean): ProductSidon — snake_case names, remove redundant heq', congrArg

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Xrttjg3619VRrMjxqUPUkL

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