OAI/MathematicalPhysics/ContinuumCoulomb/Programs/EncodingPrograms.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Actual finite-stack parsing and serialization routines for the coordinate codes. Sign bits, natural-number marker bits, and field tails are read by the program rather than by an assumed record-decoding operation.

  1. def OAI.ContinuumCoulomb.BinaryEncoding.quoted line 13

    Source documentation

    Quote a prefix code so an existing word-stack product parser can read the field. The quoting overhead is exactly linear.

    def quoted {α : Type} (c : Codec α) : Codec α where
…

    Mentions: OAI.ContinuumCoulomb.BinaryEncoding.Codec

  2. theorem OAI.ContinuumCoulomb.BinaryEncoding.quoted_length line 21
  3. def OAI.ContinuumCoulomb.EncodingPrograms.integerPayload line 30
  4. def OAI.ContinuumCoulomb.EncodingPrograms.integerNegative line 34
  5. def OAI.ContinuumCoulomb.EncodingPrograms.naturalInput line 38
  6. def OAI.ContinuumCoulomb.EncodingPrograms.naturalOutput line 45
  7. theorem OAI.ContinuumCoulomb.EncodingPrograms.quotedPair_encoding line 49
  8. def OAI.ContinuumCoulomb.EncodingPrograms.quotedFirst line 55
  9. def OAI.ContinuumCoulomb.EncodingPrograms.quotedSecond line 61
  10. def OAI.ContinuumCoulomb.EncodingPrograms.appendPair line 68

    Source documentation

    Serialize two already encoded fields by actual word concatenation.

    noncomputable def appendPair {α β : Type} (c : BinaryEncoding.Codec α)
    (d : BinaryEncoding.Codec β) :
    Procedure (prodCode c.encode d.encode) (BinaryEncoding.pair c d).encode id :=
…

    Mentions: OAI.ContinuumCoulomb.BinaryEncoding.Codec, OAI.ContinuumCoulomb.BinaryEncoding.pair

  11. theorem OAI.ContinuumCoulomb.EncodingPrograms.naturalPair_encoding line 74
  12. def OAI.ContinuumCoulomb.EncodingPrograms.naturalFirst line 79
  13. def OAI.ContinuumCoulomb.EncodingPrograms.naturalSecond line 83
  14. def OAI.ContinuumCoulomb.EncodingPrograms.integerPairPayload line 89

    Source documentation

    Read and remove the actual sign bit, retaining the coordinate payload and the entire following encoded field.

    noncomputable def integerPairPayload {α : Type} (c : BinaryEncoding.Codec α) :
    Procedure (BinaryEncoding.pair BinaryEncoding.integer c).encode
      (prodCode Nat.bits c.encode) (fun x => (integerPayload x.1, x.2)) :=
…

    Mentions: OAI.ContinuumCoulomb.BinaryEncoding.Codec, OAI.ContinuumCoulomb.BinaryEncoding.pair, OAI.ContinuumCoulomb.BinaryEncoding.integer, OAI.ContinuumCoulomb.EncodingPrograms.integerPayload

  15. def OAI.ContinuumCoulomb.EncodingPrograms.integerPairSign line 102
  16. def OAI.ContinuumCoulomb.EncodingPrograms.integerFirst line 109
  17. def OAI.ContinuumCoulomb.EncodingPrograms.integerSecond line 123
  18. def OAI.ContinuumCoulomb.EncodingPrograms.emptyUnit line 127
  19. def OAI.ContinuumCoulomb.EncodingPrograms.integerInput line 132
  20. def OAI.ContinuumCoulomb.EncodingPrograms.integerOutput line 138

    Source documentation

    Convert signed-magnitude stack integers to the exact signed-coordinate convention whose negative payload is one less than its absolute value.

    noncomputable def integerOutput : Procedure intCode BinaryEncoding.integer.encode id := by
…
  21. def OAI.ContinuumCoulomb.EncodingPrograms.affineCoordinate line 155

    Source documentation

    Scaling and translating a signed lattice coordinate uses genuine binary arithmetic and emits the signed-coordinate code.

    noncomputable def affineCoordinate (scale offset : ℤ) :
    Procedure BinaryEncoding.integer.encode BinaryEncoding.integer.encode
      (fun z => scale * z + offset) := by
…
  22. def OAI.ContinuumCoulomb.EncodingPrograms.affineCoordinate_certificate line 164