LocalRefinementCones.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Direct local enumeration computes the complete refinement Bellman cone on a spatially regular initial table. Its finite definition applies to every seed.

theorem OAI.EditApproximation.representativeList_conditions line 18
theorem OAI.EditApproximation.localRefinementRepresentatives_subset line 28
theorem OAI.EditApproximation.rationalActualWideActions_representative line 40
theorem OAI.EditApproximation.rationalActualWideActions_mono line 49
theorem OAI.EditApproximation.localRefinementRepresentatives_complete line 58

theorem OAI.EditApproximation.localRefinementBellman_eq line 83

Source documentation

Local representatives retain every cone that can improve the initial fallback. All other complete cones are discarded by their distance charge.

theorem localRefinementBellman_eq {nx ny M : ℕ}
    (parent : TargetInterval nx) (N P F : ℕ) (a : ℚ)
    (initial : TargetInterval ny → ℚ) (child : Fin M × TargetInterval ny → ℚ)
    (q : TargetInterval ny) (ha : 1 ≤ a) (hF : 1 ≤ F)
    (hinitial : 0 ≤ initial q) (hchild : ∀ s, 0 ≤ child s)
    (hspatial : ∀ r, |initial q - initial r| ≤ 32 * F * targetEndpointDistance q r) :
    rationalBellman initial (fun q r => targetEndpointDistance q r) (128 * F)
        (rationalActualWideActions parent (localRefinementRepresentatives N P F a initial q) P) child q =
      rationalBellman initial (fun q r => targetEndpointDistance q r) (128 * F)
        (rationalActualWideActions parent (representativeList N P F a initial) P) child q := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.rationalBellman, OAI.EditApproximation.rationalActualWideActions, OAI.EditApproximation.localRefinementRepresentatives, OAI.EditApproximation.representativeList

theorem OAI.EditApproximation.physical_localRefinementBellman_eq line 131

Source documentation

The actual initial table supplies the spatial hypotheses on a good seed. Thus the bounded local search computes its literal warmup cone.

theorem physical_localRefinementBellman_eq {α : Type*} [DecidableEq α] {M J : ℕ}
    (source target : List α) (U : PhysicalEntry M J target.length → ℕ)
    (N P F : ℕ) (A : ℚ) (hsize : source.length + target.length ≤ N)
    (hP : 66 ≤ P) (hF : 1 ≤ F) (hA : 1 ≤ A)
    (hseed : ∀ state, stateEditCost (physicalSource source state.1) target state.2 ≤ U state ∧
      (U state : ℚ) ≤ A * stateEditCost (physicalSource source state.1) target state.2)
    (node : PhysicalNode M J) (child : Fin M × TargetInterval target.length → ℚ)
    (hchild : ∀ s, 0 ≤ child s) (q : TargetInterval target.length) :
    rationalBellman (fun r => stageInitial source target U N P F A (node, r))
        (fun q r => targetEndpointDistance q r) (128 * F)
        (rationalActualWideActions (physicalSourceInterval source.length node)
          (localRefinementRepresentatives N P F (refinementFactor A F)
…