OAI/Combinatorics/EditApproximation/Geometry/SourceRankedEncoding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An explicit parity tag separates source coordinates and table keys. The code is computed from coordinates without enumerating the key type.

  1. def OAI.EditApproximation.SourceRanked.keyCapacity line 17
  2. def OAI.EditApproximation.SourceRanked.keyBits line 20
  3. theorem OAI.EditApproximation.SourceRanked.keyCode_injective line 23
  4. theorem OAI.EditApproximation.SourceRanked.keyCode_bound line 49
  5. theorem OAI.EditApproximation.SourceRanked.keyCode_fits line 58