OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/GlobalSinglet.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Canonical singlet/triplet coordinates for simultaneous fresh mediator pairs.

  1. theorem OAI.ContinuumCoulomb.bellScale_atLeastTwo line 17

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:194 (same declaration text).

  2. def OAI.ContinuumCoulomb.bellScale line 22

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:199 (same declaration text).

  3. theorem OAI.ContinuumCoulomb.bellScale_sq line 26
  4. theorem OAI.ContinuumCoulomb.bellScale_star line 31
  5. def OAI.ContinuumCoulomb.bellRaw line 34
  6. def OAI.ContinuumCoulomb.bellMatrix line 37
  7. theorem OAI.ContinuumCoulomb.bellRaw_gram line 39
  8. theorem OAI.ContinuumCoulomb.bellRaw_cogram line 45
  9. theorem OAI.ContinuumCoulomb.bellScale_twice_sq line 51
  10. theorem OAI.ContinuumCoulomb.bellMatrix_gram line 56
  11. theorem OAI.ContinuumCoulomb.bellMatrix_cogram line 60
  12. theorem OAI.ContinuumCoulomb.bellMatrix_singlet line 64
  13. theorem OAI.ContinuumCoulomb.bellRaw_heisenberg line 67
  14. theorem OAI.ContinuumCoulomb.bellMatrix_heisenberg line 73
  15. def OAI.ContinuumCoulomb.bellTransform line 77
  16. theorem OAI.ContinuumCoulomb.bellTransform_mul line 80
  17. theorem OAI.ContinuumCoulomb.bellTransform_zero_zero line 90

    Source documentation

    The transformed zero coordinate is the actual normalized singlet matrix element, including the normalization factor one half.

    theorem bellTransform_zero_zero (M : Matrix (Fin 4) (Fin 4) ℂ) :
    bellTransform M 0 0 = (1 / 2 : ℂ) * singletMatrixElement M := by
…

    Mentions: OAI.ContinuumCoulomb.bellTransform, OAI.ContinuumCoulomb.singletMatrixElement

  18. theorem OAI.ContinuumCoulomb.bell_first_pauli_zero line 103
  19. theorem OAI.ContinuumCoulomb.bell_second_pauli_zero line 106
  20. theorem OAI.ContinuumCoulomb.bell_first_first_zero line 109
  21. theorem OAI.ContinuumCoulomb.bell_first_second_zero line 115
  22. abbrev OAI.ContinuumCoulomb.MediatorBasis line 121
  23. def OAI.ContinuumCoulomb.globalBellMatrix line 123
  24. theorem OAI.ContinuumCoulomb.bell_column_inner line 126
  25. theorem OAI.ContinuumCoulomb.bell_row_inner line 131
  26. theorem OAI.ContinuumCoulomb.product_delta line 136
  27. theorem OAI.ContinuumCoulomb.globalBellMatrix_gram line 148

    Source documentation

    The tensor product of all local Bell changes of coordinates is unitary for every number of simultaneous mediators.

    theorem globalBellMatrix_gram (r : ℕ) :
    (globalBellMatrix r).conjTranspose * globalBellMatrix r = 1 := by
…

    Mentions: OAI.ContinuumCoulomb.globalBellMatrix

  28. theorem OAI.ContinuumCoulomb.globalBellMatrix_cogram line 157
  29. def OAI.ContinuumCoulomb.mediatorVacuum line 166
  30. def OAI.ContinuumCoulomb.mediatorExcitationNumber line 168
  31. theorem OAI.ContinuumCoulomb.mediatorExcitationNumber_pos line 171
  32. def OAI.ContinuumCoulomb.mediatorPenaltyWeight line 176
  33. abbrev OAI.ContinuumCoulomb.MediatorHighBasis line 179
  34. theorem OAI.ContinuumCoulomb.mediatorPenalty_inverse_data line 183

    Source documentation

    The actual diagonal excitation penalty has gap four Delta and its explicit inverse is bounded by the reciprocal gap.

    theorem mediatorPenalty_inverse_data (r : ℕ) {Delta : ℝ} (hDelta : 0 < Delta) :
    let weight : MediatorHighBasis r → ℝ := fun a => mediatorPenaltyWeight r Delta a.val
…

    Mentions: OAI.ContinuumCoulomb.MediatorHighBasis, OAI.ContinuumCoulomb.mediatorPenaltyWeight