OAI/Combinatorics/EditApproximation/Binary/BinaryPhysicalContinuation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The local refinement return is computed by the binary-fraction continuation. Wide actions are built from the emitted endpoint grids, and their connection charges are evaluated before the two Bellman minima.

  1. theorem OAI.EditApproximation.BinaryFraction.endpointActionWithWork_decode line 18
  2. theorem OAI.EditApproximation.BinaryFraction.wideActionsFromRepresentativesWithWork_decode line 27
  3. def OAI.EditApproximation.BinaryFraction.physicalContinuationWithWork line 40
  4. theorem OAI.EditApproximation.BinaryFraction.physicalContinuationWithWork_value line 52
  5. theorem OAI.EditApproximation.BinaryFraction.physicalContinuationWithWork_local_value line 69

    Source documentation

    Exact local-program wiring. The two equalities are representation identities for the already-computed sampled action lists.

    theorem physicalContinuationWithWork_local_value {α : Type*} (source target : List α) {M : ℕ}
    (parent : TargetInterval source.length) (N P F exponent Q : ℕ)
    (tau a : ℚ) (delta : BinaryFraction)
    (parentInitial : TargetInterval target.length → BinaryFraction)
    (childMass childInitial : Fin M → TargetInterval target.length → ℚ)
    (old current : Fin M × TargetInterval target.length → BinaryFraction)
    (draw : CellGroupDraws M F Q)
    (groups online : List (BinaryBellmanAction (TargetInterval target.length)
      (Fin M × TargetInterval target.length) M))
    (logicalOnline : List (PhysicalRationalAction M target.length)) (query : TargetInterval target.length)
    (hP : 0 < P)
    (hgroups : groups.map BinaryBellmanAction.decode = localCellGroupActions source target parent
…

    Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.CellGroupDraws, OAI.EditApproximation.BinaryBellmanAction, OAI.EditApproximation.PhysicalRationalAction, OAI.EditApproximation.BinaryBellmanAction.decode, OAI.EditApproximation.localCellGroupActions