OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalProgramEquality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete refinement is reproduced, on good incoming seeds, by bounded cell and rounded-center loops with local warmup data throughout.

  1. theorem OAI.EditApproximation.physicalLocalRefinement_online_mem_congr line 11
  2. theorem OAI.EditApproximation.physicalLocalProgram_eq line 63