diff --git a/formal/SilverSight/PIST/SidonMirrorNotch.lean b/formal/SilverSight/PIST/SidonMirrorNotch.lean
new file mode 100644
index 00000000..70338090
--- /dev/null
+++ b/formal/SilverSight/PIST/SidonMirrorNotch.lean
@@ -0,0 +1,47 @@
+/-
+  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
diff --git a/formal/SilverSight/PIST/YangBaxter.lean b/formal/SilverSight/PIST/YangBaxter.lean
index 791f75fb..3e6fd4ad 100644
--- a/formal/SilverSight/PIST/YangBaxter.lean
+++ b/formal/SilverSight/PIST/YangBaxter.lean
@@ -1,53 +1,63 @@
 /-
-  YangBaxter.lean — Layer 2d: Yang-Baxter integrability of the Sidon braid
+  YangBaxter.lean — Layer 2d  (HONEST REWRITE 2026-07-03)
 
-  Theorem: The 2×2 Sidon crossing block B = [[σ,τ],[τ,σ]] generates an
-  R-matrix R = B ⊗ B (Kronecker product) that satisfies the quantum
-  Yang-Baxter equation on ℚ² ⊗ ℚ² ⊗ ℚ².
+  The prior version proved `yang_baxter_holds` by `rfl` over two alpha-equivalent
+  sums (bound variable r ↔ s): the statement was literally X = X.  Even the
+  *intended* claim (R = B⊗B satisfies the YBE) is vacuous — on V⊗V⊗V,
+  R₁₂·R₁₃·R₂₃ = B²⊗B²⊗B² = R₂₃·R₁₃·R₁₂ for ANY B, because single-site operators
+  on distinct strands commute.
 
-  The quantum YB equation for R: V⊗V → V⊗V is:
-    R₁₂ R₁₃ R₂₃ = R₂₃ R₁₃ R₁₂
+  An exact search over ℚ (scratchpad/ybe_sidon.py, ybe_verify.py) further showed
+  the Sidon block B = σI + τX admits NO invertible, non-triangular (entangling)
+  constant R-matrix: on the B⊗B-commutant every invertible YBE solution is
+  diagonal, the permutation P, or triangular.  So "Yang-Baxter integrability of
+  the Sidon braid" is not a real theorem — the only YBE structure it carries is
+  the trivial permutation.
 
-  where R₁₂ = R⊗I, R₂₃ = I⊗R, and R₁₃ applies R to the first and
-  third factors.
-
-  For basis vectors e_a, e_b, e_c ∈ ℚ², the YB equation reduces to
-  equality of coefficients:
-
-    LHS (R₁₂ R₁₃ R₂₃):
-      Σ_{p,q,r} B[a,p]·B[b,q]·B[p,x]·B[q,y]·B[c,r]·B[r,z]
-
-    RHS (R₂₃ R₁₃ R₁₂):
-      Σ_{p,q,s} B[a,p]·B[b,q]·B[p,x]·B[q,y]·B[c,s]·B[s,z]
-
-  The equality holds by alpha-equivalence (both sides differ only by
-  renaming bound variable r↔s).
-
-  Combined with d_CE μ = 0 (CartanConnection.lean, Gate C), this closes
-  Layer 2d of the breakglass: [μ,μ]_{NR} = 0 ⇒ YB integrability.
+  This file therefore states the HONEST content: the symmetric-group braid
+  relation (the Sₙ image of Bₙ, Artin 1947), realised as a concrete 8×8
+  permutation-matrix identity on the 3-strand space, with a NEGATIVE CONTROL
+  proving the statement is falsifiable (a non-permutation gate breaks it).
+  Matrices verified independently in scratchpad/emit_braid_matrices.py.
 -/
-
+import Mathlib.LinearAlgebra.Matrix.Notation
 import Mathlib.Tactic
 
-open scoped BigOperators
-
-set_option linter.unusedVariables false
+open Matrix
 
 namespace SilverSight.PIST.YangBaxter
 
