Singlet.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Exact singlet mediator calculations

The positive-spin conversion uses the singlet mediator of Piddock–Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, Quantum Information and Computation 17 (2017), Section 2.4 and Lemma 5. The Pauli contractions and penalty identities use an unnormalized singlet vector, whose expectation values are twice the normalized values.

def OAI.ContinuumCoulomb.pauli line 22
def OAI.ContinuumCoulomb.firstPauli line 25
def OAI.ContinuumCoulomb.secondPauli line 28
def OAI.ContinuumCoulomb.singletMatrixElement line 32
Source documentation
Matrix element in the singlet of squared norm two.
```
def singletMatrixElement (A : Matrix (Fin 4) (Fin 4) ℂ) : ℂ :=
…
```
theorem OAI.ContinuumCoulomb.singlet_first_pauli line 35
theorem OAI.ContinuumCoulomb.singlet_second_pauli line 42
theorem OAI.ContinuumCoulomb.singlet_first_first line 50
Source documentation
Same-member singlet contraction: normalized value δμν.
```
theorem singlet_first_first (μ ν : Fin 3) :
    singletMatrixElement (firstPauli μ * firstPauli ν) =
      if μ = ν then 2 else 0 := by
…
```
Mentions: OAI.ContinuumCoulomb.singletMatrixElement, OAI.ContinuumCoulomb.firstPauli
theorem OAI.ContinuumCoulomb.singlet_second_second line 59
Source documentation
Same-member singlet contraction on the other mediator.
```
theorem singlet_second_second (μ ν : Fin 3) :
    singletMatrixElement (secondPauli μ * secondPauli ν) =
      if μ = ν then 2 else 0 := by
…
```
Mentions: OAI.ContinuumCoulomb.singletMatrixElement, OAI.ContinuumCoulomb.secondPauli
theorem OAI.ContinuumCoulomb.singlet_first_second line 68
Source documentation
Opposite-member singlet contraction: normalized value -δμν.
```
theorem singlet_first_second (μ ν : Fin 3) :
    singletMatrixElement (firstPauli μ * secondPauli ν) =
      if μ = ν then -2 else 0 := by
…
```
Mentions: OAI.ContinuumCoulomb.singletMatrixElement, OAI.ContinuumCoulomb.firstPauli, OAI.ContinuumCoulomb.secondPauli
theorem OAI.ContinuumCoulomb.singlet_second_first line 76
def OAI.ContinuumCoulomb.singletProjector line 85
Source documentation
Orthogonal projection onto the one-dimensional singlet space.
```
def singletProjector : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.singletProjector_idempotent line 91
theorem OAI.ContinuumCoulomb.singletProjector_singlet line 97
theorem OAI.ContinuumCoulomb.singlet_penalty_eq line 104
Source documentation
The mediator excitation penalty is exactly four times the triplet projection.
```
theorem singlet_penalty_eq :
    heisenberg + (3 : ℂ) • (1 : Matrix (Fin 4) (Fin 4) ℂ) =
      (4 : ℂ) • (1 - singletProjector) := by
…
```
Mentions: OAI.ContinuumCoulomb.heisenberg, OAI.ContinuumCoulomb.singletProjector
theorem OAI.ContinuumCoulomb.singletProjector_first_pauli line 112
Source documentation
Each Pauli action takes the singlet orthogonally to its kernel space.
```
theorem singletProjector_first_pauli (μ : Fin 3) :
    singletProjector *ᵥ (firstPauli μ *ᵥ spinSinglet) = 0 := by
…
```
Mentions: OAI.ContinuumCoulomb.singletProjector, OAI.ContinuumCoulomb.firstPauli, OAI.ContinuumCoulomb.spinSinglet
theorem OAI.ContinuumCoulomb.singletProjector_second_pauli line 120
theorem OAI.ContinuumCoulomb.firstPauli_sq line 128
theorem OAI.ContinuumCoulomb.secondPauli_sq line 133
theorem OAI.ContinuumCoulomb.first_second_pauli line 138
theorem OAI.ContinuumCoulomb.second_first_pauli line 144
theorem OAI.ContinuumCoulomb.sum_first_second_pauli line 150
theorem OAI.ContinuumCoulomb.sum_second_first_pauli line 156
def OAI.ContinuumCoulomb.otherMediatorPauli line 163
Source documentation
The second mediator spoke can meet the same or the opposite member.
```
def otherMediatorPauli (opposite : Bool) (μ : Fin 3) :
    Matrix (Fin 4) (Fin 4) ℂ :=
…
```
def OAI.ContinuumCoulomb.mediatorContraction line 170
Source documentation
Compression of the square of the two-spoke coupling to the normalized mediator singlet. The first matrix factors act on the external pair; the matrix elements contract the mediator pair.
```
def mediatorContraction (opposite : Bool) : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.mediatorContraction_same line 182
theorem OAI.ContinuumCoulomb.mediatorContraction_opposite line 198
def OAI.ContinuumCoulomb.mediatorSecondOrder line 218
Source documentation
The inverse of the unit mediator penalty is 1/4 on the excited space, and every spoke takes the singlet there. The contraction hence has the negative second-order prefactor -v²/4.
```
def mediatorSecondOrder (opposite : Bool) (v : ℝ) : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.mediatorSecondOrder_same line 221
theorem OAI.ContinuumCoulomb.mediatorSecondOrder_opposite line 232