OAI/NumberTheory/Ostmann/Construction/FinalGraphIdentification.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.FinalGraphVertex line 10
2. def OAI.Ostmann.finalVertexPerm line 13
3. def OAI.Ostmann.finalReassignedGraph line 17
4. theorem OAI.Ostmann.finalReassignedGraph_diagonal line 22
5. theorem OAI.Ostmann.final_reassignment_graph_interaction line 31

   Source documentation

   The coefficient formulas are the output of anchor creation, subsequent outside-anchor copies, and regularity of bulk rows. All other edges are arbitrary.

   theorem final_reassignment_graph_interaction {n m : ℕ} {J : Type*}
       (graph : FinalGraphVertex n m J → FinalGraphVertex n m J → ℤ)
       (α : Fin (n + 1) → ℤ) (hα : ∀ j, α j = 1 ∨ α j = -1)
       (hincoming : ∀ x j b, graph (.inr (.inl (j, b))) (.inl x) =
         anchorIncoming α (parityPathValue x.1) j b)
       (hregular : ∀ x j b, graph (.inl x) (.inr (.inl (j, b))) =
         finalCopyParity (parityPathValue x.1))
       (e f : FinalParityReassignments n m) (hef : e ≠ f) :
       ∃ (x : ParityPathSum n × Fin m) (j : Fin (n + 1)) (b : Bool),
         let G := graphDifference (finalReassignedGraph graph e) (finalReassignedGraph graph f)
   …

   Mentions: OAI.Ostmann.FinalGraphVertex, OAI.Ostmann.anchorIncoming, OAI.Ostmann.parityPathValue, OAI.Ostmann.finalCopyParity, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.ParityPathSum, OAI.Ostmann.graphDifference, OAI.Ostmann.finalReassignedGraph

6. theorem OAI.Ostmann.final_reassignment_graph_character line 49

   Source documentation

   The character at the small anchor is a genuine nonprincipal signed square.

   theorem final_reassignment_graph_character {n m : ℕ} {J : Type*}
       (graph : FinalGraphVertex n m J → FinalGraphVertex n m J → ℤ)
       (α : Fin (n + 1) → ℤ) (hα : ∀ j, α j = 1 ∨ α j = -1)
       (hincoming : ∀ x j b, graph (.inr (.inl (j, b))) (.inl x) =
         anchorIncoming α (parityPathValue x.1) j b)
       (hregular : ∀ x j b, graph (.inl x) (.inr (.inl (j, b))) =
         finalCopyParity (parityPathValue x.1))
       (χ : Fin (n + 1) → Bool → ∀ q : ℕ, DirichletCharacter ℂ q)
       (Q : Fin (n + 1) → Bool → Finset ℕ)
       (hχ : ∀ j b q, q ∈ Q j b → χ j b q ^ 2 ≠ 1)
       (e f : FinalParityReassignments n m) (hef : e ≠ f) :
       ∃ (x : ParityPathSum n × Fin m) (j : Fin (n + 1)) (b : Bool),
   …

   Mentions: OAI.Ostmann.FinalGraphVertex, OAI.Ostmann.anchorIncoming, OAI.Ostmann.parityPathValue, OAI.Ostmann.finalCopyParity, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.ParityPathSum