OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/BinaryEncoding.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Explicit prefix-free binary encodings for finite source and circuit data. Natural numbers use their binary digits, with one marker bit per digit. Pairs concatenate; lists have a binary length header. In particular, list serialization does not repeatedly pair large natural-number codes.

  1. abbrev OAI.ContinuumCoulomb.BinaryEncoding.BitString line 15

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:12 (same declaration text).

  2. structure OAI.ContinuumCoulomb.BinaryEncoding.Codec line 17

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:14 (same declaration text).

  3. theorem OAI.ContinuumCoulomb.BinaryEncoding.Codec.encode_injective line 22
  4. def OAI.ContinuumCoulomb.BinaryEncoding.encodeDigits line 28

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:19 (same declaration text).

  5. def OAI.ContinuumCoulomb.BinaryEncoding.readDigits line 32

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:23 (same declaration text).

  6. theorem OAI.ContinuumCoulomb.BinaryEncoding.readDigits_encode line 37

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:28 (same declaration text).

  7. def OAI.ContinuumCoulomb.BinaryEncoding.decodeDigits line 43

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:34 (same declaration text).

  8. theorem OAI.ContinuumCoulomb.BinaryEncoding.decodeDigits_bits line 47

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:38 (same declaration text).

  9. def OAI.ContinuumCoulomb.BinaryEncoding.natural line 52

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:43 (same declaration text).

  10. theorem OAI.ContinuumCoulomb.BinaryEncoding.encodeDigits_length line 57
  11. theorem OAI.ContinuumCoulomb.BinaryEncoding.natural_length line 64

    Source documentation

    The code of a natural has linear overhead in its binary bit length.

    theorem natural_length (n : ℕ) : (natural.encode n).length = 2 * n.size + 1 := by
…
  12. def OAI.ContinuumCoulomb.BinaryEncoding.encodeUnary line 69

    Source documentation

    Unary electron counts use one true bit per electron and a false terminator.

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:48 (same declaration text).

    def encodeUnary : ℕ → BitString
  | 0 => [false]
  | n + 1 => true :: encodeUnary n

    Mentions: OAI.ContinuumCoulomb.BinaryEncoding.BitString

  13. def OAI.ContinuumCoulomb.BinaryEncoding.readUnary line 73

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:52 (same declaration text).

  14. theorem OAI.ContinuumCoulomb.BinaryEncoding.readUnary_encode line 78

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:57 (same declaration text).

  15. def OAI.ContinuumCoulomb.BinaryEncoding.unary line 84

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:63 (same declaration text).

  16. theorem OAI.ContinuumCoulomb.BinaryEncoding.unary_length line 89
  17. def OAI.ContinuumCoulomb.BinaryEncoding.integer line 95

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:68 (same declaration text).

  18. def OAI.ContinuumCoulomb.BinaryEncoding.pair line 106

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:79 (same declaration text).

  19. def OAI.ContinuumCoulomb.BinaryEncoding.readCount line 113

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:86 (same declaration text).

  20. theorem OAI.ContinuumCoulomb.BinaryEncoding.readCount_encode line 117

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:90 (same declaration text).

  21. def OAI.ContinuumCoulomb.BinaryEncoding.list line 124

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:97 (same declaration text).

  22. def OAI.ContinuumCoulomb.BinaryEncoding.equiv line 130

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:103 (same declaration text).

  23. def OAI.ContinuumCoulomb.BinaryEncoding.sum line 135

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:108 (same declaration text).

  24. theorem OAI.ContinuumCoulomb.BinaryEncoding.pair_length line 146
  25. theorem OAI.ContinuumCoulomb.BinaryEncoding.list_length line 150