OAI/Combinatorics/EditApproximation/Refinement/PhysicalRequestEncoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fixed-width keys for the bounded physical cache. Their construction uses only the request's coordinates, without enumerating table entries.

  1. def OAI.EditApproximation.PhysicalTableRequest.capacity line 18
  2. def OAI.EditApproximation.PhysicalTableRequest.bits line 21
  3. theorem OAI.EditApproximation.PhysicalTableRequest.code_injective line 24
  4. theorem OAI.EditApproximation.PhysicalTableRequest.code_bound line 52
  5. theorem OAI.EditApproximation.PhysicalTableRequest.code_fits line 67