Hubbard.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Two-site Hubbard superexchange

The four canonical fermion modes are L↑, L↓, R↑, R↓, in that order. Creation and annihilation use the parity of occupied modes preceding the acted-on mode. Thus the hopping signs are computed from the canonical fermionic action, rather than assumed as transition amplitudes.

Only the two-electron sector used by the Coulomb reductions is needed. Its first four basis states are singly occupied, followed by the left and right doubly occupied states. The penalty of either virtual excitation is U - v, including the intersite direct Coulomb contribution.

abbrev OAI.ContinuumCoulomb.FourModeOccupation line 29
abbrev OAI.ContinuumCoulomb.FourModeFock line 30
def OAI.ContinuumCoulomb.fermionParity line 32
def OAI.ContinuumCoulomb.createBasis line 35
def OAI.ContinuumCoulomb.annihilateBasis line 38
def OAI.ContinuumCoulomb.fermionCreate line 41
def OAI.ContinuumCoulomb.fermionAnnihilate line 44
theorem OAI.ContinuumCoulomb.fermionCreate_single line 47
theorem OAI.ContinuumCoulomb.fermionAnnihilate_single line 51
def OAI.ContinuumCoulomb.twoElectronOccupation line 55
def OAI.ContinuumCoulomb.twoElectronBasis line 58
def OAI.ContinuumCoulomb.twoSiteHopping line 62
Source documentation
Unit hopping amplitude, with the conventional minus sign.
```
def twoSiteHopping : FourModeFock →ₗ[ℂ] FourModeFock :=
…
```
Mentions: OAI.ContinuumCoulomb.FourModeFock
theorem OAI.ContinuumCoulomb.twoSiteHopping_up_up line 68
theorem OAI.ContinuumCoulomb.twoSiteHopping_up_down line 73
theorem OAI.ContinuumCoulomb.twoSiteHopping_down_up line 81
theorem OAI.ContinuumCoulomb.twoSiteHopping_down_down line 89
theorem OAI.ContinuumCoulomb.twoSiteHopping_double_left line 94
theorem OAI.ContinuumCoulomb.twoSiteHopping_double_right line 101
def OAI.ContinuumCoulomb.twoSiteHoppingMatrix line 110
Source documentation
Matrix of the actual canonical hopping action on the two-electron sector.
```
def twoSiteHoppingMatrix : Matrix (Fin 6) (Fin 6) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.twoSiteHopping_basis line 118
def OAI.ContinuumCoulomb.leftOccupancyDeviation line 128
Source documentation
Occupancy deviation at the left site.
```
def leftOccupancyDeviation (s : FourModeOccupation) : ℝ :=
…
```
Mentions: OAI.ContinuumCoulomb.FourModeOccupation
def OAI.ContinuumCoulomb.rightOccupancyDeviation line 131
def OAI.ContinuumCoulomb.twoSiteOccupancyPenalty line 135
Source documentation
The quadratic Coulomb occupancy penalty before the scalar -v shift.
```
def twoSiteOccupancyPenalty (U v : ℝ) (s : FourModeOccupation) : ℝ :=
…
```
Mentions: OAI.ContinuumCoulomb.FourModeOccupation
theorem OAI.ContinuumCoulomb.twoSiteOccupancyPenalty_basis line 139
def OAI.ContinuumCoulomb.twoSiteHoppingBlock line 147
Source documentation
The hopping block from the singly occupied spin space to virtual pairs.
```
def twoSiteHoppingBlock : Matrix (Fin 4) (Fin 2) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.twoSiteHoppingMatrix_low_block line 150
theorem OAI.ContinuumCoulomb.twoSiteHoppingMatrix_cross_block line 154
theorem OAI.ContinuumCoulomb.twoSiteHoppingBlock_square line 159
def OAI.ContinuumCoulomb.twoSiteSecondOrder line 168
Source documentation
Exact negative second-order compression with excitation cost U-v.
```
def twoSiteSecondOrder (t U v : ℝ) : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.twoSiteSecondOrder_eq line 172
theorem OAI.ContinuumCoulomb.twoSiteSecondOrder_calibrated line 182
Source documentation
The manuscript's hopping calibration gives the required exchange, while the intersite interaction remains in its virtual denominator.
```
theorem twoSiteSecondOrder_calibrated
    {t U v τ K : ℝ} (hgap : U - v ≠ 0)
    (ht : t ^ 2 = τ ^ 2 * K * (U - v)) :
    twoSiteSecondOrder t U v =
      ((τ ^ 2 * K : ℝ) : ℂ) • (heisenberg - 1) := by
…
```
Mentions: OAI.ContinuumCoulomb.twoSiteSecondOrder, OAI.ContinuumCoulomb.heisenberg
def OAI.ContinuumCoulomb.twoSiteInversePenaltyMatrix line 190
Source documentation
The inverse penalty vanishes on the singly occupied kernel.
```
def twoSiteInversePenaltyMatrix (U v : ℝ) : Matrix (Fin 6) (Fin 6) ℂ :=
…
```
def OAI.ContinuumCoulomb.twoSiteCompressedInverseTerm line 194
Source documentation
Compression of the actual six-dimensional negative inverse term.
```
def twoSiteCompressedInverseTerm (t U v : ℝ) : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.twoSiteCompressedInverseTerm_eq line 199