OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePromise.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Finite binary input and promise language for the published signed, field-free square-lattice Heisenberg problem. Invalid encodings and inputs outside the energy promise belong to neither promise set.

  1. structure OAI.ContinuumCoulomb.BinaryRational line 15

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

  2. def OAI.ContinuumCoulomb.BinaryRational.value line 20

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

  3. def OAI.ContinuumCoulomb.binaryRationalEquiv line 23

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

  4. def OAI.ContinuumCoulomb.binaryRationalCodec line 29

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

  5. def OAI.ContinuumCoulomb.BinaryRational.ofRat line 31
  6. theorem OAI.ContinuumCoulomb.BinaryRational.value_ofRat line 33
  7. structure OAI.ContinuumCoulomb.BinaryHeisenbergEdge line 36
  8. def OAI.ContinuumCoulomb.binaryHeisenbergEdgeEquiv line 42
  9. def OAI.ContinuumCoulomb.binaryHeisenbergEdgeCodec line 48
  10. structure OAI.ContinuumCoulomb.BinaryHeisenberg line 51
  11. def OAI.ContinuumCoulomb.binaryHeisenbergEquiv line 58
  12. def OAI.ContinuumCoulomb.binaryHeisenbergCodec line 65
  13. structure OAI.ContinuumCoulomb.BinaryHeisenberg.Valid line 70
  14. def OAI.ContinuumCoulomb.BinaryHeisenberg.toSource line 89

    Source documentation

    Decode valid finite data into the existing actual spin Hamiltonian.

    def BinaryHeisenberg.toSource (d : BinaryHeisenberg) (h : d.Valid) : SquareLatticeHeisenberg where
…

    Mentions: OAI.ContinuumCoulomb.BinaryHeisenberg, OAI.ContinuumCoulomb.SquareLatticeHeisenberg

  15. structure OAI.ContinuumCoulomb.BinaryHeisenberg.PolynomialPromise line 116

    Source documentation

    A single fixed exponent bounds lattice extent, source weights and inverse gap, as in the polynomial-weight spatially sparse source branch.

    structure BinaryHeisenberg.PolynomialPromise (k : ℕ) (d : BinaryHeisenberg) : Prop where
…

    Mentions: OAI.ContinuumCoulomb.BinaryHeisenberg

  16. def OAI.ContinuumCoulomb.sourceHeisenbergPromise line 127
  17. def OAI.ContinuumCoulomb.PublishedCMPHardness line 143

    Source documentation

    Field-free signed square-lattice Heisenberg hardness of Cubitt–Montanaro–Piddock, arXiv:1701.05182v4, Theorem 48 and Section 10.1, with the polynomial-weight sparse construction of Lemma 47.

    def PublishedCMPHardness : Prop :=
…