OAI/Combinatorics/EditApproximation/Binary/BinaryBandTailWork.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Work of the literal representative tail. The sole callback premise is an explicit bound on the already-defined band predicate, whose primitive bound is bandPredicateWithWork_cost; no accuracy property is assumed.

  1. def OAI.EditApproximation.BinaryFraction.bandFromActionsBitBudget line 12
  2. theorem OAI.EditApproximation.BinaryFraction.bandFromActionsWithWork_cost line 15
  3. def OAI.EditApproximation.BinaryFraction.representativeTailInputBudget line 46
  4. def OAI.EditApproximation.BinaryFraction.representativeTailBitBudget line 49
  5. theorem OAI.EditApproximation.BinaryFraction.representativeFromActionsWithWork_cost line 54
  6. def OAI.EditApproximation.BinaryFraction.representativeGuardInputBudget line 106
  7. def OAI.EditApproximation.BinaryFraction.representativeCompleteBitBudget line 109
  8. theorem OAI.EditApproximation.BinaryFraction.representativeFromActionsWithWork_complete_cost line 117

    Source documentation

    Every prefix-cut callback in the representative tail is bounded by the proved finite-prefix implementation, rather than an assumed callback budget. The premises concern only the stored input widths.

    theorem representativeFromActionsWithWork_complete_cost {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (sourceLength b : ℕ) (tau theta : BinaryFraction)
    (child : Fin M → TargetInterval ny → BinaryFraction)
    (actions : List (Fin M → TargetInterval ny)) (B : ℕ)
    (htau : tau.width ≤ B) (htheta : theta.width ≤ B)
    (hsourceLength : Nat.size sourceLength + 2 ≤ B)
    (hb : Nat.size b + 2 ≤ B) (hM : Nat.size M + 2 ≤ B)
    (hrl : Nat.size r.lo + 2 ≤ B) (hrh : Nat.size r.hi + 2 ≤ B)
    (hp : Nat.size parent.lo + 2 ≤ B)
    (hsource : ∀ i : Fin M, Nat.size (sourceChild parent i).lo + 2 ≤ B ∧
      Nat.size (sourceChild parent i).hi + 2 ≤ B)
    (hanchor : ∀ i : Fin M, Nat.size (r.lo + ((sourceChild parent i).lo - parent.lo)) + 2 ≤ B ∧
…

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