OAI/Combinatorics/EditApproximation/Geometry/MemoCodeWork.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Address generation is charged separately from binary trie traversal. The loops visit only coordinates in a key, never the ambient key space.

  1. theorem OAI.EditApproximation.naturalPairWithWork_value line 14
  2. theorem OAI.EditApproximation.naturalPairWithWork_cost line 19
  3. theorem OAI.EditApproximation.treeLayerCodeWithWork_value line 25
  4. theorem OAI.EditApproximation.treeLayerCodeWithWork_cost line 31
  5. theorem OAI.EditApproximation.physicalNodeCodeWithWork_value line 39
  6. theorem OAI.EditApproximation.physicalNodeCodeWithWork_cost line 44
  7. theorem OAI.EditApproximation.physicalEntryCodeWithWork_value line 52
  8. theorem OAI.EditApproximation.physicalEntryCodeWithWork_cost line 57
  9. theorem OAI.EditApproximation.physicalTableCodeWithWork_value line 65
  10. theorem OAI.EditApproximation.physicalTableCodeWithWork_cost line 71
  11. theorem OAI.EditApproximation.chargedPhysicalCodeWithWork_value line 80
  12. theorem OAI.EditApproximation.chargedPhysicalCodeWithWork_cost line 86
  13. theorem OAI.EditApproximation.physicalScalarCodeWithWork_value line 99
  14. theorem OAI.EditApproximation.physicalScalarCodeWithWork_cost line 106
  15. theorem OAI.EditApproximation.physicalFamilyCodeWithWork_value line 143
  16. theorem OAI.EditApproximation.physicalFamilyCodeWithWork_cost line 151
  17. theorem OAI.EditApproximation.computedFamilyMemoCodeWithWork_value line 165
  18. theorem OAI.EditApproximation.computedFamilyMemoCodeWithWork_cost line 171