MediatorCompression.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Exact simultaneous singlet-penalty diagonalization and inverse compression. All tensor matrices here act on the complete mediator configuration basis.

def OAI.ContinuumCoulomb.mediatorTensor line 14
Source documentation
Tensor product over the actual four-state mediator pairs.
```
def mediatorTensor (r : ℕ) (M : Fin r → Matrix (Fin 4) (Fin 4) ℂ) :
    Matrix (MediatorBasis r) (MediatorBasis r) ℂ := fun a b => ∏ e, M e (a e) (b e)
```
Mentions: OAI.ContinuumCoulomb.MediatorBasis
theorem OAI.ContinuumCoulomb.mediatorTensor_one line 17
theorem OAI.ContinuumCoulomb.mediatorTensor_mul line 21
theorem OAI.ContinuumCoulomb.mediatorTensor_star line 27
theorem OAI.ContinuumCoulomb.mediatorTensor_diagonal line 32
def OAI.ContinuumCoulomb.mediatorLocal line 45
Source documentation
An operator acting on one actual fresh pair, with identity on all others.
```
def mediatorLocal (r : ℕ) (e : Fin r) (M : Matrix (Fin 4) (Fin 4) ℂ) :
    Matrix (MediatorBasis r) (MediatorBasis r) ℂ :=
…
```
Mentions: OAI.ContinuumCoulomb.MediatorBasis
theorem OAI.ContinuumCoulomb.mediatorLocal_apply line 49
theorem OAI.ContinuumCoulomb.mediatorLocal_vacuum line 62
theorem OAI.ContinuumCoulomb.mediatorLocal_mul_same line 66
theorem OAI.ContinuumCoulomb.mediatorLocal_diagonal line 75
theorem OAI.ContinuumCoulomb.mediatorLocal_bellTransform line 91
Source documentation
Conjugating the actual physical one-pair operator by the global Bell basis gives exactly the same local operator in Bell coordinates.
```
theorem mediatorLocal_bellTransform (r : ℕ) (e : Fin r)
    (M : Matrix (Fin 4) (Fin 4) ℂ) :
    (globalBellMatrix r).conjTranspose * mediatorLocal r e M * globalBellMatrix r =
      mediatorLocal r e (bellTransform M) := by
…
```
Mentions: OAI.ContinuumCoulomb.globalBellMatrix, OAI.ContinuumCoulomb.mediatorLocal, OAI.ContinuumCoulomb.bellTransform
theorem OAI.ContinuumCoulomb.bellTransform_penalty line 106
def OAI.ContinuumCoulomb.physicalMediatorPenalty line 126
Source documentation
The physical central-bond sum, with its singlet scalar shifts.
```
def physicalMediatorPenalty (r : ℕ) (Delta : ℝ) :
    Matrix (MediatorBasis r) (MediatorBasis r) ℂ :=
…
```
Mentions: OAI.ContinuumCoulomb.MediatorBasis
theorem OAI.ContinuumCoulomb.mediatorExcitationNumber_sum line 130
theorem OAI.ContinuumCoulomb.physicalMediatorPenalty_diagonal line 137
Source documentation
Exact diagonalization of the entire simultaneous central Hamiltonian.
```
theorem physicalMediatorPenalty_diagonal (r : ℕ) (Delta : ℝ) :
    (globalBellMatrix r).conjTranspose * physicalMediatorPenalty r Delta * globalBellMatrix r =
      Matrix.diagonal (fun a => (mediatorPenaltyWeight r Delta a : ℂ)) := by
…
```
Mentions: OAI.ContinuumCoulomb.globalBellMatrix, OAI.ContinuumCoulomb.physicalMediatorPenalty, OAI.ContinuumCoulomb.mediatorPenaltyWeight
def OAI.ContinuumCoulomb.mediatorInverseWeight line 160
Source documentation
Full inverse on the triplet complement and zero on the singlet kernel.
```
def mediatorInverseWeight (r : ℕ) (Delta : ℝ) (a : MediatorBasis r) : ℂ :=
…
```
Mentions: OAI.ContinuumCoulomb.MediatorBasis
def OAI.ContinuumCoulomb.mediatorInverseMatrix line 163
theorem OAI.ContinuumCoulomb.mediatorLocal_column_support line 167
theorem OAI.ContinuumCoulomb.mediatorLocal_column_excitation line 182

