OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumMergedCoefficientBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Merging the actual bond tape reduces its length and increases each coefficient by at most the input length. These bounds apply directly to the numeric graph used by the final route compiler.

  1. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_length_le_input line 14
  2. theorem OAI.ContinuumCoulomb.QuantumListMerge.value_coefficient_bound line 22
  3. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_count line 35
  4. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_coefficientBound line 41
  5. theorem OAI.ContinuumCoulomb.QuantumPlanarTapeGeometry.graph_coefficientBound_of_raw line 57
  6. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_planar_bounds line 80
  7. theorem OAI.ContinuumCoulomb.QuantumCrossingSelectProgram.compiled_planar_nat line 121