GlobalSuperexchange.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact global Hubbard second-order compression on the spin sector.

def OAI.ContinuumCoulomb.HubbardGlobal.graphHopping line 14

theorem OAI.ContinuumCoulomb.HubbardGlobal.hopping_inverse_graphHopping_spinWedge line 18

Source documentation

Only the matching graph edge survives an inverse compression.

theorem hopping_inverse_graphHopping_spinWedge (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (left right : Edge → Fin (m + 1)) (t : Edge → ℂ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (s : SourceSpinBasis (m + 1)) (e : Edge) :
    lowProjection m (siteHopping m (left e) (right e)
      (chargeInverse m U V (graphHopping m left right t (spinWedge m s)))) =
        t e • (((U - V (left e) (right e))⁻¹ : ℝ) : ℂ) •
          ((2 : ℂ) • (spinWedge m s - spinWedge m (sourceSpinSwap (left e) (right e) s))) := by
…

Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.lowProjection, OAI.ContinuumCoulomb.HubbardGlobal.siteHopping, OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.graphHopping, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge, OAI.ContinuumCoulomb.sourceSpinSwap

theorem OAI.ContinuumCoulomb.HubbardGlobal.graphHopping_inverse_graphHopping_spinWedge line 43

Source documentation

The actual global inverse compression is the sum of the local exchange terms, with the Coulomb-corrected denominator on every edge.

theorem graphHopping_inverse_graphHopping_spinWedge (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (left right : Edge → Fin (m + 1)) (t : Edge → ℂ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (s : SourceSpinBasis (m + 1)) :
    lowProjection m (graphHopping m left right t
      (chargeInverse m U V (graphHopping m left right t (spinWedge m s)))) =
        ∑ e, t e ^ 2 • (((U - V (left e) (right e))⁻¹ : ℝ) : ℂ) •
          ((2 : ℂ) • (spinWedge m s - spinWedge m (sourceSpinSwap (left e) (right e) s))) := by
…

Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.lowProjection, OAI.ContinuumCoulomb.HubbardGlobal.graphHopping, OAI.ContinuumCoulomb.HubbardGlobal.chargeInverse, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge, OAI.ContinuumCoulomb.sourceSpinSwap

theorem OAI.ContinuumCoulomb.HubbardGlobal.graphSuperexchange_calibrated line 66

Source documentation

Choosing t_e² = J_e (U-V_e) gives the genuine Heisenberg inverse term, including the scalar -J_e I on every edge.

theorem graphSuperexchange_calibrated (m : ℕ) (U : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hdiag : ∀ i, V i i = 0)
    (left right : Edge → Fin (m + 1)) (t J : Edge → ℂ)
    (hloop : ∀ e, left e ≠ right e)
    (hsimple : ∀ e f, e ≠ f →
      ¬(left e = left f ∧ right e = right f) ∧ ¬(left e = right f ∧ right e = left f))
    (hgap : ∀ e, U - V (left e) (right e) ≠ 0)
    (hcal : ∀ e, t e ^ 2 = J e * ((U - V (left e) (right e) : ℝ) : ℂ))
    (s : SourceSpinBasis (m + 1)) :
    -(lowProjection m (graphHopping m left right t
      (chargeInverse m U V (graphHopping m left right t (spinWedge m s))))) =
…