From 55830c96b99b1aa4b37c1b1de75aea0651384ea4 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 5 Jul 2026 15:05:34 -0500 Subject: [PATCH] chore: remove bak file --- formal/SilverSight/ChiralClockModel.lean.bak | 263 ------------------- 1 file changed, 263 deletions(-) delete mode 100644 formal/SilverSight/ChiralClockModel.lean.bak diff --git a/formal/SilverSight/ChiralClockModel.lean.bak b/formal/SilverSight/ChiralClockModel.lean.bak deleted file mode 100644 index a60fcb5c..00000000 --- a/formal/SilverSight/ChiralClockModel.lean.bak +++ /dev/null @@ -1,263 +0,0 @@ -/- - ChiralClockModel.lean — SU(2) Quaternion Spin Model with Baker-Hopf Coupling - - The reformulated SilverSight model: a Z₂⁴ Ashkin-Teller projection of an - SU(2) quaternion spin model, where the coupling is the Baker functional - weighted by the Hopf fibre direction. - - Foundational papers: - - Huse (1981) PRB 24, 2643 — chiral clock model - - Ostlund (1981) PRB 24, 398 — phase diagram - - Baxter (1982) — exact solutions, chiral Potts connection - - arXiv:2301.10609 — Ashkin-Teller phase diagram (fourfold point) - - arXiv:2606.25618 — SU(2) gauge glass = O(4) spin glass - - arXiv:2410.08754 — Hopf fibration variational formula for spin glasses - - arXiv:2606.11146 — chiral Potts YBE with three spectral parameters - - Model: - H = -Σ_{} Re(q_i⁻¹ · J_ij · q_j), q_i ∈ S³ - - J_ij = log(a_i + a_j) · n̂_ij^Hopf (Baker-weighted Hopf coupling) - - QAOA projection: Z₂⁴ Ashkin-Teller (4 independent binary spins per site) - - CRITICAL DOMAIN NOTE: - For ℕ-valued addresses, arg(a_i + i·a_j) ∈ [0, π/2) — always positive. - Frustration requires ℤ-valued (signed) addresses, where the Gaussian - argument can fall in [π, 2π) producing antiferromagnetic couplings. - The SilverSight model uses ℤ-valued Sidon sets (addresses can be negative) - to ensure the chiral angle has full 360° range. - - Connection to existing SilverSight: - - HopfFibration.lean: Quaternion structure, chiral labels → {1,i,j,k} - - BraidCross.lean: Z₂ XOR crossing slots → Z₂⁴ block structure - - YangBaxter.lean: R₁₂R₁₃R₂₃ = R₂₃R₁₃R₁₂ (integrability preserved) - - CartanConnection.lean: NR bracket [μ,μ]=0 (Sidon block-diagonal) --/ - -import Mathlib.Analysis.SpecialFunctions.Log.Basic -import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -import Mathlib.Tactic - -namespace SilverSight.ChiralClockModel - --- ── Core types ──────────────────────────────────────────────────────── - -/-- A signed Sidon address in Z_n. Addresses can be negative (ℤ-valued) - to ensure the Gaussian argument has full 360° range. -/ -structure SidonAddress where - val : ℤ - mod : ℕ - deriving Repr - -/-- The Baker coupling weight: log(a_i + a_j). - Requires a_i + a_j > 0 (positive sum). -/ -noncomputable def bakerWeight (a₁ a₂ : ℤ) (h : 0 < a₁ + a₂) : ℝ := - Real.log ((a₁ + a₂ : ℝ)) - -/-- The Hopf fibre direction from a pair of signed addresses. - The Gaussian integer a₁ + i·a₂ maps to S² via stereographic projection: - n̂ = (2a₁, 2a₂, a₁² - a₂²) / (a₁² + a₂² + 1) -/ -noncomputable def hopfDirection (a₁ a₂ : ℤ) : ℝ × ℝ × ℝ := - let r1 := (a₁ : ℝ) - let r2 := (a₂ : ℝ) - let norm := r1^2 + r2^2 + 1 - (2 * r1 / norm, 2 * r2 / norm, (r1^2 - r2^2) / norm) - -/-- The Hopf fibre angle (continuous chirality, 360°). - arg(a₁ + i·a₂) = atan2(a₂, a₁) - For ℤ-valued addresses: full [0, 2π) range. -/ -noncomputable def hopfAngle (a₁ a₂ : ℤ) : ℝ := - Real.arctan ((a₂ : ℝ) / (a₁ : ℝ)) - -/-- The full Baker-Hopf coupling: J_ij = log(a_i + a_j) · n̂_ij. - Returns a 3D vector (the imaginary part of the quaternion coupling). - Requires a_i + a_j > 0. -/ -noncomputable def bakerHopfCoupling (a₁ a₂ : ℤ) (h : 0 < a₁ + a₂) : ℝ × ℝ × ℝ := - let w := bakerWeight a₁ a₂ h - let (hx, hy, hz) := hopfDirection a₁ a₂ - (w * hx, w * hy, w * hz) - --- ── Z₂⁴ Ashkin-Teller projection ───────────────────────────────────── - -/-- The Z₂⁴ spin state: 4 independent binary variables per site. - This is the QAOA-solvable projection of the SU(2) quaternion. - Each component corresponds to one of the 4 disjoint 2×2 blocks - in the Sidon crossing matrix (BraidCross.lean). -/ -structure Z2Quad where - s0 : Bool -- block 0 (pair 0↔1) - s1 : Bool -- block 1 (pair 2↔3) - s2 : Bool -- block 2 (pair 4↔5) - s3 : Bool -- block 3 (pair 6↔7) - deriving Repr, DecidableEq - -/-- Convert Z₂ value to ±1. -/ -def z2Sign (b : Bool) : ℤ := - if b then 1 else -1 - -/-- The Z₂⁴ Ashkin-Teller Hamiltonian over all pairs (complete graph). - H = -Σ_{i if b then (1:ℝ) else (-1:ℝ) - -- Pair all addresses (a_i, a_j) with i < j - (List.range addrs.length).foldl (fun acc i => - (List.range addrs.length).foldl (fun acc j => - if i < j then - let a_i := addrs.nthLe i (by - have : i < addrs.length := by - have : i ∈ List.range addrs.length := by - simp - simpa using this - exact this) - let a_j := addrs.nthLe j (by - have : j < addrs.length := by - have : j ∈ List.range addrs.length := by - simp - simpa using this - exact this) - let w := bakerWeight a_i a_j (by - -- hpos ensures 0 < a_i + a_j when a_i ≠ a_j - -- For i ≠ j, we have a_i ≠ a_j (different addresses may be equal, but assume hpos - have a_i_mem : a_i ∈ addrs := by - apply List.mem_of_mem_nthLe - have a_j_mem : a_j ∈ addrs := by - apply List.mem_of_mem_nthLe - -- Use hpos; i ≠ j doesn't guarantee a_i ≠ a_j, but the addresses are - -- typically distinct in Sidon sets. We assume this for the stub. - sorry) - let (hx, hy, _) := hopfDirection a_i a_j - let δ := hopfAngle a_i a_j - -- Chirality sign: +1 if arg < π, -1 if arg ≥ π - let χ := if δ < Real.pi then (1:ℝ) else (-1:ℝ) - let J := w * χ -- signed coupling (Baker weight × chirality sign) - let U := w * (hx * hx + hy * hy) -- AT 4-spin coupling from Hopf - let s_i := spins.nthLe i (by - have : i < spins.length := by - -- spins length equals addrs length in valid Hamiltonians - sorry - exact this) - let s_j := spins.get! j - -- AT: J·(s⁰·s⁰ + s¹·s¹) + U·(s⁰·s¹·s⁰·s¹) - let two_spin := sgn s_i.s0 * sgn s_j.s0 + sgn s_i.s1 * sgn s_j.s1 - let four_spin := sgn s_i.s0 * sgn s_i.s1 * sgn s_j.s0 * sgn s_j.s1 - acc - J * two_spin - U * four_spin - ) 0 - --- ── Frustration ─────────────────────────────────────────────────────── - -/-- Coupling sign from the Gaussian argument chirality. - sign = +1 if arg(a_i + i·a_j) ∈ [0, π), -1 if ∈ [π, 2π). - For ℤ-valued addresses with negative components, arg can exceed π. -/ -noncomputable def chiralitySign (a₁ a₂ : ℤ) : ℤ := - let θ := hopfAngle a₁ a₂ - if θ < Real.pi then 1 else -1 - -/-- A triangle (i, j, k) is frustrated if it has an odd number of - antiferromagnetic (negative) bonds. -/ -noncomputable def isFrustrated (a₁ a₂ a₃ : ℤ) : Bool := - let s12 := chiralitySign a₁ a₂ - let s23 := chiralitySign a₂ a₃ - let s13 := chiralitySign a₁ a₃ - decide (s12 * s23 * s13 < 0) - -/-- Count frustrated triangles in a signed Sidon set. -/ -noncomputable def frustratedTriangleCount (addrs : List ℤ) : ℕ := - let arr := addrs.toArray - let n := arr.size - (List.range n).foldl (fun acc i => - (List.range n).foldl (fun acc j => - (List.range n).foldl (fun acc k => - if i < j ∧ j < k then - if isFrustrated arr[i] arr[j] arr[k] then acc + 1 else acc - else acc - ) acc - ) acc - ) 0 - --- ── Baker functional Λ ──────────────────────────────────────────────── - -/-- The Baker collapse functional: - Λ = Σ_{i 0 - | a :: rest => - (List.foldl (fun acc b => acc + (1 / ((b - a : ℝ))) * Real.log ((a + b : ℝ))) 0 rest) + - bakerLambda rest (by - intro x hx y hy hne - exact hpos x (List.mem_cons_of_mem _ hx) y (List.mem_cons_of_mem _ hy) hne) - --- ── Theorems ────────────────────────────────────────────────────────── - -/-- The Baker weight is positive when the sum exceeds 1. -/ -theorem bakerWeight_pos (a₁ a₂ : ℤ) (h : 1 < a₁ + a₂) : - 0 < bakerWeight a₁ a₂ (by omega) := by - unfold bakerWeight - apply Real.log_pos - norm_cast - omega - -/-- For ℕ-valued (non-negative) addresses, the Gaussian argument - is always in [0, π/2), so chiralitySign is always +1. - This means: frustration requires SIGNED (ℤ-valued) addresses - where the argument can fall in [π, 2π). -/ -theorem chiralitySign_pos_for_nonneg (a₁ a₂ : ℕ) (h1 : 0 ≤ (a₁ : ℤ)) (h2 : 0 ≤ (a₂ : ℤ)) : - chiralitySign a₁ a₂ = 1 := by - unfold chiralitySign hopfAngle - -- atan2(a₂, a₁) for a₁, a₂ ≥ 0 is in [0, π/2] ⊂ [0, π) - -- So the condition θ < π is true, giving sign = 1 - sorry -- needs: Real.atan2_nonneg_of_nonneg - -/-- The Ashkin-Teller Hamiltonian decomposes into 2 independent - Ising models when the 4-spin coupling U = 0 (i.e., hx = hy = 0). -/ -theorem at_decomposes_when_hopf_imaginary_zero - (addrs : List ℤ) (spins : List Z2Quad) - (hpos : ∀ a ∈ addrs, ∀ b ∈ addrs, a ≠ b → 0 < a + b) - (hHopf : ∀ a₁ a₂, hopfDirection a₁ a₂ = (0, 0, 0)) : - ashkinTellerHamiltonian addrs spins hpos = - -- Two independent Ising models (no 4-spin term) - (List.range addrs.length).foldl (fun acc i => - (List.range addrs.length).foldl (fun acc j => - if i < j then - let aᵢ := (addrs.toArray)[i] - let aⱼ := (addrs.toArray)[j] - let w := bakerWeight aᵢ aⱼ (by sorry) - let δ := hopfAngle aᵢ aⱼ - let χ := if δ < Real.pi then (1:ℝ) else (-1:ℝ) - let J := w * χ - let s_i := (spins.toArray)[i] - let s_j := (spins.toArray)[j] - let sgn := fun (b : Bool) => if b then (1:ℝ) else (-1:ℝ) - acc - J * (sgn s_i.s0 * sgn s_j.s0 + sgn s_i.s1 * sgn s_j.s1) - else acc - ) acc - ) 0 := by - sorry - --- ── #eval witnesses ─────────────────────────────────────────────────── - -/-- Baker weight for positive address pairs. -/ -/-- Baker weight for positive address pairs. -/ -/-- Hopf direction for (1, 2). -/ -/-- Hopf angle for (1, 2) — should be in [0, π/2). -/ - -/-- Chirality sign for (1, 2) — should be +1 (arg < π). -/ -/-- Chirality sign for (-1, 2) — should be -1 (arg in [π, 3π/2)). -/ -/-- Chirality sign for (-1, 2) — should be -1 (arg in [π, 3π/2)). -/ - -- This is where frustration comes from: mixed signs produce antiferromagnetic coupling. - -/-- Frustrated triangle: {1, -2, 3} — mixed signs produce frustration. -/ -/-- Baker Λ for {1, 2, 4} (all positive — no frustration). -/ - -end SilverSight.ChiralClockModel