OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalRefinement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The local finite refinement recurrence, with direct query groups and local warmup data. Current-index dependencies go only to physical children; the recurrence is well founded before any accuracy assertion.

  1. def OAI.EditApproximation.physicalLocalChildMass line 12
  2. def OAI.EditApproximation.physicalLocalRefinement line 18
  3. theorem OAI.EditApproximation.physicalLocalRefinement_bounds line 48