OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryOutput.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedQueryAnswerWithWork_execution line 9

   Source documentation

   The binary evaluator returns exactly the answer used in the execution-law theorem.

   theorem computedQueryAnswerWithWork_execution (source target : List ℕ) (N : ℕ)
       (epsilon : BinaryFraction) (hlarge : physicalLargeInput N epsilon)
       (hsize : source.length + target.length ≤ N)
       (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (hs : ∀ z ∈ source, z < 2 ^ symbolBits) (ht : ∀ z ∈ target, z < 2 ^ symbolBits)
       (hp : target.length ≤ 2 ^ positionBits)
       (htable : occurrence = occurrenceBuild symbolBits positionBits target.zipIdx)
       (execution : ComputedExecutionOutcome source target N) :
       bitWordValue (computedQueryAnswerWithWork source target N occurrence symbolBits positionBits
         (computedExecutionAccepted source target N execution)).1 =
         computedFullAnswer source target N (.inr execution) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.physicalLargeInput, OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.occurrenceBuild, OAI.EditApproximation.ComputedExecutionOutcome, OAI.EditApproximation.bitWordValue, OAI.EditApproximation.computedQueryAnswerWithWork, OAI.EditApproximation.computedExecutionAccepted, OAI.EditApproximation.computedFullAnswer