OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrdinalProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A literal ordinal-slot program. For an encoded cell list and a unary label it counts earlier labels in the same cell; the result agrees with the bounded injective slots used by the spatial construction.

  1. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.increment line 14
  2. theorem OAI.ContinuumCoulomb.QuantumOrdinalProgram.fold_increment line 16
  3. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.incrementProgram line 24
  4. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.countProgram line 30
  5. abbrev OAI.ContinuumCoulomb.QuantumOrdinalProgram.Input line 45
  6. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.inputCode line 46
  7. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.sameCell line 48
  8. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.value line 51
  9. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.sameCellProgram line 53
  10. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.program line 65
  11. def OAI.ContinuumCoulomb.QuantumOrdinalProgram.certificate line 69
  12. theorem OAI.ContinuumCoulomb.QuantumOrdinalProgram.value_eq_card line 72
  13. theorem OAI.ContinuumCoulomb.QuantumOrdinalProgram.lookup_ofFn line 83
  14. theorem OAI.ContinuumCoulomb.QuantumOrdinalProgram.value_ofFn line 89