/-
  SidonMirrorNotch.lean — the mirror-projection spine  (NEW, drafted 2026-07-03)

  Written from scratch: no such file existed in the tree, despite being cited as
  `SidonMirrorNotch.lean:32`.  Formalizes the honest, elementary content:

    * mirror involution  τ(a) = S − a
    * mirror-difference invariance — the "observerless invariant": the difference
      set is preserved (up to sign) under the mirror, so it is observer-independent
    * the NOTCH condition: two mirror images a and S−a collapse to the same residue
      for an observer working modulo ℓ exactly when  ℓ ∣ (2a − S).

  This is exact elementary number theory (an involution + Int.ModEq).  The
  multi-observer CRT recovery (coprime ℓ₁,ℓ₂ ⇒ recover a mod ℓ₁ℓ₂) is the standard
  Chinese Remainder Theorem (Mathlib: `ZMod.chineseRemainder`) and is left as the
  next layer.
-/
import Mathlib.Data.Int.ModEq
import Mathlib.Tactic

namespace SilverSight.PIST.SidonMirrorNotch

/-- The mirror involution of the Sidon set with reflection point `S`: `τ(a) = S − a`. -/
def mirror (S a : ℤ) : ℤ := S - a

/-- `τ` is an involution: `τ(τ a) = a`. -/
theorem mirror_involutive (S a : ℤ) : mirror S (mirror S a) = a := by
  unfold mirror; ring

/-- Observerless invariant: the mirror negates differences, so the difference
    set `{±(a−b)}` is mirror-invariant (independent of which mirror you observe). -/
theorem mirror_diff (S a b : ℤ) : mirror S a - mirror S b = -(a - b) := by
  unfold mirror; ring

/-- **Mirror Notch.**  An observer working modulo `ℓ` sees `a` and its mirror
    `S − a` as the same residue exactly when `ℓ ∣ (2a − S)`.  This is the
    exact-projection (notch) condition: the mirror pair collapses under the
    mod-`ℓ` observation iff `ℓ ∣ (2a − S)`. -/
theorem mirror_notch (S a l : ℤ) : a ≡ mirror S a [ZMOD l] ↔ l ∣ (2 * a - S) := by
  unfold mirror
  rw [Int.modEq_iff_dvd, show (S - a) - a = -(2 * a - S) from by ring, dvd_neg]

/-- Fixed point (self-mirror) case: `a` is its own mirror iff `2a = S`. -/
theorem mirror_fixed (S a : ℤ) : mirror S a = a ↔ 2 * a = S := by
  unfold mirror; omega

end SilverSight.PIST.SidonMirrorNotch
