OAI/Combinatorics/EditApproximation/Binary/BinaryRepresentativeKernel.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The finite representative-band construction on stored binary fractions: connection and child sums, the exact wide minimum, velocity, and every literal band predicate. The Cartesian product materializes the wide-action enumeration.

  1. theorem OAI.EditApproximation.BinaryFraction.nat_distance_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.rationalConnectionBudget_nat line 23
  3. theorem OAI.EditApproximation.BinaryFraction.endpointDistanceWithWork_value line 33
  4. theorem OAI.EditApproximation.BinaryFraction.endpointConnectionWithWork_value line 40
  5. def OAI.EditApproximation.BinaryFraction.endpointScoreWithWork line 46
  6. theorem OAI.EditApproximation.BinaryFraction.endpointScoreWithWork_value line 54
  7. def OAI.EditApproximation.BinaryFraction.wideMinimumWithWork line 61
  8. theorem OAI.EditApproximation.BinaryFraction.wideMinimumWithWork_value line 69
  9. theorem OAI.EditApproximation.BinaryFraction.stateGapWithWork_value line 79
  10. def OAI.EditApproximation.BinaryFraction.bandFromActionsWithWork line 84

    Source documentation

    Every filter callback is the literal binary band predicate.

    def bandFromActionsWithWork {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (b : ℕ) (tau theta velocity : BinaryFraction)
    (child : Fin M → TargetInterval ny → BinaryFraction)
    (actions : List (Fin M → TargetInterval ny)) (hne : actions ≠ []) :
    List (Fin M → TargetInterval ny) × ℕ :=
…

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

  11. theorem OAI.EditApproximation.BinaryFraction.bandFromActionsWithWork_value line 97
  12. def OAI.EditApproximation.BinaryFraction.representativeFromActionsWithWork line 121

    Source documentation

    The actions have been materialized once and are reused for the wide minimum and all prefix queries.

    def representativeFromActionsWithWork {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)) : List (Fin M → TargetInterval ny) × ℕ :=
…

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

  13. def OAI.EditApproximation.BinaryFraction.representativeBandWithWork line 137

    Source documentation

    Full stored-data representative construction, including the Cartesian product and all subsequent numerical work.

    def representativeBandWithWork {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (sourceLength b P : ℕ) (tau theta : BinaryFraction)
    (child : Fin M → TargetInterval ny → BinaryFraction) : List (Fin M → TargetInterval ny) × ℕ :=
…

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

  14. theorem OAI.EditApproximation.BinaryFraction.representativeFromActionsWithWork_value line 144
  15. theorem OAI.EditApproximation.BinaryFraction.representativeBandWithWork_value line 171