-/-- The 2×2 Sidon crossing block with σ = 39/256 (diagonal) and
-    τ = 1/7 (same-block off-diagonal), matching UnifiedCovariant. -/
-def B (i j : Fin 2) : ℚ :=
-  if i = j then (39/256 : ℚ) else (1/7 : ℚ)
+/-- SWAP of strands (1,2) on the 3-strand computational space (2³ = 8-dim),
+    as a permutation matrix.  Equals SWAP ⊗ I₂. -/
+abbrev sL : Matrix (Fin 8) (Fin 8) ℤ :=
+  !![1,0,0,0,0,0,0,0; 0,1,0,0,0,0,0,0; 0,0,0,0,1,0,0,0; 0,0,0,0,0,1,0,0;
+     0,0,1,0,0,0,0,0; 0,0,0,1,0,0,0,0; 0,0,0,0,0,0,1,0; 0,0,0,0,0,0,0,1]
 
-/-- Theorem: R = B ⊗ B satisfies the quantum Yang-Baxter equation.
+/-- SWAP of strands (2,3).  Equals I₂ ⊗ SWAP. -/
+abbrev sR : Matrix (Fin 8) (Fin 8) ℤ :=
+  !![1,0,0,0,0,0,0,0; 0,0,1,0,0,0,0,0; 0,1,0,0,0,0,0,0; 0,0,0,1,0,0,0,0;
+     0,0,0,0,1,0,0,0; 0,0,0,0,0,0,1,0; 0,0,0,0,0,1,0,0; 0,0,0,0,0,0,0,1]
 
-    The equation R₁₂ R₁₃ R₂₃ = R₂₃ R₁₃ R₁₂ (on ℚ²⊗ℚ²⊗ℚ²) is verified
-    by checking the coefficient equality for each output basis vector
-    e_x⊗e_y⊗e_z, for all input basis vectors e_a⊗e_b⊗e_c. -/
-theorem yang_baxter_holds : ∀ (a b c x y z : Fin 2),
-    (∑ p : Fin 2, ∑ q : Fin 2, ∑ r : Fin 2, B a p * B b q * B p x * B q y * B c r * B r z) =
-    (∑ p : Fin 2, ∑ q : Fin 2, ∑ s : Fin 2, B a p * B b q * B p x * B q y * B c s * B s z) :=
-  fun a b c x y z => rfl
+/-- **Honest braid relation** (Sₙ image of B₃): the adjacent-strand swaps satisfy
+    σ₁σ₂σ₁ = σ₂σ₁σ₂; both sides realise the (1 3) transposition.  This is the
+    TRIVIAL (permutation) solution of the Yang-Baxter equation — the only YBE
+    structure the Sidon braid actually carries (see header). -/
+theorem braid_relation_S8 : sL * sR * sL = sR * sL * sR := by decide
+
+/-- Negative control gate 1 (a non-permutation shear on strands 1,2). -/
+abbrev sBadL : Matrix (Fin 8) (Fin 8) ℤ :=
+  !![1,0,1,0,0,0,0,0; 0,1,0,1,0,0,0,0; 0,0,1,0,0,0,0,0; 0,0,0,1,0,0,0,0;
+     0,0,0,0,1,0,0,0; 0,0,0,0,0,1,0,0; 0,0,0,0,0,0,1,0; 0,0,0,0,0,0,0,1]
+
+/-- Negative control gate 2 (the same shear on strands 2,3). -/
+abbrev sBadR : Matrix (Fin 8) (Fin 8) ℤ :=
+  !![1,1,0,0,0,0,0,0; 0,1,0,0,0,0,0,0; 0,0,1,0,0,0,0,0; 0,0,0,1,0,0,0,0;
+     0,0,0,0,1,1,0,0; 0,0,0,0,0,1,0,0; 0,0,0,0,0,0,1,0; 0,0,0,0,0,0,0,1]
+
+/-- **Negative control** (anti-smuggle): the braid relation is FALSIFIABLE.
+    A non-permutation gate on the same strands BREAKS the relation, so
+    `braid_relation_S8` is not vacuous.  Verified in emit_braid_matrices.py. -/
+theorem braid_relation_falsifiable :
+    sBadL * sBadR * sBadL ≠ sBadR * sBadL * sBadR := by decide
 
 end SilverSight.PIST.YangBaxter