CollisionFramework.lean

/-
  Additive collision hypergraph framework for Erdos Problem 530.

  This file does not prove the open asymptotic conjecture. It provides a
  reusable checked layer for the strategy: a Sidon subset is an independent set
  in the hypergraph whose edges are nontrivial additive-collision supports.
-/

import Mathlib.Data.Finset.Card
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

namespace Erdos530
namespace CollisionFramework

variable {alpha : Type*} [Add alpha]

/-! ## Sidon sets and additive collisions -/

/-- A finite set is Sidon if pairwise sums determine the unordered pair. -/
def IsSidon (S : Finset alpha) : Prop :=
  forall a b c d : alpha, a ∈ S -> b ∈ S -> c ∈ S -> d ∈ S ->
    a + b = c + d -> ({a, b} : Set alpha) = {c, d}

/-- A nontrivial additive collision inside a finite set. -/
def HasAdditiveCollision (S : Finset alpha) : Prop :=
  exists a b c d : alpha, a ∈ S /\ b ∈ S /\ c ∈ S /\ d ∈ S /\
    a + b = c + d /\ ({a, b} : Set alpha) ≠ {c, d}

/-- Being Sidon is exactly having no nontrivial additive collision. -/
theorem isSidon_iff_no_additiveCollision (S : Finset alpha) :
  IsSidon S <-> ¬ HasAdditiveCollision S := by
  constructor
  · intro hSidon hCollision
    rcases hCollision with ⟨a, b, c, d, ha, hb, hc, hd, hSum, hNeq⟩
    exact hNeq (hSidon a b c d ha hb hc hd hSum)
  · intro hNoCollision a b c d ha hb hc hd hSum
    by_contra hPair
    exact hNoCollision ⟨a, b, c, d, ha, hb, hc, hd, hSum, hPair⟩

/-- Sidon sets are closed downward under taking subsets. -/
theorem IsSidon.mono {T S : Finset alpha} (hSidon : IsSidon S) (hTS : T ⊆ S) :
    IsSidon T := by
  intro a b c d ha hb hc hd hSum
  exact hSidon a b c d (hTS ha) (hTS hb) (hTS hc) (hTS hd) hSum

/-! ## Transfer through additive-relation models -/

variable {beta : Type*} [Add beta]

/--
`f` reflects additive relations on `A`: if a two-term additive equality holds
after applying `f`, then the original two-term additive equality already held.
-/
def ReflectsAdditiveRelationsOn (A : Finset alpha) (f : alpha -> beta) : Prop :=
  forall a b c d : alpha, a ∈ A -> b ∈ A -> c ∈ A -> d ∈ A ->
    f a + f b = f c + f d -> a + b = c + d

/-- Applying any map to both sides of an unordered pair equality preserves it. -/
theorem pair_image_eq_of_pair_eq {gamma delta : Type*} {f : gamma -> delta} {a b c d : gamma}
  (h : ({a, b} : Set gamma) = {c, d}) :
  ({f a, f b} : Set delta) = {f c, f d} := by
  ext x
  constructor
  · intro hx
    rcases hx with rfl | rfl
    · have ha : a = c ∨ a = d := by
        have : a ∈ ({c, d} : Set gamma) := by
          rw [← h]
          simp
        simpa using this
      rcases ha with rfl | rfl <;> simp
    · have hb : b = c ∨ b = d := by
        have : b ∈ ({c, d} : Set gamma) := by
          rw [← h]
          simp
        simpa using this
      rcases hb with rfl | rfl <;> simp
  · intro hx
    rcases hx with rfl | rfl
    · have hc : c = a ∨ c = b := by
        have : c ∈ ({a, b} : Set gamma) := by
          rw [h]
          simp
        simpa using this
      rcases hc with rfl | rfl <;> simp
    · have hd : d = a ∨ d = b := by
        have : d ∈ ({a, b} : Set gamma) := by
          rw [h]
          simp
        simpa using this
      rcases hd with rfl | rfl <;> simp

/--
The Sidon property transfers to the image of a set under any map that reflects
two-term additive relations on the ambient set.
-/
theorem IsSidon.image_of_reflectsAdditiveRelationsOn [DecidableEq beta]
    {A S : Finset alpha} {f : alpha -> beta}
    (hSidon : IsSidon S) (hSubset : S ⊆ A)
    (hReflect : ReflectsAdditiveRelationsOn A f) :
    IsSidon (S.image f) := by
  classical
  intro x y z w hx hy hz hw hSum
  rcases Finset.mem_image.mp hx with ⟨a, haS, rfl⟩
  rcases Finset.mem_image.mp hy with ⟨b, hbS, rfl⟩
  rcases Finset.mem_image.mp hz with ⟨c, hcS, rfl⟩
  rcases Finset.mem_image.mp hw with ⟨d, hdS, rfl⟩
  have hOrigSum : a + b = c + d :=
    hReflect a b c d (hSubset haS) (hSubset hbS) (hSubset hcS) (hSubset hdS) hSum
  exact pair_image_eq_of_pair_eq (hSidon a b c d haS hbS hcS hdS hOrigSum)

/-- Casting natural numbers to real numbers reflects two-term additive relations. -/
theorem natCast_reflectsAdditiveRelationsOn_real (A : Finset Nat) :
    ReflectsAdditiveRelationsOn A (fun n : Nat => (n : Real)) := by
  intro a b c d _ _ _ _ h
  have h' : ((a + b : Nat) : Real) = ((c + d : Nat) : Real) := by
    simpa using h
  exact Nat.cast_inj.mp h'

