OAI/Combinatorics/EditApproximation/Refinement/PhysicalRandomGlobalQuery.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Global physical table bodies with explicit random reads. Only positive internal refinement steps request random coordinates. All other cases use finite warmup and initial queries.

  1. theorem OAI.EditApproximation.inactiveIfEq line 14
  2. theorem OAI.EditApproximation.physicalGlobalQuery_inactive line 42
  3. theorem OAI.EditApproximation.physicalRandomGlobalQuery_inactive line 58
  4. theorem OAI.EditApproximation.physicalRandomGlobalQuery_active_value line 74
  5. theorem OAI.EditApproximation.physicalRandomGlobalQuery_compare line 96