Spin.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

The two-spin Heisenberg interaction

The basis order is ↑↑, ↑↓, ↓↑, ↓↓. The matrix below is X ⊗ X + Y ⊗ Y + Z ⊗ Z = 2 SWAP - I in that basis. The exact singlet/triplet computation supplies the interaction bound used when rounding or deleting source coefficients in both continuum Coulomb manuscripts (their sections on rational source normalization).

def OAI.ContinuumCoulomb.pauliX line 24
def OAI.ContinuumCoulomb.pauliY line 26
def OAI.ContinuumCoulomb.pauliZ line 28
def OAI.ContinuumCoulomb.twoSpinTensor line 31
Source documentation
Tensor product written in the fixed four-state computational basis.
```
def twoSpinTensor (A B : Matrix (Fin 2) (Fin 2) ℂ) :
    Matrix (Fin 4) (Fin 4) ℂ :=
…
```
def OAI.ContinuumCoulomb.heisenberg line 39
Source documentation
The spin-1/2 isotropic Heisenberg matrix in the computational basis.
```
def heisenberg : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.heisenberg_eq_pauli line 45
def OAI.ContinuumCoulomb.twoSpinSwap line 53
Source documentation
Exchange of the two spin coordinates in the computational basis.
```
def twoSpinSwap : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.heisenberg_eq_two_swap_sub_one line 59
theorem OAI.ContinuumCoulomb.heisenberg_mulVec line 65
def OAI.ContinuumCoulomb.spinSinglet line 72
Source documentation
The unnormalized singlet, of squared norm two.
```
def spinSinglet : Fin 4 → ℂ := ![0, 1, -1, 0]
```
def OAI.ContinuumCoulomb.spinTripletUp line 74
def OAI.ContinuumCoulomb.spinTripletZero line 77
Source documentation
The unnormalized zero-magnetization triplet, of squared norm two.
```
def spinTripletZero : Fin 4 → ℂ := ![0, 1, 1, 0]
```
def OAI.ContinuumCoulomb.spinTripletDown line 79
theorem OAI.ContinuumCoulomb.heisenberg_singlet line 81
theorem OAI.ContinuumCoulomb.heisenberg_triplet_up line 87
theorem OAI.ContinuumCoulomb.heisenberg_triplet_zero line 93
theorem OAI.ContinuumCoulomb.heisenberg_triplet_down line 99
theorem OAI.ContinuumCoulomb.spin_singlet_triplet_decomposition line 106
Source documentation
Every spin vector decomposes explicitly into its singlet and triplets.
```
theorem spin_singlet_triplet_decomposition (u : Fin 4 → ℂ) :
    u = u 0 • spinTripletUp + ((u 1 + u 2) / 2) • spinTripletZero +
      ((u 1 - u 2) / 2) • spinSinglet + u 3 • spinTripletDown := by
…
```
Mentions: OAI.ContinuumCoulomb.spinTripletUp, OAI.ContinuumCoulomb.spinTripletZero, OAI.ContinuumCoulomb.spinSinglet, OAI.ContinuumCoulomb.spinTripletDown
def OAI.ContinuumCoulomb.twoSpinNormSq line 114
def OAI.ContinuumCoulomb.twoSpinEnergy line 116
theorem OAI.ContinuumCoulomb.twoSpinNormSq_nonneg line 119
theorem OAI.ContinuumCoulomb.twoSpinEnergy_upper_identity line 123
Source documentation
The upper form bound follows from the antisymmetric component.
```
theorem twoSpinEnergy_upper_identity (u : Fin 4 → ℂ) :
    twoSpinNormSq u - twoSpinEnergy u = 2 * Complex.normSq (u 1 - u 2) := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinNormSq, OAI.ContinuumCoulomb.twoSpinEnergy
theorem OAI.ContinuumCoulomb.twoSpinEnergy_lower_identity line 130
Source documentation
The lower form bound follows from the symmetric components.
```
theorem twoSpinEnergy_lower_identity (u : Fin 4 → ℂ) :
    twoSpinEnergy u + 3 * twoSpinNormSq u =
      4 * Complex.normSq (u 0) + 2 * Complex.normSq (u 1 + u 2) +
        4 * Complex.normSq (u 3) := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinEnergy, OAI.ContinuumCoulomb.twoSpinNormSq
