OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalProgram.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The full charged refinement program on physical ranked requests and scalar source requests. This connects the local Boolean implementation to the same adaptive query used in the accuracy and dependency proofs.

  1. def OAI.EditApproximation.queryPhysicalRandomDataRequest line 22
  2. theorem OAI.EditApproximation.queryPhysicalRandomDataRequest_refines line 43