QuantumRoutingForms.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact quadratic forms for the finite singlet routing gadgets.

theorem OAI.ContinuumCoulomb.routingLowRestriction_low line 12
theorem OAI.ContinuumCoulomb.routingHighInclusion_coupling line 23
Source documentation
Hopping a singlet-sector state creates only actual mediator excitations.
```
theorem routingHighInclusion_coupling (n r : ℕ)
    (W : Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ)
    (hWlow : mediatorCompression n r W = 0) (p : MediatorLowSpace n) :
    mediatorHighInclusion n r (routingCoupling n r W p) =
      spinMatrixOperator W
        (mediatorLowInclusion n r p) := by
…
```
Mentions: OAI.ContinuumCoulomb.MediatedSpinBasis, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.MediatorLowSpace, OAI.ContinuumCoulomb.mediatorHighInclusion, OAI.ContinuumCoulomb.routingCoupling, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.mediatorLowInclusion

def OAI.ContinuumCoulomb.routingHamiltonian line 38

Source documentation

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

def routingHamiltonian (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (W : Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ) :
    Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ :=
…

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

theorem OAI.ContinuumCoulomb.routing_effectiveForm line 46
Source documentation
Exact effective quadratic form for every entangled original-spin vector.
```
theorem routing_effectiveForm (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (W : Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ)
    (hW : W.conjTranspose = W) (hWlow : mediatorCompression n r W = 0)
    (p : MediatorLowSpace n) :
    Perturbation.effectiveForm (actualMediatorLowBlock n r C)
      (diagonalPenalty (fun s => (actualMediatorWeight n r Delta s)⁻¹))
      (routingCoupling n r W) p =
      ⟪p, spinMatrixOperator (C - mediatorCompression n r
        (W * liftedMediatorInverse n r Delta *
          W)) p⟫_ℝ := by
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.MediatedSpinBasis, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.MediatorLowSpace, OAI.ContinuumCoulomb.Perturbation.effectiveForm, OAI.ContinuumCoulomb.actualMediatorLowBlock, OAI.ContinuumCoulomb.diagonalPenalty, OAI.ContinuumCoulomb.actualMediatorWeight, OAI.ContinuumCoulomb.routingCoupling, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.liftedMediatorInverse
theorem OAI.ContinuumCoulomb.routingHamiltonian_form_blocks line 90
Source documentation
Full-state quadratic-form equality for the concrete low/high blocks.
```
theorem routingHamiltonian_form_blocks (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) (hC : C.conjTranspose = C)
    (W : Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ)
    (hW : W.conjTranspose = W) (hWlow : mediatorCompression n r W = 0)
    (p : MediatorLowSpace n) (q : MediatorHighSpace n r) :
    ⟪assembleMediator n r p q,
      spinMatrixOperator (routingHamiltonian n r Delta C W)
        (assembleMediator n r p q)⟫_ℝ =
      Perturbation.lowBlockEnergy (actualMediatorLowBlock n r C)
        (diagonalPenalty (actualMediatorWeight n r Delta))
        (routingHighBlock n r C W)
        (routingCoupling n r W) p q := by
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.MediatedSpinBasis, OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.MediatorLowSpace, OAI.ContinuumCoulomb.MediatorHighSpace, OAI.ContinuumCoulomb.assembleMediator, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.routingHamiltonian, OAI.ContinuumCoulomb.Perturbation.lowBlockEnergy, OAI.ContinuumCoulomb.actualMediatorLowBlock, OAI.ContinuumCoulomb.diagonalPenalty, OAI.ContinuumCoulomb.actualMediatorWeight, OAI.ContinuumCoulomb.routingHighBlock, OAI.ContinuumCoulomb.routingCoupling