OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryRawWork.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryRawWorkDegree line 12
2. def OAI.EditApproximation.computedQueryRawWidthDegree line 13
3. theorem OAI.EditApproximation.computedQueryMemoRaw_bounds line 16

   Source documentation

   Every raw body is charged on the actual, proved normalized-child oracle.

   theorem computedQueryMemoRaw_bounds :
       ∀ᶠ N : ℕ in atTop, ∀ source target : List ℕ, source.length + target.length ≤ N →
         ∀ (input : ComputedFamilyInput source target N)
         (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ),
         symbolBits ≤ inputHeight N ^ 3 → positionBits ≤ inputHeight N ^ 3 →
         (∀ z ∈ source, z < 2 ^ symbolBits) → (∀ z ∈ target, z < 2 ^ symbolBits) →
         target.length ≤ 2 ^ positionBits → occurrence = occurrenceBuild symbolBits positionBits target.zipIdx →
         ∀ key : ComputedFamilyMemoKey source target N,
         let oracle := fun child : {child : ComputedFamilyMemoKey source target N //
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.inputHeight, OAI.EditApproximation.occurrenceBuild, OAI.EditApproximation.ComputedFamilyMemoKey