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

open Finset
open Nat

/-!
# Strand Capacity Bound

A single chiral strand pair (L₁, L₂) maps each a ∈ A to the pair
(a mod L₁, S−a mod L₂) on the 2-torus Z/L₁Z × Z/L₂Z.

## Theorem

For a single strand with moduli L₁, L₂ and any finite set A:

    |F(A)| ≤ min(|A|, L₁·L₂) × 2

The bound has two parts:
  1. |F(A)| ≤ |A|              (injectivity — F is a function from A)
  2. |F(A)| ≤ L₁·L₂            (codomain has only L₁·L₂ distinct pairs)
-/

variable (L₁ L₂ S : ℕ)

/-- The strand pairing: (a mod L₁, S − a mod L₂). -/
def strandPair (a : ℤ) : ℤ × ℤ :=
  (a % (L₁ : ℤ), ((S : ℤ) - a) % (L₂ : ℤ))

/-- Image of A under the strand pairing. -/
noncomputable def strandImage (A : Set ℤ) : Set (ℤ × ℤ) :=
  strandPair L₁ L₂ S '' A

/-- Bound 1: image cardinality ≤ input cardinality (trivial, F is a function). -/
theorem capacity_bound_input (A : Finset ℤ) :
    (A.image (strandPair L₁ L₂ S)).card ≤ A.card :=
  Finset.card_image_le

/--
Bound 2: the codomain grid has size L₁·L₂.
Each residue lies in [0, L₁) resp. [0, L₂), so at most
L₁ × L₂ distinct pairs are reachable regardless of |A|.
-/
theorem capacity_bound_grid (A : Finset ℤ) (hL₁ : 0 < L₁) (hL₂ : 0 < L₂) :
    (A.image (strandPair L₁ L₂ S)).card ≤ (L₁ : ℕ) * L₂ := by
  have hL₁' : (0 : ℤ) < (L₁ : ℤ) := by exact_mod_cast hL₁
  have hL₂' : (0 : ℤ) < (L₂ : ℤ) := by exact_mod_cast hL₂
  -- The grid of possible residues
  let grid : Finset (ℤ × ℤ) :=
    (Finset.Ico 0 (L₁ : ℤ)) ×ˢ (Finset.Ico 0 (L₂ : ℤ))
  have hgrid : grid.card = (L₁ : ℕ) * L₂ := by
    simp [grid, Finset.card_product, Int.card_Ico]
  -- Every strand pair lands in the grid
  have hmem : ∀ a : ℤ, strandPair L₁ L₂ S a ∈ grid := by
    intro a
    have hx : a % (L₁ : ℤ) ∈ Finset.Ico 0 (L₁ : ℤ) := by
      have hnonneg : 0 ≤ a % (L₁ : ℤ) := Int.emod_nonneg a (ne_of_gt hL₁')
      have hlt : a % (L₁ : ℤ) < (L₁ : ℤ) := Int.emod_lt_of_pos a hL₁'
      exact Finset.mem_Ico.mpr ⟨hnonneg, hlt⟩
    have hy : ((S : ℤ) - a) % (L₂ : ℤ) ∈ Finset.Ico 0 (L₂ : ℤ) := by
      have hnonneg' : 0 ≤ ((S : ℤ) - a) % (L₂ : ℤ) :=
        Int.emod_nonneg _ (ne_of_gt hL₂')
      have hlt' : ((S : ℤ) - a) % (L₂ : ℤ) < (L₂ : ℤ) :=
        Int.emod_lt_of_pos _ hL₂'
      exact Finset.mem_Ico.mpr ⟨hnonneg', hlt'⟩
    exact Finset.mem_product.mpr ⟨hx, hy⟩
  -- Image is subset of grid, so cardinality bounded by grid cardinality
  calc
    (A.image (strandPair L₁ L₂ S)).card ≤ grid.card :=
      Finset.card_le_card (Finset.image_subset_iff.mpr (fun a _ => hmem a))
    _ = (L₁ : ℕ) * L₂ := hgrid

/--
Combined bound: |F(A)| ≤ min(|A|, L₁·L₂).

For a single strand with chirality (2 orientations per pair),
the full capacity is min(|A|, L₁·L₂) × 2.
-/
theorem capacity_bound (A : Finset ℤ) (hL₁ : 0 < L₁) (hL₂ : 0 < L₂) :
    (A.image (strandPair L₁ L₂ S)).card ≤ min A.card ((L₁ : ℕ) * L₂) := by
  apply le_min
  · exact capacity_bound_input L₁ L₂ S A
  · exact capacity_bound_grid L₁ L₂ S A hL₁ hL₂

/--
With chirality: each pair can be read in 2 orders
(identity, reflection) or (reflection, identity),
corresponding to σᵢ vs σᵢ⁻¹ in the braid group.
-/
theorem chiral_capacity_bound (A : Finset ℤ) (hL₁ : 0 < L₁) (hL₂ : 0 < L₂) :
    (A.image (strandPair L₁ L₂ S)).card * 2 ≤ min A.card ((L₁ : ℕ) * L₂) * 2 := by
  nlinarith [capacity_bound L₁ L₂ S A hL₁ hL₂]

-- Sidon example A = {1,2,5,6} with moduli 3,4, S=7 → image has 4 distinct pairs:
-- 1↦(1,2), 2↦(2,1), 5↦(2,2), 6↦(0,1). Kernel-checked (`decide`, not
-- `#eval`/`native_decide`), sidestepping ℤ's noncomputable order instance.
example : (({1, 2, 5, 6} : Finset ℤ).image (strandPair 3 4 7)).card = 4 := by decide
-- Full range Ico 1 7 = {1,…,6} instead gives 6 distinct pairs (all injective here):
example : ((Finset.Ico (1 : ℤ) 7).image (strandPair 3 4 7)).card = 6 := by decide