OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLatticeEncoding.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite source objects serialize to valid binary instances with canonical rational coefficients and the same physical sites and thresholds.

  1. def OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binaryEdge line 12
  2. def OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary line 15
  3. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_vertices line 21
  4. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_edges line 23
  5. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.get_ofFn_value line 26
  6. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_getEdge line 30
  7. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_getCoordinate line 34
  8. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_valid line 40
  9. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_lower line 75
  10. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_upper line 77
  11. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.ext_data line 80
  12. theorem OAI.ContinuumCoulomb.SquareLatticeHeisenberg.binary_toSource line 96