OAI/Combinatorics/ParityLifts/GraphOutput.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.Complexity.ChoiceData.matrix_eq line 9
2. lemma OAI.ParityWL.Complexity.ChoiceData.vertices_length_eq line 23
3. def OAI.ParityWL.Complexity.ChoiceData.output line 30
4. def OAI.ParityWL.Complexity.PolyProgram.vertexCount line 33
5. def OAI.ParityWL.Complexity.PolyProgram.orderPrefix line 38
6. def OAI.ParityWL.Complexity.PolyProgram.leftOutput line 45
7. def OAI.ParityWL.Complexity.PolyProgram.graphOutput line 53
8. lemma OAI.ParityWL.Complexity.matrix_cast line 60
9. theorem OAI.ParityWL.Complexity.ChoiceData.output_spec line 70

   Source documentation

   The actual generated bit string is the two full adjacency matrices of the uncolored simple graphs in the parity reduction, up to proved finite indexing.

   theorem ChoiceData.output_spec (k : ℕ) (hk : 4≤k) (c : Convention)
       (D : ChoiceData (bagParameter c k)) :
       ∃ (n : ℕ) (G H : SimpleGraph (Fin n)),
         D.output = encodeGraphs G H ∧
         (∀ i : Implementation, Equivalent G H c i k ↔ ¬ D.system.Successful) ∧
         n = (D.vertices (fun _ => 0)).length := by
   …

   Mentions: OAI.ParityWL.Convention, OAI.ParityWL.Complexity.ChoiceData, OAI.ParityWL.bagParameter, OAI.ParityWL.Complexity.encodeGraphs, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Equivalent