theorem OAI.ContinuumCoulomb.mediatorInverse_local_column line 208

Source documentation

Every single fresh-pair excitation has the same denominator four Delta.

theorem mediatorInverse_local_column (r : ℕ) (Delta : ℝ) (e : Fin r)
    (N : Matrix (Fin 4) (Fin 4) ℂ) (hN : N 0 0 = 0) (a : MediatorBasis r) :
    mediatorInverseWeight r Delta a * mediatorLocal r e N a (mediatorVacuum r) =
      ((4 * Delta)⁻¹ : ℝ) * mediatorLocal r e N a (mediatorVacuum r) := by
…

Mentions: OAI.ContinuumCoulomb.MediatorBasis, OAI.ContinuumCoulomb.mediatorInverseWeight, OAI.ContinuumCoulomb.mediatorLocal, OAI.ContinuumCoulomb.mediatorVacuum

theorem OAI.ContinuumCoulomb.mediatorLocal_cross_vacuum line 218

theorem OAI.ContinuumCoulomb.mediator_inverse_compression line 231

Source documentation

Exact inverse-compressed contraction. Different fresh pairs cancel; the same pair has the actual excitation denominator four Delta.

theorem mediator_inverse_compression (r : ℕ) (Delta : ℝ) (e f : Fin r)
    (M N : Matrix (Fin 4) (Fin 4) ℂ) (hM : M 0 0 = 0) (hN : N 0 0 = 0) :
    (mediatorLocal r e M * mediatorInverseMatrix r Delta * mediatorLocal r f N)
      (mediatorVacuum r) (mediatorVacuum r) =
      if e = f then ((4 * Delta)⁻¹ : ℝ) * (M * N) 0 0 else 0 := by
…

Mentions: OAI.ContinuumCoulomb.mediatorLocal, OAI.ContinuumCoulomb.mediatorInverseMatrix, OAI.ContinuumCoulomb.mediatorVacuum

theorem OAI.ContinuumCoulomb.bell_second_second_zero line 256
theorem OAI.ContinuumCoulomb.bell_second_first_zero line 262
def OAI.ContinuumCoulomb.bellMemberPauli line 269
Source documentation
Actual Pauli action on either member of a mediator pair in Bell coordinates.
```
def bellMemberPauli (member : Fin 2) (μ : Fin 3) : Matrix (Fin 4) (Fin 4) ℂ :=
…
```
theorem OAI.ContinuumCoulomb.bellMemberPauli_zero line 272
theorem OAI.ContinuumCoulomb.bellMemberPauli_product line 279

theorem OAI.ContinuumCoulomb.mediator_pauli_inverse_compression line 288

Source documentation

The exact global inverse contraction, with arbitrary spectator mediator pairs: different pairs or Pauli axes vanish, and opposite members change sign.

theorem mediator_pauli_inverse_compression (r : ℕ) (Delta : ℝ) (e f : Fin r)
    (member other : Fin 2) (μ ν : Fin 3) :
    (mediatorLocal r e (bellMemberPauli member μ) * mediatorInverseMatrix r Delta *
      mediatorLocal r f (bellMemberPauli other ν)) (mediatorVacuum r) (mediatorVacuum r) =
      if e = f ∧ μ = ν then
        ((4 * Delta)⁻¹ : ℝ) * (if member = other then (1 : ℂ) else -1) else 0 := by
…

Mentions: OAI.ContinuumCoulomb.mediatorLocal, OAI.ContinuumCoulomb.bellMemberPauli, OAI.ContinuumCoulomb.mediatorInverseMatrix, OAI.ContinuumCoulomb.mediatorVacuum