mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-20 14:17:28 +00:00
chore: remove bak file
This commit is contained in:
parent
5f8ffd59b7
commit
55830c96b9
1 changed files with 0 additions and 263 deletions
|
|
@ -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 = -Σ_{<ij>} 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<j} Σ_{k=0}^{1} J_ij · s_i^k · s_j^k
|
|
||||||
- Σ_{i<j} U_ij · s_i^0 · s_i^1 · s_j^0 · s_j^1
|
|
||||||
|
|
||||||
where:
|
|
||||||
- J_ij = Baker weight = log(a_i + a_j) (transcendental coupling)
|
|
||||||
- U_ij = J_ij · (hx² + hy²) (4-spin term from Hopf direction)
|
|
||||||
- The chirality δ_ij enters through the SIGNED coupling:
|
|
||||||
the effective coupling is J_ij · sign(δ_ij) where δ_ij = hopfAngle. -/
|
|
||||||
noncomputable def ashkinTellerHamiltonian (addrs : List ℤ) (spins : List Z2Quad)
|
|
||||||
(hpos : ∀ a ∈ addrs, ∀ b ∈ addrs, a ≠ b → 0 < a + b) : ℝ :=
|
|
||||||
let sgn := fun (b : Bool) => 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<j} 1/(aⱼ - aᵢ) · log(aᵢ + aⱼ)
|
|
||||||
|
|
||||||
This is the integral of the PFE of cot (E₁ Eisenstein series).
|
|
||||||
In the reformulated model, Λ is the CURVATURE of the coupling. -/
|
|
||||||
noncomputable noncomputable def bakerLambda (addrs : List ℤ) (hpos : ∀ a ∈ addrs, ∀ b ∈ addrs, a ≠ b → 0 < a + b) : ℝ :=
|
|
||||||
match addrs with
|
|
||||||
| [] => 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
|
|
||||||
Loading…
Add table
Reference in a new issue