MediatorForms.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Full simultaneous-mediator quadratic forms and their exact effective matrix.

theorem OAI.ContinuumCoulomb.spinMatrixOperator_zero line 12
theorem OAI.ContinuumCoulomb.spinMatrixOperator_sub line 17
theorem OAI.ContinuumCoulomb.spinMatrixOperator_real_symmetric line 22
theorem OAI.ContinuumCoulomb.actualMediatorLowBlock_eq line 30
theorem OAI.ContinuumCoulomb.mediatorLowRestriction_spokes_low line 37
theorem OAI.ContinuumCoulomb.mediatorHighInclusion_coupling line 47
Source documentation
Hopping a singlet-sector state creates only actual mediator excitations.
```
theorem mediatorHighInclusion_coupling (n r : ℕ) (left right : Fin r → Fin n)
    (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) (p : MediatorLowSpace n) :
    mediatorHighInclusion n r (actualMediatorCoupling n r left right member amplitude p) =
      spinMatrixOperator (totalMediatorSpokes n r left right member amplitude)
        (mediatorLowInclusion n r p) := by
…
```
Mentions: OAI.ContinuumCoulomb.MediatorLowSpace, OAI.ContinuumCoulomb.mediatorHighInclusion, OAI.ContinuumCoulomb.actualMediatorCoupling, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.totalMediatorSpokes, OAI.ContinuumCoulomb.mediatorLowInclusion
def OAI.ContinuumCoulomb.bellMediatorPenaltyMatrix line 60
theorem OAI.ContinuumCoulomb.bellMediatorPenalty_low line 64
theorem OAI.ContinuumCoulomb.bellMediatorPenalty_high line 74

def OAI.ContinuumCoulomb.bellMediatorHamiltonian line 89

Source documentation

The actual full matrix in the complete Bell-coordinate spin space.

def bellMediatorHamiltonian (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) :
    Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ :=
…

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

theorem OAI.ContinuumCoulomb.actualMediator_effectiveForm line 97

Source documentation

Exact effective quadratic form for every entangled original-spin vector.

theorem actualMediator_effectiveForm (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ)
    (p : MediatorLowSpace n) :
    Perturbation.effectiveForm (actualMediatorLowBlock n r C)
      (diagonalPenalty (fun s => (actualMediatorWeight n r Delta s)⁻¹))
      (actualMediatorCoupling n r left right member amplitude) p =
      ⟪p, spinMatrixOperator (C - mediatorCompression n r
        (totalMediatorSpokes n r left right member amplitude * liftedMediatorInverse n r Delta *
          totalMediatorSpokes n r left right member amplitude)) p⟫_ℝ := by
…

Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.MediatorLowSpace, OAI.ContinuumCoulomb.Perturbation.effectiveForm, OAI.ContinuumCoulomb.actualMediatorLowBlock, OAI.ContinuumCoulomb.diagonalPenalty, OAI.ContinuumCoulomb.actualMediatorWeight, OAI.ContinuumCoulomb.actualMediatorCoupling, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.totalMediatorSpokes, OAI.ContinuumCoulomb.liftedMediatorInverse

theorem OAI.ContinuumCoulomb.bellMediatorHamiltonian_form_blocks line 142

Source documentation

Full-state quadratic-form equality for the concrete low/high blocks.

theorem bellMediatorHamiltonian_form_blocks (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) (hC : C.conjTranspose = C)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ)
    (p : MediatorLowSpace n) (q : MediatorHighSpace n r) :
    ⟪assembleMediator n r p q,
      spinMatrixOperator (bellMediatorHamiltonian n r Delta C left right member amplitude)
        (assembleMediator n r p q)⟫_ℝ =
      Perturbation.lowBlockEnergy (actualMediatorLowBlock n r C)
        (diagonalPenalty (actualMediatorWeight n r Delta))
        (actualMediatorHighBlock n r C left right member amplitude)
        (actualMediatorCoupling n r left right member amplitude) p q := by
…