OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalOnlineEquality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A proof adapter couples the bounded online query loop to the original finite product slots. The adapter is used only to compare laws: local execution uses scale/center keys and never searches a complete table.

  1. def OAI.EditApproximation.physicalRepresentativeFin line 20
  2. theorem OAI.EditApproximation.physicalRepresentativeFin_get line 24
  3. def OAI.EditApproximation.physicalOnlineIntegersOfStreams line 29
  4. theorem OAI.EditApproximation.physicalOnlineIntegersOfStreams_get line 36
  5. theorem OAI.EditApproximation.physicalLocalOnline_mem_iff line 49