PhysicalWarmupStepQuery.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A local warmup step gathers its candidate initial values and each distinct wide child coordinate before evaluating the finite Bellman minimum. Wide action enumeration makes no recursive oracle calls.

theorem OAI.EditApproximation.localRefinementRepresentatives_congr_raw line 16
theorem OAI.EditApproximation.wideWarmupInputs_action line 32
theorem OAI.EditApproximation.localWarmupStepQuery_value line 47
theorem OAI.EditApproximation.physicalWarmupStepQuery_value line 93

theorem OAI.EditApproximation.physicalWarmupRequestQuery_value line 120

Source documentation

Every child read of a positive warmup step carries its concrete strict progress proof. The previous-pass seed reader is supplied by the pass wrapper, so its own reads must carry the same strict proof.

theorem physicalWarmupRequestQuery_value {α : Type*} [DecidableEq α] {M J : ℕ}
    (source target : List α) (N P F : ℕ) (A : ℚ)
    (pass copy T S j : ℕ) (node : PhysicalNode M J) (q : TargetInterval target.length)
    (seedRead : PhysicalEntry M J target.length →
      FiniteQuery {child : PhysicalTableRequest M J target.length //
        child.combinedRank T S < (PhysicalTableRequest.warmup pass copy node j q).combinedRank T S})
    (values : PhysicalTableRequest M J target.length → ℚ)
    (U : PhysicalEntry M J target.length → ℕ)
    (hseed : ∀ state, (seedRead state).value (fun child => values child.val) = (U state : ℚ))
    (hchild : ∀ (hbelow : node.1.val < J) (input : Fin M × TargetInterval target.length),
      values (PhysicalTableRequest.warmup pass copy (physicalChild node hbelow input.1) (j - 1) input.2) =
        physicalLocalWarmup source target U N P F A (j - 1)
…

Mentions: OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.PhysicalTableRequest, OAI.EditApproximation.PhysicalTableRequest.warmup, OAI.EditApproximation.physicalChild, OAI.EditApproximation.physicalLocalWarmup