import Mathlib.Data.Nat.Basic
import Mathlib.Data.Int.Basic
import Mathlib.Tactic

open Nat

/-!
# Sidon Creation: Wrapping Criterion

STATUS: DEVELOPMENT — NOT part of active build.
HONESTY CLASS: DEVELOPMENT (in progress, contains untagged sorries and axioms)

Two pairs (a,b) and (c,d) with a+b = c+d = T collide under F modulo M,
but their integer lifts ℤ may differ if the individual sums straddle the
modulus boundary M differently. This breaks the Sidon collision.

## Theorem (Wrapping Criterion)

Let F̂(a) ∈ [0, M) be the CRT integer lift of a.
If a+b = c+d but (F̂(a)+F̂(b) ≥ M) ≠ (F̂(c)+F̂(d) ≥ M),
then F(A) is Sidon where A was not.

## 2-modulus special case

For k = 2 with moduli (L₁, L₂), the CRT lift has closed form:
  F̂(a) = a + L₁·((S − 2a) · L₁⁻¹ mod L₂)
where L₁⁻¹ is the modular inverse of L₁ modulo L₂.
-/

variable (L₁ L₂ S : ℕ)

/-- CRT inverse: given residues (r₁ mod L₁, r₂ mod L₂), return the unique
integer in [0, L₁·L₂) with those residues. Requires gcd(L₁, L₂) = 1. This
is left as an axiom for now; the full CRT lemma is in Mathlib/Data/ZMod.
HONESTY CLASS: DEVELOPMENT (scaffold axiom, not used in active build). -/
axiom crtLift (r₁ r₂ : ℤ) : ℤ

/-- The CRT lift of the strand pair (a mod L₁, S−a mod L₂). -/
def strandLift (a : ℤ) : ℤ :=
  crtLift L₁ L₂ (a % (L₁ : ℤ)) (((S : ℤ) - a) % (L₂ : ℤ))

/-- Wrapping indicator: 1 if the sum of two lifts crosses M = L₁·L₂, else 0. -/
def wrap (a b : ℤ) : ℕ :=
  if strandLift L₁ L₂ S a + strandLift L₁ L₂ S b ≥ (L₁ : ℕ) * L₂ then 1 else 0

/--
Two pairs (a,b) and (c,d) with the same integer sum T = a+b = c+d.
Their image sums differ by exactly(wrap₁ − wrap₂)·M.
-/
theorem wrapping_diff (a b c d : ℤ) (hsum : a + b = c + d) :
    (strandLift L₁ L₂ S a + strandLift L₁ L₂ S b) -
    (strandLift L₁ L₂ S c + strandLift L₁ L₂ S d) =
    ((wrap L₁ L₂ S a b : ℤ) - (wrap L₁ L₂ S c d : ℤ)) * ((L₁ : ℕ) * L₂ : ℤ) := by
  have hmod : strandLift L₁ L₂ S a + strandLift L₁ L₂ S b ≡
             strandLift L₁ L₂ S c + strandLift L₁ L₂ S d [ZMOD (L₁ : ℕ) * L₂] := by
    -- Both sums are ≡ T (mod L₁) and ≡ 2S−T (mod L₂), hence ≡ T (mod M) by CRT
    -- (This holds by AXIOM because crtLift is a CRT representative)
    sorry
  -- The difference is a multiple of M, either 0 or ±M depending on wraps
  sorry

/--
Sidon creation: if the two pairs wrap differently, their integer sums differ.
-/
theorem sidon_creation (a b c d : ℤ) (hsum : a + b = c + d)
    (hw : wrap L₁ L₂ S a b ≠ wrap L₁ L₂ S c d) :
    strandLift L₁ L₂ S a + strandLift L₁ L₂ S b ≠
    strandLift L₁ L₂ S c + strandLift L₁ L₂ S d := by
  intro heq
  have := wrapping_diff L₁ L₂ S a b c d hsum
  have hzero : (wrap L₁ L₂ S a b : ℤ) - (wrap L₁ L₂ S c d : ℤ) = 0 := by
    nlinarith
  have : wrap L₁ L₂ S a b = wrap L₁ L₂ S c d := by
    omega
  exact hw this

-- #eval witness for the Sidon example
#eval let L₁ := 3; L₂ := 4; S := 7 in
  wrap L₁ L₂ S (1 : ℤ) (6 : ℤ)  -- expected: 1 (10+9=19 ≥ 12)
#eval let L₁ := 3; L₂ := 4; S := 7 in
  wrap L₁ L₂ S (2 : ℤ) (5 : ℤ)  -- expected: 0 (5+2=7 < 12)
