OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorEffective.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Exact effective matrices for simultaneous singlet mediators, on the complete original-spin Hilbert space.

  1. abbrev OAI.ContinuumCoulomb.MediatedSpinBasis line 15
  2. def OAI.ContinuumCoulomb.mediatorCompression line 18

    Source documentation

    Restriction to original spins tensored with all mediator singlets.

    def mediatorCompression (n r : ℕ) :
    Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ →ₗ[ℂ]
      Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ where
…

    Mentions: OAI.ContinuumCoulomb.MediatedSpinBasis, OAI.ContinuumCoulomb.SourceSpinBasis

  3. theorem OAI.ContinuumCoulomb.mediatorCompression_kronecker line 25
  4. def OAI.ContinuumCoulomb.liftedMediatorInverse line 35
  5. def OAI.ContinuumCoulomb.elementaryMediatorSpoke line 39
  6. theorem OAI.ContinuumCoulomb.elementaryMediatorSpoke_compression line 46

    Source documentation

    Fresh-pair cancellation with arbitrary original-spin operators. This is a matrix identity and therefore covers entangled original states.

    theorem elementaryMediatorSpoke_compression (n r : ℕ) (Delta : ℝ) (e f : Fin r)
    (member other : Fin 2) (μ ν : Fin 3)
    (A B : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) :
    mediatorCompression n r
      (elementaryMediatorSpoke n r e member μ A * liftedMediatorInverse n r Delta *
        elementaryMediatorSpoke n r f other ν B) =
      if e = f ∧ μ = ν then
        (((4 * Delta)⁻¹ : ℝ) * (if member = other then (1 : ℂ) else -1)) • (A * B)
      else 0 := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.elementaryMediatorSpoke, OAI.ContinuumCoulomb.liftedMediatorInverse

  7. def OAI.ContinuumCoulomb.mediatorEdgeSpoke line 62

    Source documentation

    The two physical spokes incident to one original edge. The left spoke uses the first mediator member; the right can use either member.

    def mediatorEdgeSpoke (n r : ℕ) (e : Fin r) (i j : Fin n) (member : Fin 2) :
    Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ :=
…

    Mentions: OAI.ContinuumCoulomb.MediatedSpinBasis

  8. theorem OAI.ContinuumCoulomb.mediatorEdgeSpoke_cross_compression line 68
  9. def OAI.ContinuumCoulomb.mediatorAxisSpoke line 79
  10. theorem OAI.ContinuumCoulomb.mediatorAxisSpoke_compression line 83
  11. theorem OAI.ContinuumCoulomb.mediatorEdgeSpoke_as_add line 101
  12. def OAI.ContinuumCoulomb.mediatorMemberSign line 107
  13. theorem OAI.ContinuumCoulomb.mediatorEdgeSpoke_self_compression line 110

    Source documentation

    Exact two-spoke self-energy, including the scalar shift six/(four Delta).

    theorem mediatorEdgeSpoke_self_compression (n r : ℕ) (Delta : ℝ) (e : Fin r)
    (i j : Fin n) (hij : i ≠ j) (member : Fin 2) :
    mediatorCompression n r
      (mediatorEdgeSpoke n r e i j member * liftedMediatorInverse n r Delta *
        mediatorEdgeSpoke n r e i j member) =
      (((4 * Delta)⁻¹ : ℝ) : ℂ) •
        ((6 : ℂ) • 1 + (2 * mediatorMemberSign member) • sourceHeisenbergMatrix n i j) := by
…

    Mentions: OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.mediatorEdgeSpoke, OAI.ContinuumCoulomb.liftedMediatorInverse, OAI.ContinuumCoulomb.mediatorMemberSign, OAI.ContinuumCoulomb.sourceHeisenbergMatrix

  14. theorem OAI.ContinuumCoulomb.mediatorEdgeSpoke_compression line 139
  15. def OAI.ContinuumCoulomb.totalMediatorSpokes line 157
  16. theorem OAI.ContinuumCoulomb.totalMediatorSpokes_compression line 163

    Source documentation

    The simultaneous second-order matrix contains no cross-edge terms.

    theorem totalMediatorSpokes_compression (n r : ℕ) (Delta : ℝ)
    (left right : Fin r → Fin n) (hneq : ∀ e, left e ≠ right e)
    (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) :
    mediatorCompression n r
      (totalMediatorSpokes n r left right member amplitude * liftedMediatorInverse n r Delta *
        totalMediatorSpokes n r left right member amplitude) =
      ∑ e, ((amplitude e : ℂ) ^ 2 * ((4 * Delta)⁻¹ : ℝ)) •
        ((6 : ℂ) • 1 + (2 * mediatorMemberSign (member e)) •
          sourceHeisenbergMatrix n (left e) (right e)) := by
