OAI/Combinatorics/EditApproximation/Refinement/PhysicalInputEncoding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed-width binary keys for gathered child states. The encoding uses mixed radix arithmetic on the child label and the two state endpoints.

  1. theorem OAI.EditApproximation.mixedRadix_injective line 12
  2. theorem OAI.EditApproximation.childInputCode_injective line 23
  3. theorem OAI.EditApproximation.childInputCode_bound line 33
  4. def OAI.EditApproximation.childInputBits line 44
  5. theorem OAI.EditApproximation.childInputCode_fits line 46
  6. theorem OAI.EditApproximation.childInputBinaryKey_injective line 51
  7. theorem OAI.EditApproximation.childInputBits_le line 58