OAI/Combinatorics/EditApproximation/Refinement/PhysicalRefinementDataRequest.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

All initial and warmup-mass data are ordinary earlier table requests. A positive refinement step therefore has no fixed-table oracle arguments. Parent initial data use the same node's warmup-zero entry; child data and histories use the concrete physical children.

  1. theorem OAI.EditApproximation.physicalInitialQuery_value_local line 15
  2. theorem OAI.EditApproximation.physicalWarmupStepQuery_value_local line 40
  3. theorem OAI.EditApproximation.physicalWarmupRequestQuery_value_local line 60
  4. theorem OAI.EditApproximation.physicalRefinementMassQuery_value line 95
  5. def OAI.EditApproximation.physicalRefinementDataRequestQuery line 113
  6. theorem OAI.EditApproximation.physicalRefinementDataRequestQuery_value line 126