OAI/Combinatorics/EditApproximation/Binary/BinaryDistanceWork.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Absolute differences used in the literal prefix and band tests. The sign update retains the magnitude words; subtraction uses signed Boolean arithmetic.

  1. theorem OAI.EditApproximation.BinaryFraction.absolute_value line 18
  2. theorem OAI.EditApproximation.BinaryFraction.absolute_width line 26
  3. theorem OAI.EditApproximation.BinaryFraction.nat_value line 28
  4. theorem OAI.EditApproximation.BinaryFraction.canonicalAddWithWork_width line 31
  5. theorem OAI.EditApproximation.BinaryFraction.subWithWork_width line 41
  6. theorem OAI.EditApproximation.BinaryFraction.distanceWithWork_value line 48
  7. theorem OAI.EditApproximation.BinaryFraction.distanceWithWork_width line 52
  8. theorem OAI.EditApproximation.BinaryFraction.distanceWithWork_cost line 57
  9. theorem OAI.EditApproximation.BinaryFraction.connectionTermsWithWork_length line 66

    Source documentation

    List of the literal endpoint differences. Natural endpoints are encoded when encountered, and their bit-writing work is charged here.

    @[simp] theorem connectionTermsWithWork_length {n : ℕ} (start finish : BinaryFraction)
    (states : List (TargetInterval n)) :
    (connectionTermsWithWork start states finish).1.length = states.length + 1 := by
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction.connectionTermsWithWork

  10. theorem OAI.EditApproximation.BinaryFraction.connectionTermsWithWork_value line 74
  11. theorem OAI.EditApproximation.BinaryFraction.connectionTermsWithWork_width line 85
  12. def OAI.EditApproximation.BinaryFraction.connectionTermsBitBudget line 106
  13. theorem OAI.EditApproximation.BinaryFraction.connectionTermsWithWork_cost line 109
  14. theorem OAI.EditApproximation.BinaryFraction.connectionWithWork_value line 135
  15. def OAI.EditApproximation.BinaryFraction.connectionWordBudget line 141
  16. def OAI.EditApproximation.BinaryFraction.connectionBitBudget line 143
  17. theorem OAI.EditApproximation.BinaryFraction.connectionWithWork_width line 146
  18. theorem OAI.EditApproximation.BinaryFraction.connectionWithWork_cost line 155