ComputedCurrentQueryBudget.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial same-index call budget after substituting the computed window, cell, scale-label, sampling and rounding parameters.

def OAI.EditApproximation.localCurrentBudget line 11
theorem OAI.EditApproximation.localCurrentBudget_poly line 14
theorem OAI.EditApproximation.computed_window_exponent_bound line 46
theorem OAI.EditApproximation.computed_local_cell_budget line 56
theorem OAI.EditApproximation.computed_refinement_window line 77

theorem OAI.EditApproximation.computed_currentQueryInputCover_card line 96

Source documentation

The actual finite local shared/selected/online input cover is bounded by M*ell^256 on every seed. The online-loop length premise is the literal one-action-per-applicable-scale property proved for the physical program.

theorem computed_currentQueryInputCover_card {α : Type*} (source target : List α)
    (N P : ℕ) (hN : 0 < N) (hell : 200 ≤ inputSmallLog N)
    (parent : TargetInterval source.length) (A tau : ℚ)
    (hA : A ≤ ((integerParameters N).initialFactor : ℚ))
    (parentInitial : TargetInterval target.length → ℚ)
    (child initial current : Fin (integerParameters N).M → TargetInterval target.length → ℚ)
    (draw : CellGroupDraws (integerParameters N).M (inputSmallLog N) (inputSmallLog N ^ 80))
    (q : TargetInterval target.length) (hw : 0 ≤ parentInitial q)
    (online : List (PhysicalRationalAction (integerParameters N).M target.length))
    (honline : online.length ≤
      (dyadicQueryWindow N (parentInitial q) (refinementFactor A (inputSmallLog N)) (inputSmallLog N)).length) :
    (currentQueryInputCover source target parent N P (inputSmallLog N) (40 * smallLogExponent N)
…

Mentions: OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.integerParameters, OAI.EditApproximation.CellGroupDraws, OAI.EditApproximation.PhysicalRationalAction, OAI.EditApproximation.dyadicQueryWindow, OAI.EditApproximation.refinementFactor, OAI.EditApproximation.currentQueryInputCover, OAI.EditApproximation.smallLogExponent