diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
index cf80ea4e..f2ecdf7b 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
@@ -207,6 +207,19 @@ theorem E4_sq_eq_E8_coeff (n : ℕ) (hn : 2 ≤ n) :
 -- §5. Sidon Set Basics
 -- ═══════════════════════════════════════════════════════════════════════════════
 
+/-- Dimensional annotation lemma (RRC-style classification):
+    Finset pair equality {a,b} = {c,d} classifies into exactly two shapes:
+    (a=c ∧ b=d) or (a=d ∧ b=c). This is the "vocabulary" for all Sidon
+    counting proofs — once this is established, cardinality bounds become
+    mechanical routing through the two shapes.
+    Uses Set.pair_eq_pair_iff via Finset.coe_pair coercion. -/
+private lemma finset_pair_eq_iff {a b c d : ℕ}
+    (h : ({a, b} : Finset ℕ) = {c, d}) :
+    (a = c ∧ b = d) ∨ (a = d ∧ b = c) := by
+  have hset : ({a, b} : Set ℕ) = {c, d} := by
+    rw [← Finset.coe_pair, ← Finset.coe_pair, Finset.coe_inj.mpr h]
+  exact Set.pair_eq_pair_iff.mp hset
+
 /-- A finite set S ⊆ ℕ is a Sidon set (B₂ set) if all pairwise sums a+b
     (with a ≤ b, both in S) are distinct. Equivalently, the sumset S+S
     has no repeated representations. -/
@@ -238,16 +251,35 @@ def additiveEnergy (S : Finset ℕ) : ℕ :=
   ((S ×ˢ S) ×ˢ (S ×ˢ S)).filter
     (fun ((a, b), (c, d)) => a + b = c + d) |>.card
 
-/-- Sidon sets have additive energy exactly 2|S|² - |S|. -/
+/-- Sidon sets have additive energy at most 2|S|².
+    Proof by RRC-style dimensional classification: finset_pair_eq_iff
+    routes every quadruple to shape "same" or "swap", each bounded by k². -/
 theorem sidon_energy_bound (S : Finset ℕ) (hS : IsSidonSet S) :
     additiveEnergy S ≤ 2 * S.card ^ 2 := by
-  -- TODO(lean-port): By Sidon, every (a,b,c,d) ∈ S⁴ with a+b=c+d has {a,b}={c,d}.
-  -- So (c,d) = (a,b) or (c,d) = (b,a). The filtered set ⊆ same_set ∪ swap_set,
-  -- each of which injects into S×S via Prod.fst (uniquely determined by first pair).
-  -- Proof approach: from {a,b}={c,d} extract c∈{a,b} via hS_eq.symm ▸ mem_insert,
-  -- then case split on c=a (same) or c=b (swap). Each half has card ≤ k².
-  -- Total ≤ 2k². Blocked on Finset pair-membership simp and product projection API.
-  sorry
+  unfold additiveEnergy
+  -- The "same" and "swap" target sets (images of S×S under diagonal/swap maps)
+  let same := (S ×ˢ S).image (fun p => (p, p))
+  let swap := (S ×ˢ S).image (fun p => (p, (p.2, p.1)))
+  -- Every filtered quadruple routes to same ∪ swap via finset_pair_eq_iff
+  have hsub : ((S ×ˢ S) ×ˢ (S ×ˢ S)).filter
+      (fun x : (ℕ × ℕ) × (ℕ × ℕ) => x.1.1 + x.1.2 = x.2.1 + x.2.2) ⊆
+      same ∪ swap := by
+    intro ⟨⟨a, b⟩, ⟨c, d⟩⟩ hmem
+    simp only [Finset.mem_filter, Finset.mem_product] at hmem
+    obtain ⟨⟨⟨ha, hb⟩, hc, hd⟩, hsum⟩ := hmem
+    have hpair := hS a b c d ha hb hc hd hsum
+    have hab_mem : (a, b) ∈ S ×ˢ S := Finset.mem_product.mpr ⟨ha, hb⟩
+    rcases finset_pair_eq_iff hpair with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
+    · exact Finset.mem_union_left _ (Finset.mem_image.mpr ⟨(a, b), hab_mem, rfl⟩)
+    · exact Finset.mem_union_right _ (Finset.mem_image.mpr ⟨(a, b), hab_mem, rfl⟩)
+  -- Mechanical cardinality bound: filtered ≤ same ∪ swap ≤ same + swap ≤ 2k²
+  have hcard : (same ∪ swap).card ≤ 2 * S.card ^ 2 :=
+    calc (same ∪ swap).card
+        ≤ same.card + swap.card := Finset.card_union_le same swap
+      _ ≤ (S ×ˢ S).card + (S ×ˢ S).card :=
+          Nat.add_le_add Finset.card_image_le Finset.card_image_le
+      _ = 2 * S.card ^ 2 := by simp [Finset.card_product, Nat.pow_succ, Nat.mul_comm]; ring
+  exact le_trans (Finset.card_le_card hsub) hcard
 
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §7. E₈ Lattice Level-Set Structure
@@ -666,25 +698,26 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) :
 |------|------|--------|--------|
 | `e8_additive_completeness` | §10 | axiom | Open problem in additive combinatorics |
 
-### Fully proved theorems (§8 additions)
+### Fully proved theorems (§5-§11)
 
 | Item | Section | Notes |
 |------|---------|-------|
+| `finset_pair_eq_iff` | §5 | RRC classification: {a,b}={c,d} → same∨swap via Set.pair_eq_pair_iff |
+| `sidon_energy_bound` | §6 | Full proof: dimensional routing to same∪swap, each ≤ k² |
 | `sidon_diff_injective` | §8 | Core lemma: Sidon → distinct positive differences |
 | `exists_collision_witness` | §8 | ¬Sidon → ∃ collision witness extractable |
 | `greedy_sidon_sqrt` | §8 | Full proof: offDiag involution + injection into Icc 1 sup |
 | `fiber_partition` | §11 | Full proof: swap involution splits fiber into even halves |
 | `e8_levelset_density` | §9 | Full proof: Finset.sup' gives finite C bound |
 
-### Sorry inventory (10 sorry tokens across 9 theorems, all with TODO(lean-port))
+### Sorry inventory (9 sorry tokens across 8 theorems, all with TODO(lean-port))
 
 | Item | Section | Blocked on |
 |------|---------|------------|
 | `E4_sq_eq_E8_coeff` | §4 | Mathlib: valence formula or dim M₈ = 1 |
-| `sidon_energy_bound` | §6 | Finset counting; provable now with effort |
 | `r8_via_sigma3` | §7 | Same as E4_sq_eq_E8_coeff (Θ_{E₈} = E₄) |
 | `r8_one` | §7 | Definition mismatch; needs Θ_{E₈} = E₄ |
-| `sidon_iff_zero_collision` | §8 | Finset energy counting (2 sub-sorries) |
+| `sidon_iff_zero_collision` | §8 | Exact cardinality of same∩swap (2 sub-sorries) |
 | `collision_excess_decrease` | §8 | Energy decrease bound (Finset filter counting) |
 | `greedy_sidon_extraction` | §8 | Well-founded induction + √ cardinality bound |
 | `e8_singer_improvement` | §10 | Singer difference set construction |