OAI/Computability/MaxCut/Encoding/VerticesBits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.OptimalMaxCut.RawGrid.vertices_bits line 14
2. theorem OAI.OptimalMaxCut.RawGrid.edges_bits line 15
3. theorem OAI.OptimalMaxCut.RawGrid.row_source line 16
4. theorem OAI.OptimalMaxCut.RawGrid.row_target line 19
5. theorem OAI.OptimalMaxCut.RawGrid.row_image line 21
6. theorem OAI.OptimalMaxCut.RawGrid.degree_bits line 24
7. theorem OAI.OptimalMaxCut.RawGrid.lookup_fin line 33
8. theorem OAI.OptimalMaxCut.RawGrid.permCode_bits line 37
9. theorem OAI.OptimalMaxCut.RawGrid.query_bits line 43
10. theorem OAI.OptimalMaxCut.RawGrid.gridSize_bits line 50
11. theorem OAI.OptimalMaxCut.RawGrid.rational_floor line 54
12. theorem OAI.OptimalMaxCut.RawGrid.atom_bits line 68
13. theorem OAI.OptimalMaxCut.RawGrid.weights_bits line 82

    Source documentation

    Byte-oriented integer aggregation is exactly the rational rounded law. This identity is independent of computational complexity assumptions.

    theorem weights_bits {q : ℕ} (g : Instance q) (t : ℚ)
        (ht : t ∈ Set.Icc (-1:ℚ) 1) (K : ℕ)
        (anchor : Fin (g.vertices*2^q)) (u v : Fin (g.vertices*2^q)) :
        (ofInstance g).gridWeights t ht (vertexEquiv g.vertices q) anchor K u v =
          (weights q t ht K (bits g) u.val v.val : ℚ) / gridSize q K (bits g) := by
    …

    Mentions: OAI.OptimalMaxCut.RawGrid.weights, OAI.OptimalMaxCut.RawGrid.gridSize