PhysicalLocalGroupProgram.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite indexed group program has an equivalent cell-keyed realization. Good initial seeds permit its whole cone to be evaluated using only the directly enumerated query cells.

def OAI.EditApproximation.physicalGroupStreamsOfKeys line 18
theorem OAI.EditApproximation.physicalProgramCells_keyed line 25
theorem OAI.EditApproximation.physicalProgramGroups_keyed line 30

theorem OAI.EditApproximation.physicalProgramGroups_local_minimum line 57

Source documentation

Actual chosen-group cone at one node, evaluated by bounded query cell loops. The old-child fallback is arbitrary provided it is at most the literal initial value.

theorem physicalProgramGroups_local_minimum (T : ℕ) (tau : ℚ) {R : ℕ} [NeZero R]
    (draw : PhysicalInternalNode M J → Fin R → CellGroupDraws M F Q)
    (node : PhysicalNode M J) (hbelow : node.1.val < J)
    (children : PhysicalChildTables M target.length) (t : ℕ)
    (q : TargetInterval target.length) (fallback : ℚ)
    (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)
    (hfallback : fallback ≤ stageInitial source target U N P F A (node, q))
    (hchild : ∀ i r, 0 ≤ children i t r) :
    rationalMinimum fallback
        ((localCellGroupActions source target (physicalSourceInterval source.length node)
…

Mentions: OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.CellGroupDraws, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.PhysicalChildTables, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource, OAI.EditApproximation.stageInitial, OAI.EditApproximation.rationalMinimum, OAI.EditApproximation.localCellGroupActions, OAI.EditApproximation.physicalSourceInterval