From 094f2119226df9b9a7a0e3468640944916424a21 Mon Sep 17 00:00:00 2001 From: allaun Date: Fri, 3 Jul 2026 04:26:05 -0500 Subject: [PATCH] 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 --- formal/SilverSight/PIST/UnifiedCovariant.lean | 25 ++++++++----------- lakefile.lean | 1 + 2 files changed, 11 insertions(+), 15 deletions(-) diff --git a/formal/SilverSight/PIST/UnifiedCovariant.lean b/formal/SilverSight/PIST/UnifiedCovariant.lean index 712fac17..bfa6bb5e 100644 --- a/formal/SilverSight/PIST/UnifiedCovariant.lean +++ b/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 diff --git a/lakefile.lean b/lakefile.lean index 2d058cab..03a72a14 100644 --- a/lakefile.lean +++ b/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,