OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/AutomaticCalibrationList.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

All edges share one fixed calibration program and one rational spacing. Mapping that program over the edge coefficients retains a polynomial running time in the complete encoded input.

  1. abbrev OAI.ContinuumCoulomb.AutomaticCalibrationList.Environment line 14
  2. abbrev OAI.ContinuumCoulomb.AutomaticCalibrationList.Input line 15
  3. def OAI.ContinuumCoulomb.AutomaticCalibrationList.environmentCode line 17
  4. def OAI.ContinuumCoulomb.AutomaticCalibrationList.inputCode line 19
  5. def OAI.ContinuumCoulomb.AutomaticCalibrationList.value line 21
  6. opaque OAI.ContinuumCoulomb.AutomaticCalibrationList.elementProgram line 24
  7. opaque OAI.ContinuumCoulomb.AutomaticCalibrationList.program line 34
  8. def OAI.ContinuumCoulomb.AutomaticCalibrationList.certificate line 40
  9. theorem OAI.ContinuumCoulomb.AutomaticCalibrationList.value_near_one line 44
  10. theorem OAI.ContinuumCoulomb.AutomaticCalibrationList.value_length line 51