OAI/Combinatorics/EditApproximation/Refinement/PhysicalBoundedQuery.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual global read program stays within the bounded cache-key domain. Restricting its type therefore preserves the complete local-pass value and gives an injectively encoded memo evaluator.

  1. instance OAI.EditApproximation.PhysicalTableRequest.decidableBounded line 15
  2. theorem OAI.EditApproximation.globalSeedRead_keys_bounded line 20
  3. theorem OAI.EditApproximation.physicalGlobalQuery_keys_bounded line 50
  4. def OAI.EditApproximation.physicalBoundedQuery line 106
  5. theorem OAI.EditApproximation.physicalBoundedQuery_value line 114
  6. def OAI.EditApproximation.physicalMemoEvaluate line 129
  7. theorem OAI.EditApproximation.physicalMemoEvaluate_value line 139