OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelFamily.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

A literal indexed list stage, shared by the six fixed local reductions. New mediator indices are the old qubit count plus the input term index. Unary counts bound the output size; rational coefficients stay binary.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.Entry line 15
  2. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.State line 16
  3. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.Input line 17
  4. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.BlockInput line 18
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.entryCode line 20
  6. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.stateCode line 21
  7. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.inputCode line 22
  8. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.blockCode line 23
  9. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.weights line 25
  10. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.radius line 26
  11. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.indexed line 27
  12. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.block line 30
  13. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.family line 34
  14. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.value line 38
  15. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.stateProgram line 42
  16. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.precisionProgram line 43
  17. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.countProgram line 44
  18. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.entriesProgram line 46
  19. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.lengthProgram line 48
  20. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.weightsProgram line 50
  21. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.radiusProgram line 53
  22. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.indexedProgram line 56
  23. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.blockProgram line 64
  24. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.familyProgram line 79
  25. def OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.valueProgram line 88
  26. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelFamily.family_length line 94