/-- A natural-number Sidon set remains Sidon after casting it into `Real`. -/
theorem IsSidon.image_natCast_real {S : Finset Nat} (hSidon : IsSidon S) :
    IsSidon (S.image (fun n : Nat => (n : Real))) := by
  exact hSidon.image_of_reflectsAdditiveRelationsOn (A := S) (f := fun n : Nat => (n : Real))
    (by intro x hx; exact hx) (natCast_reflectsAdditiveRelationsOn_real S)

/-! ## Predicate-style collision hypergraph -/

variable [DecidableEq alpha]

/--
`CollisionHyperedge A edge` means `edge` is the support of a nontrivial
additive collision among elements of `A`.
-/
def CollisionHyperedge (A edge : Finset alpha) : Prop :=
  exists a b c d : alpha, a ∈ A /\ b ∈ A /\ c ∈ A /\ d ∈ A /\
    a + b = c + d /\ ({a, b} : Set alpha) ≠ {c, d} /\
      edge = ({a, b, c, d} : Finset alpha)

/-- A subset is independent if it contains no collision hyperedge. -/
def HypergraphIndependent (A S : Finset alpha) : Prop :=
  S ⊆ A /\ forall edge : Finset alpha, CollisionHyperedge A edge -> ¬ edge ⊆ S

/-- Hypergraph independence is exactly subset containment plus no collision. -/
theorem hypergraphIndependent_iff_subset_and_no_collision (A S : Finset alpha) :
  HypergraphIndependent A S <-> S ⊆ A /\ ¬ HasAdditiveCollision S := by
  constructor
  · intro hIndependent
    refine ⟨hIndependent.1, ?_⟩
    intro hCollision
    rcases hCollision with ⟨a, b, c, d, ha, hb, hc, hd, hSum, hNeq⟩
    let edge : Finset alpha := {a, b, c, d}
    have hEdge : CollisionHyperedge A edge := by
      exact ⟨a, b, c, d, hIndependent.1 ha, hIndependent.1 hb,
        hIndependent.1 hc, hIndependent.1 hd, hSum, hNeq, rfl⟩
    have hEdgeSubset : edge ⊆ S := by
      intro x hx
      simp only [edge, Finset.mem_insert, Finset.mem_singleton] at hx
      rcases hx with rfl | rfl | rfl | rfl
      · exact ha
      · exact hb
      · exact hc
      · exact hd
    exact hIndependent.2 edge hEdge hEdgeSubset
  · intro h
    refine ⟨h.1, ?_⟩
    intro edge hEdge hEdgeSubset
    rcases hEdge with ⟨a, b, c, d, _ha, _hb, _hc, _hd, hSum, hNeq, rfl⟩
    apply h.2
    refine ⟨a, b, c, d, ?_, ?_, ?_, ?_, hSum, hNeq⟩
    · exact hEdgeSubset (by simp : a ∈ ({a, b, c, d} : Finset alpha))
    · exact hEdgeSubset (by simp : b ∈ ({a, b, c, d} : Finset alpha))
    · exact hEdgeSubset (by simp : c ∈ ({a, b, c, d} : Finset alpha))
    · exact hEdgeSubset (by simp : d ∈ ({a, b, c, d} : Finset alpha))

/-- Sidon subsets are exactly independent sets in the collision hypergraph. -/
theorem hypergraphIndependent_iff_subset_and_sidon (A S : Finset alpha) :
    HypergraphIndependent A S <-> S ⊆ A /\ IsSidon S := by
  rw [hypergraphIndependent_iff_subset_and_no_collision]
  constructor
  · intro h
    exact ⟨h.1, (isSidon_iff_no_additiveCollision S).2 h.2⟩
  · intro h
    exact ⟨h.1, (isSidon_iff_no_additiveCollision S).1 h.2⟩

/-- Independent sets are closed downward under taking subsets. -/
theorem HypergraphIndependent.mono {A S T : Finset alpha}
    (hIndependent : HypergraphIndependent A S) (hTS : T ⊆ S) :
    HypergraphIndependent A T := by
  rw [hypergraphIndependent_iff_subset_and_sidon] at hIndependent ⊢
  exact ⟨fun x hx => hIndependent.1 (hTS hx), hIndependent.2.mono hTS⟩

/-! ## Deleting a hitting set -/

/-- A set `R` hits every additive-collision hyperedge of `A`. -/
def HitsEveryCollisionHyperedge (A R : Finset alpha) : Prop :=
  forall edge : Finset alpha, CollisionHyperedge A edge -> exists x, x ∈ edge /\ x ∈ R

/-- Deleting a set that hits every collision hyperedge leaves an independent set. -/
theorem sdiff_hittingSet_independent (A R : Finset alpha)
    (hHit : HitsEveryCollisionHyperedge A R) :
    HypergraphIndependent A (A \ R) := by
  refine ⟨Finset.sdiff_subset, ?_⟩
  intro edge hEdge hEdgeSubset
  rcases hHit edge hEdge with ⟨x, hxEdge, hxR⟩
  have hxNotR : x ∉ R := (Finset.mem_sdiff.mp (hEdgeSubset hxEdge)).2
  exact hxNotR hxR

/-- Deleting a set that hits every collision hyperedge leaves a Sidon set. -/
theorem sdiff_hittingSet_isSidon (A R : Finset alpha)
    (hHit : HitsEveryCollisionHyperedge A R) :
    IsSidon (A \ R) := by
  exact (hypergraphIndependent_iff_subset_and_sidon A (A \ R)).1
    (sdiff_hittingSet_independent A R hHit) |>.2

end CollisionFramework
end Erdos530