OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceEncodingSize.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Size bounds for the actual binary source serialization. In particular, the number of sites and edges is bounded by the input bit length.

  1. theorem OAI.ContinuumCoulomb.BinaryEncoding.natural_length_pos line 13
  2. theorem OAI.ContinuumCoulomb.BinaryEncoding.integer_length_pos line 17
  3. theorem OAI.ContinuumCoulomb.BinaryEncoding.list_count_le line 20
  4. theorem OAI.ContinuumCoulomb.binaryRational_length_pos line 34
  5. theorem OAI.ContinuumCoulomb.binaryHeisenbergEdge_length_pos line 41
  6. theorem OAI.ContinuumCoulomb.binaryHeisenberg_count_le_length line 49
  7. theorem OAI.ContinuumCoulomb.binaryHeisenberg_vertices_le_length line 61
  8. theorem OAI.ContinuumCoulomb.binaryHeisenberg_edges_le_length line 67
  9. theorem OAI.ContinuumCoulomb.binaryHeisenberg_decoded_extent line 74

    Source documentation

    The promised polynomial extent holds for every actual decoded lattice site.

    theorem binaryHeisenberg_decoded_extent (k : ℕ) (d : BinaryHeisenberg) (h : d.Valid)
    (hp : d.PolynomialPromise k) (i : Fin (d.toSource h).vertices) :
    |(((d.toSource h).coordinate i).1 : ℝ)| ≤ ((binaryHeisenbergCodec.encode d).length + 1 : ℝ) ^ k ∧
      |(((d.toSource h).coordinate i).2 : ℝ)| ≤ ((binaryHeisenbergCodec.encode d).length + 1 : ℝ) ^ k := by
…

    Mentions: OAI.ContinuumCoulomb.BinaryHeisenberg