HubbardGlobal.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Global finite-fermion identities for the Hubbard reduction

These are identities of actual creation and contraction operators on the finite exterior algebra. They retain every spectator mode and therefore do not assume transition signs from the two-site calculation.

def OAI.ContinuumCoulomb.HubbardGlobal.transfer line 24
def OAI.ContinuumCoulomb.HubbardGlobal.number line 27
def OAI.ContinuumCoulomb.HubbardGlobal.totalNumber line 29
theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_mul line 31
theorem OAI.ContinuumCoulomb.HubbardGlobal.quartic_exchange line 37
theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_commutator line 48
Source documentation
The matrix-unit commutator, proved from the full CAR operators.
```
theorem transfer_commutator (i j k l : Fin (Q + 1)) :
    transfer i j * transfer k l - transfer k l * transfer i j =
      delta j k • transfer i l - delta l i • transfer k j := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.transfer
theorem OAI.ContinuumCoulomb.HubbardGlobal.number_idempotent line 54
theorem OAI.ContinuumCoulomb.HubbardGlobal.number_commute line 59
theorem OAI.ContinuumCoulomb.HubbardGlobal.number_transfer_commutator line 66
theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_number_self line 75
theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_number_commute line 84
theorem OAI.ContinuumCoulomb.HubbardGlobal.pair_annihilate_siteNumber line 95
theorem OAI.ContinuumCoulomb.HubbardGlobal.pair_annihilate_of_single line 112
Source documentation
Local particle number one rules out a pair annihilation, directly from the CAR; no occupation-basis or sign assumption is needed.
```
theorem pair_annihilate_of_single (i j : Fin (Q + 1)) (hij : i ≠ j)
    (x : Space Q) (hx : (number i + number j) x = x) :
    (annihilate i * annihilate j) x = 0 := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.number
theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_commute_of_distinct line 123
theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_sq_of_ne line 128
theorem OAI.ContinuumCoulomb.HubbardGlobal.quartic_number line 133
theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_reverse_product line 146
def OAI.ContinuumCoulomb.HubbardGlobal.bondTransfer line 151
theorem OAI.ContinuumCoulomb.HubbardGlobal.bondTransfer_sq line 154
theorem OAI.ContinuumCoulomb.HubbardGlobal.transfer_exchange line 167
Source documentation
A two-transfer exchange identity before imposing occupation constraints. It is independent of every spectator mode.
```
theorem transfer_exchange (i j k l : Fin (Q + 1))
    (hjk : j ≠ k) (hlk : l ≠ k) :
    transfer i j * transfer k l = -(transfer i l * transfer k j) := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.transfer
theorem OAI.ContinuumCoulomb.HubbardGlobal.bondTransfer_commute line 177
def OAI.ContinuumCoulomb.HubbardGlobal.spinSwap line 185
def OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping line 189

theorem OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping_sq line 194

Source documentation

The full hopping-square identity. The final two terms are the pair hops, which vanish on singly occupied sites.

theorem twoSiteHopping_sq (a b c d : Fin (Q + 1))
    (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d)
    (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) :
    twoSiteHopping a b c d * twoSiteHopping a b c d =
      number a + number b + number c + number d - (2 : ℂ) • spinSwap a b c d -
        (2 : ℂ) • (create a * create b * annihilate c * annihilate d +
          create c * create d * annihilate a * annihilate b) := by
…

Mentions: OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping, OAI.ContinuumCoulomb.HubbardGlobal.number, OAI.ContinuumCoulomb.HubbardGlobal.spinSwap

def OAI.ContinuumCoulomb.HubbardGlobal.siteHeisenberg line 221

theorem OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping_sq_on_singlyOccupied line 226

Source documentation

The occupied-sector second-order numerator, on a genuine Fock vector with arbitrary spectators and local particle number one.

theorem twoSiteHopping_sq_on_singlyOccupied (a b c d : Fin (Q + 1))
    (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d)
    (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d)
    (x : Space Q)
    (hleft : (number a + number b) x = x)
    (hright : (number c + number d) x = x) :
    (twoSiteHopping a b c d * twoSiteHopping a b c d) x =
      (1 - siteHeisenberg a b c d) x := by
…

Mentions: OAI.ContinuumCoulomb.HubbardGlobal.number, OAI.ContinuumCoulomb.HubbardGlobal.twoSiteHopping, OAI.ContinuumCoulomb.HubbardGlobal.siteHeisenberg

theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_commute_transfer line 256
Source documentation
Every one-particle transfer preserves the total fermion number.
```
theorem totalNumber_commute_transfer (i j : Fin (Q + 1)) :
    Commute (totalNumber Q) (transfer i j) := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.totalNumber, OAI.ContinuumCoulomb.HubbardGlobal.transfer
def OAI.ContinuumCoulomb.HubbardGlobal.oneBody line 265
def OAI.ContinuumCoulomb.HubbardGlobal.densityInteraction line 268
theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_commute_oneBody line 271
theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_commute_densityInteraction line 280
theorem OAI.ContinuumCoulomb.HubbardGlobal.preserves_number_sector line 293
Source documentation
The actual hopping-plus-density Hamiltonian preserves every fixed particle-number sector, including the half-filled sector used here.
```
theorem preserves_number_sector (w v : Fin (Q + 1) → Fin (Q + 1) → ℂ)
    (x : Space Q) (N : ℂ) (hx : totalNumber Q x = N • x) :
    totalNumber Q ((oneBody w + densityInteraction v) x) =
      N • ((oneBody w + densityInteraction v) x) := by
…
```
Mentions: OAI.ContinuumCoulomb.HubbardGlobal.totalNumber, OAI.ContinuumCoulomb.HubbardGlobal.oneBody, OAI.ContinuumCoulomb.HubbardGlobal.densityInteraction