Close the loop: retire re-exported YB tautology; register SidonMirrorNotch

UnifiedCovariant.lean: layer_2d_yang_baxter_holds (a re-export of the deleted X=X tautology, using the removed B) replaced by layer_2d_braid_relation := braid_relation_S8; the false YB-integrability-by-alpha-equivalence docstring corrected. lakefile.lean: register SilverSight.PIST.SidonMirrorNotch. Full lake build of the chain is green (3300 jobs); remaining sorry warnings are pre-existing Layer-3 geometric-conjecture stubs, not introduced here.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

formal/SilverSight/PIST/UnifiedCovariant.lean

@@ -167,23 +167,18 @@ lemma gate_C_jacobiator_basis_zero (i j k : Fin 7) : Jacobiator mu (v i) (v j) (
   Jacobiator_basis_zero i j k
 
 /--
-  Layer 2d — Yang-Baxter integrability of the Sidon braid.
+  Layer 2d — the honest braid content of the Sidon crossing.
 
-  The 2×2 Sidon crossing block B = [[39/256, 1/7], [1/7, 39/256]]
-  generates an R-matrix R = B⊗B (Kronecker product) satisfying the
-  quantum Yang-Baxter equation on ℚ²⊗ℚ²⊗ℚ²:
-
-    R₁₂ R₁₃ R₂₃ = R₂₃ R₁₃ R₁₂
-
-  The equality holds by alpha-equivalence: both sides differ only by
-  renaming the bound summation variable r↔s.
-
-  See YangBaxter.lean for the full derivation and coefficient formulas.
+  The prior claim "R = B⊗B satisfies the quantum Yang-Baxter equation" was
+  vacuous: R = B⊗B satisfies the YBE for ANY B (both sides reduce to
+  B²⊗B²⊗B²), and the old proof was `rfl` over an alpha-renamed sum (X = X).
+  An exact ℚ search (scratchpad/ybe_sidon.py) further showed the Sidon block
+  admits no invertible, non-triangular R-matrix.  The real, non-vacuous content
+  is the symmetric-group braid relation, stated as an 8×8 permutation-matrix
+  identity in YangBaxter.lean (`braid_relation_S8`, with a negative control).
 -/
-theorem layer_2d_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) :=
-  yang_baxter_holds
+theorem layer_2d_braid_relation : sL * sR * sL = sR * sL * sR :=
+  braid_relation_S8
 
 end Layer2c_NRBracket
 

lakefile.lean

@@ -74,6 +74,7 @@ lean_lib «SilverSightRRC» where
     `SilverSight.PIST.UnifiedCovariant,
     `SilverSight.PIST.CartanConnection,
     `SilverSight.PIST.YangBaxter,
+    `SilverSight.PIST.SidonMirrorNotch,
     `SilverSight.PIST.Tdoku16D,
     `SilverSight.PIST.CrossDomainSynthesis,
     `SilverSight.PIST.MultiSurfacePacker,