mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
Replace vacuous YangBaxter tautology with honest S_n braid relation; add SidonMirrorNotch
YangBaxter.lean: the prior `yang_baxter_holds` was `rfl` over two alpha-equivalent sums (literally X = X); even the intended R = B(x)B claim satisfies YBE vacuously (B^2(x)B^2(x)B^2 on both sides, for any B). An exact rational search (ybe_sidon.py, ybe_verify.py) showed the Sidon block admits no invertible, non-triangular R-matrix. Replaced with `braid_relation_S8` -- the honest symmetric-group (S_n image of B_n, Artin 1947) braid relation as a concrete 8x8 permutation-matrix identity, by `decide` -- plus `braid_relation_falsifiable`, a negative control proving the statement is not vacuous (a non-permutation gate breaks it). Both axiom-clean: no sorryAx, no ofReduceBool (genuine kernel `decide`, not native_decide). SidonMirrorNotch.lean (new): the mirror-projection spine, written from scratch (no such file existed despite being cited). Mirror involution tau(a) = S - a, the observerless difference-invariant, and the notch congruence a == S - a [ZMOD l] <-> l | (2a - S). Both files verified standalone via `lake env lean` (elan toolchain v4.30.0-rc2). Known follow-up (next commit): UnifiedCovariant.lean re-exports the deleted `yang_baxter_holds` and must be retired for a green full `lake build`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
069e54d8e9
commit
0125c9b487
2 changed files with 96 additions and 39 deletions
47
formal/SilverSight/PIST/SidonMirrorNotch.lean
Normal file
47
formal/SilverSight/PIST/SidonMirrorNotch.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue