OAI/MathematicalPhysics/ContinuumCoulomb/Programs/RationalLogScaleProgram.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic scale is computed from a binary power and a literal bit-counting machine. Its fixed rational multiplier is independent of the input instance.

  1. opaque OAI.ContinuumCoulomb.RationalLogScale.powerProgram line 13
  2. opaque OAI.ContinuumCoulomb.RationalLogScale.bitLengthProgram line 18
  3. opaque OAI.ContinuumCoulomb.RationalLogScale.bitLengthRationalProgram line 22
  4. opaque OAI.ContinuumCoulomb.RationalLogScale.program line 26
  5. def OAI.ContinuumCoulomb.RationalLogScale.certificate line 30