OAI/Combinatorics/EditApproximation/Geometry/CanonicalFractionWork.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Fractions retain their unreduced numerator and denominator, but discard leading zero bits after each operation. This exposes actual storage length without charging or performing rational normalization.

  1. theorem OAI.EditApproximation.BinaryFraction.canonicalizeWithWork_representation line 17
  2. theorem OAI.EditApproximation.BinaryFraction.canonicalizeWithWork_width line 23
  3. theorem OAI.EditApproximation.BinaryFraction.canonicalizeWithWork_cost line 30
  4. theorem OAI.EditApproximation.BinaryFraction.canonicalAddWithWork_representation line 41
  5. theorem OAI.EditApproximation.BinaryFraction.canonicalMulWithWork_representation line 45
  6. theorem OAI.EditApproximation.BinaryFraction.rawAdd_width line 49
  7. theorem OAI.EditApproximation.BinaryFraction.rawMul_width line 65
  8. theorem OAI.EditApproximation.BinaryFraction.canonicalAddWithWork_cost line 76
  9. theorem OAI.EditApproximation.BinaryFraction.canonicalMulWithWork_cost line 84
  10. theorem OAI.EditApproximation.BinaryFraction.canonicalizeWithWork_width_le_storageBits line 92
  11. theorem OAI.EditApproximation.BinaryFraction.canonicalAddWithWork_width_le_storageBits line 98
  12. theorem OAI.EditApproximation.BinaryFraction.canonicalMulWithWork_width_le_storageBits line 105
  13. theorem OAI.EditApproximation.BinaryFraction.canonicalAddWithWork_self_width line 112
  14. theorem OAI.EditApproximation.BinaryFraction.canonicalMulWithWork_self_width line 117