…

    Mentions: OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.totalMediatorSpokes, OAI.ContinuumCoulomb.liftedMediatorInverse, OAI.ContinuumCoulomb.mediatorMemberSign, OAI.ContinuumCoulomb.sourceHeisenbergMatrix

  17. def OAI.ContinuumCoulomb.signedMediatorMember line 182
  18. def OAI.ContinuumCoulomb.signedMediatorAmplitude line 184
  19. theorem OAI.ContinuumCoulomb.signedMediatorAmplitude_nonneg line 186
  20. theorem OAI.ContinuumCoulomb.signedMediatorAmplitude_calibration line 189
  21. theorem OAI.ContinuumCoulomb.calibratedMediator_edge line 195

    Source documentation

    The exact manuscript calibration, with the constant self-energy retained.

    theorem calibratedMediator_edge {Delta amplitude J : ℝ} (hDelta : 0 < Delta)
    (hcal : amplitude ^ 2 = 2 * Delta * |J|)
    {n : ℕ} (i j : Fin n) :
    ((amplitude : ℂ) ^ 2 * ((4 * Delta)⁻¹ : ℝ)) •
      ((6 : ℂ) • 1 + (2 * mediatorMemberSign (signedMediatorMember J)) •
        sourceHeisenbergMatrix n i j) =
      (3 * |J| : ℝ) • (1 : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) -
        (J : ℂ) • sourceHeisenbergMatrix n i j := by
…

    Mentions: OAI.ContinuumCoulomb.mediatorMemberSign, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.sourceHeisenbergMatrix, OAI.ContinuumCoulomb.SourceSpinBasis

  22. theorem OAI.ContinuumCoulomb.signedMediator_effective_matrix line 231

    Source documentation

    Exact signed-source simulation at second order for all original-spin states. Unreplaced terms survive as the explicit low block C.

    theorem signedMediator_effective_matrix (n r : ℕ) {Delta : ℝ} (hDelta : 0 < Delta)
    (left right : Fin r → Fin n) (hneq : ∀ e, left e ≠ right e)
    (J amplitude : Fin r → ℝ) (hcal : ∀ e, amplitude e ^ 2 = 2 * Delta * |J e|)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) :
    C - mediatorCompression n r
      (totalMediatorSpokes n r left right (fun e => signedMediatorMember (J e)) amplitude *
        liftedMediatorInverse n r Delta *
        totalMediatorSpokes n r left right (fun e => signedMediatorMember (J e)) amplitude) =
      C + (∑ e, (J e : ℂ) • sourceHeisenbergMatrix n (left e) (right e)) -
        (3 * ∑ e, |J e| : ℝ) • 1 := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.totalMediatorSpokes, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.liftedMediatorInverse, OAI.ContinuumCoulomb.sourceHeisenbergMatrix

  23. def OAI.ContinuumCoulomb.physicalMemberPauli line 252
  24. theorem OAI.ContinuumCoulomb.physicalMemberPauli_transform line 255
  25. def OAI.ContinuumCoulomb.fullMediatorBellMatrix line 260
  26. theorem OAI.ContinuumCoulomb.fullMediatorBellMatrix_gram line 264
  27. theorem OAI.ContinuumCoulomb.fullMediatorBellMatrix_cogram line 271
  28. theorem OAI.ContinuumCoulomb.physicalSpoke_bellTransform line 280

    Source documentation

    The elementary matrices above are precisely Bell transforms of the physical original-spin to mediator-member Pauli interactions.

    theorem physicalSpoke_bellTransform (n r : ℕ) (e : Fin r) (member : Fin 2) (μ : Fin 3)
    (A : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) :
    (fullMediatorBellMatrix n r).conjTranspose *
      (A ⊗ₖ mediatorLocal r e (physicalMemberPauli member μ)) * fullMediatorBellMatrix n r =
      elementaryMediatorSpoke n r e member μ A := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.fullMediatorBellMatrix, OAI.ContinuumCoulomb.mediatorLocal, OAI.ContinuumCoulomb.physicalMemberPauli, OAI.ContinuumCoulomb.elementaryMediatorSpoke

  29. theorem OAI.ContinuumCoulomb.elementaryMediatorSpoke_low_compression line 292
  30. theorem OAI.ContinuumCoulomb.totalMediatorSpokes_low_compression line 299
  31. theorem OAI.ContinuumCoulomb.mediator_first_order_matrix line 307

    Source documentation

    The unreplaced original Hamiltonian survives the low compression exactly.

    theorem mediator_first_order_matrix (n r : ℕ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) :
    mediatorCompression n r
      (C ⊗ₖ 1 + totalMediatorSpokes n r left right member amplitude) = C := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.totalMediatorSpokes