OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingPacketBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Coefficient bounds for the actual serialized crossing packet. The transfer uses the literal nine-bond blocks, including the scalar offset.

  1. theorem OAI.ContinuumCoulomb.QuantumCrossingListLayer.actual_bonds_coefficientBound line 16
  2. theorem OAI.ContinuumCoulomb.QuantumCrossingListLayer.actualGraph_coefficientBound line 35
  3. theorem OAI.ContinuumCoulomb.QuantumCrossingListLayer.actualGraph_card line 46
  4. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_graph_coefficientBound line 62
  5. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_graph_count line 70
  6. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_merged_coefficientBound line 80
  7. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_merged_nat line 97