OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLatticePromise.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual lattice serialization preserves the source energy promise. Numerical envelopes may be measured against any retained input size; the output bit length is at least the number of physical spins.

  1. def OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binaryPacket line 18

    Source documentation

    The literal serializer receives precisely the finite data of this source.

    def binaryPacket (d : SquareLatticeHeisenberg) : QuantumLatticeSerialization.Input :=
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.QuantumLatticeSerialization.Input

  2. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binaryPacket_value line 23
  3. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_polynomialPromise line 34
  4. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_mem_yes line 59
  5. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_mem_no line 66
  6. def OAI.ContinuumCoulomb.QMAPortRouteData.marginSource line 83

    Source documentation

    Preserve a positive gap by moving both thresholds inward by the proved simulation error, before removing the exact scalar matrix offset.

    def marginSource (hn : 0 < G.n) (a b ε : ℚ) (hab : a+ε < b-ε) : SquareLatticeHeisenberg :=
…

    Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg

  7. theorem OAI.ContinuumCoulomb.QMAPortRouteData.marginSource_yes line 86
  8. theorem OAI.ContinuumCoulomb.QMAPortRouteData.marginSource_no line 97