OAI/Combinatorics/EditApproximation/Refinement/PhysicalMedianQuery.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A seed entry is computed by querying the previous pass at the same physical node in each copy, then applying the literal clamped median. The copy coordinate never changes the dependency rank.

  1. theorem OAI.EditApproximation.previousPassRequest_progress line 16
  2. theorem OAI.EditApproximation.physicalMedianSeedQuery_value line 29
  3. theorem OAI.EditApproximation.physicalMedianSeedQuery_cost line 40
  4. theorem OAI.EditApproximation.physicalMedianSeedQuery_eq_update line 50