theorem OAI.ContinuumCoulomb.twoSpinEnergy_le line 138
theorem OAI.ContinuumCoulomb.twoSpinEnergy_ge line 144
theorem OAI.ContinuumCoulomb.twoSpinEnergy_abs_le line 154
Source documentation
The interaction quadratic form has absolute value at most three times the squared norm. The singlet attains the lower endpoint.
```
theorem twoSpinEnergy_abs_le (u : Fin 4 → ℂ) :
    |twoSpinEnergy u| ≤ 3 * twoSpinNormSq u := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinEnergy, OAI.ContinuumCoulomb.twoSpinNormSq
theorem OAI.ContinuumCoulomb.spinSinglet_normSq line 163
theorem OAI.ContinuumCoulomb.spinSinglet_energy line 166
theorem OAI.ContinuumCoulomb.heisenberg_coefficient_error line 170
Source documentation
The coefficient-rounding estimate on a normalized two-spin state.
```
theorem heisenberg_coefficient_error
    (J K : ℝ) (u : Fin 4 → ℂ) (hu : twoSpinNormSq u = 1) :
    |J * twoSpinEnergy u - K * twoSpinEnergy u| ≤ 3 * |J - K| := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinNormSq, OAI.ContinuumCoulomb.twoSpinEnergy
theorem OAI.ContinuumCoulomb.heisenberg_spectator_form_bound line 183
Source documentation
A two-spin interaction tensored with any finite spectator space has the same form bound. The vector can be entangled with the spectators.
```
theorem heisenberg_spectator_form_bound
    {ι : Type*} [Fintype ι] (u : ι → Fin 4 → ℂ) :
    |∑ k, twoSpinEnergy (u k)| ≤ 3 * ∑ k, twoSpinNormSq (u k) := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinEnergy, OAI.ContinuumCoulomb.twoSpinNormSq
theorem OAI.ContinuumCoulomb.heisenberg_spectator_coefficient_error line 195
Source documentation
The coefficient-rounding bound remains valid on a normalized state with arbitrary entanglement with the remaining spins.
```
theorem heisenberg_spectator_coefficient_error
    {ι : Type*} [Fintype ι] (J K : ℝ) (u : ι → Fin 4 → ℂ)
    (hu : ∑ k, twoSpinNormSq (u k) = 1) :
    |J * (∑ k, twoSpinEnergy (u k)) - K * (∑ k, twoSpinEnergy (u k))| ≤
      3 * |J - K| := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinNormSq, OAI.ContinuumCoulomb.twoSpinEnergy
theorem OAI.ContinuumCoulomb.heisenberg_edge_rounding line 211
Source documentation
Sum of coefficient errors for all source edges. For each edge, u e is the common state reindexed into its two interacting spins and all spectators. No product-state assumption is made.
```
theorem heisenberg_edge_rounding
    {κ ι : Type*} [Fintype κ] [Fintype ι]
    (J K : κ → ℝ) (u : κ → ι → Fin 4 → ℂ)
    (hu : ∀ e, ∑ k, twoSpinNormSq (u e k) = 1) :
    |∑ e, (J e - K e) * (∑ k, twoSpinEnergy (u e k))| ≤
      3 * ∑ e, |J e - K e| := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSpinNormSq, OAI.ContinuumCoulomb.twoSpinEnergy

theorem OAI.ContinuumCoulomb.heisenberg_source_rounding line 229

Source documentation

The manuscripts' per-edge rounding budget gives total form error 3ε.

theorem heisenberg_source_rounding
    {κ ι : Type*} [Fintype κ] [Fintype ι]
    (J K : κ → ℝ) (u : κ → ι → Fin 4 → ℂ) {ε : ℝ}
    (hε : 0 ≤ ε) (hu : ∀ e, ∑ k, twoSpinNormSq (u e k) = 1)
    (hcoeff : ∀ e, |J e - K e| ≤ ε / (max 1 (Fintype.card κ) : ℕ)) :
    |∑ e, (J e - K e) * (∑ k, twoSpinEnergy (u e k))| ≤ 3 * ε := by
…

Mentions: OAI.ContinuumCoulomb.twoSpinNormSq, OAI.ContinuumCoulomb.twoSpinEnergy