OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedWeightProgram.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Uniform literal rational-list programs for all five early gadget stages. The lists retain input order and emit each fixed block in its word order.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.Pair line 15
  2. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.pairCode line 16
  3. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.radius line 17
  4. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.coupling line 18
  5. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.radiusSquare line 19
  6. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.radiusCube line 21
  7. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.radiusHalf line 23
  8. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.cubeHalf line 25
  9. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.couplingHalf line 27
  10. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.correction line 29
  11. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.fourProgram line 33
  12. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.sevenProgram line 48
  13. abbrev OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.Input line 69
  14. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.inputCode line 70
  15. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.scale line 71
  16. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.scaleProgram line 73
  17. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.block line 88
  18. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.stage line 89
  19. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.stageProgram line 92
  20. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.four line 102
  21. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.seven line 104
  22. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.fourListProgram line 106
  23. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.sevenListProgram line 108
  24. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.nextFour line 111
  25. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.nextSeven line 112
  26. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.nextFourProgram line 113
  27. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.nextSevenProgram line 115
  28. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.output line 118
  29. opaque OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.outputProgram line 119
  30. def OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.certificate line 123
  31. theorem OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.scale_ofFn line 126
  32. theorem OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.four_ofFn line 131
  33. theorem OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.seven_ofFn line 140
  34. theorem OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.stage_length line 149
  35. theorem OAI.ContinuumCoulomb.QuantumOrderedWeightProgram.output_length line 161