SourceHamiltonian.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Signed square-lattice Heisenberg source

The finite source is the field-free Heisenberg problem of Cubitt–Montanaro–Piddock, Universal quantum Hamiltonians, arXiv:1701.05182v4, Theorem 48, Lemma 47 and Section 10.1. The coordinate-swap action realizes 2 SWAP - I. Coefficient-rounding estimates hold for arbitrary many-spin states, including entangled states.

abbrev OAI.ContinuumCoulomb.SourceSpinBasis line 26
Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:187 (same declaration text).
abbrev OAI.ContinuumCoulomb.SourceSpinVector line 27
def OAI.ContinuumCoulomb.sourceSpinMass line 29
def OAI.ContinuumCoulomb.sourceSpinSwap line 33
Source documentation
Swap the two selected spin coordinates, leaving every spectator fixed.
```
def sourceSpinSwap {n : ℕ} (i j : Fin n) :
    SourceSpinBasis n ≃ SourceSpinBasis n :=
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinBasis
theorem OAI.ContinuumCoulomb.sourceSpinSwap_apply line 37
theorem OAI.ContinuumCoulomb.sourceSpinSwap_involutive line 42
theorem OAI.ContinuumCoulomb.sourceSpinMass_nonneg line 48
theorem OAI.ContinuumCoulomb.sourceSpinMass_swap line 52
def OAI.ContinuumCoulomb.sourceSwapExpectation line 57
Source documentation
The expectation of coordinate exchange, taking its real part.
```
def sourceSwapExpectation {n : ℕ} (i j : Fin n) (u : SourceSpinVector n) : ℝ :=
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinVector
theorem OAI.ContinuumCoulomb.sourceSwapExpectation_add_identity line 60
theorem OAI.ContinuumCoulomb.sourceSwapExpectation_sub_identity line 76
theorem OAI.ContinuumCoulomb.sourceSwapExpectation_bounds line 92
def OAI.ContinuumCoulomb.sourceHeisenbergAction line 105
Source documentation
The local Heisenberg action on the complete n-spin Hilbert space.
```
def sourceHeisenbergAction {n : ℕ} (i j : Fin n) (u : SourceSpinVector n) :
    SourceSpinVector n :=
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinVector
def OAI.ContinuumCoulomb.sourceHeisenbergForm line 110
Source documentation
The real quadratic form of the local Heisenberg interaction.
```
def sourceHeisenbergForm {n : ℕ} (i j : Fin n) (u : SourceSpinVector n) : ℝ :=
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinVector
theorem OAI.ContinuumCoulomb.sourceHeisenbergForm_eq line 113
theorem OAI.ContinuumCoulomb.sourceHeisenbergForm_bounds line 125
theorem OAI.ContinuumCoulomb.sourceHeisenbergForm_abs_le line 133
structure OAI.ContinuumCoulomb.SquareLatticeHeisenberg line 144
Source documentation
The signed rational field-free square-lattice source input. Polynomial size/weight bounds are properties of the published reduction, not extra one-site terms or restrictions on the variational spin states.
```
structure SquareLatticeHeisenberg where
…
```
theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.edge_ne line 163
def OAI.ContinuumCoulomb.sourceHamiltonian line 171
Source documentation
Complete finite Hamiltonian, with no magnetic or one-site terms.
```
def sourceHamiltonian (d : SquareLatticeHeisenberg)
    (u : SourceSpinVector d.vertices) : SourceSpinVector d.vertices :=
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.SourceSpinVector
def OAI.ContinuumCoulomb.sourceHamiltonianForm line 176
theorem OAI.ContinuumCoulomb.sourceHamiltonianForm_eq_expectation line 181
Source documentation
Real quadratic form of the explicitly defined complete Hamiltonian.
```
theorem sourceHamiltonianForm_eq_expectation (d : SquareLatticeHeisenberg)
    (u : SourceSpinVector d.vertices) :
    sourceHamiltonianForm d u =
      (∑ s, star (u s) * sourceHamiltonian d u s).re := by
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.sourceHamiltonianForm, OAI.ContinuumCoulomb.sourceHamiltonian
def OAI.ContinuumCoulomb.sourceGroundEnergy line 196
Source documentation
Variational source energy over all normalized spin states.
```
def sourceGroundEnergy (d : SquareLatticeHeisenberg) : EReal :=
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg
theorem OAI.ContinuumCoulomb.sourceHamiltonianForm_rounding line 202
Source documentation
Rounding arbitrary signed coefficients incurs the sum of the local 3|ΔJ| errors, for the actual complete many-spin state.
```
theorem sourceHamiltonianForm_rounding
    (d : SquareLatticeHeisenberg) (rounded : Fin d.edges → ℝ)
    (u : SourceSpinVector d.vertices) (hu : sourceSpinMass u = 1) :
    |sourceHamiltonianForm d u -
      ∑ e, rounded e * sourceHeisenbergForm (d.left e) (d.right e) u| ≤
      3 * ∑ e, |(d.coefficient e : ℝ) - rounded e| := by
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.sourceSpinMass, OAI.ContinuumCoulomb.sourceHamiltonianForm, OAI.ContinuumCoulomb.sourceHeisenbergForm