OAI/NumberTheory/TwoPoint/Walks/ForestPathRealization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.list_idxOf_map_injective line 16
2. def OAI.TwoPointCorrelations.forestPathDataOfRepresentation line 29

   Source documentation

   Relabeling by Fin changes no forest index. The graph, walks, and non-reversal proofs are transported rather than postulated.

   noncomputable def forestPathDataOfRepresentation
       (G : SimpleGraph V) (hG : G.IsAcyclic) (hN : Fintype.card V ≤ N)
       (t : BinaryTree V) (ht : (forestNodes t).Nodup) (hc : ∀ v, v ∈ forestNodes t)
       (ha : ∀ a b, forestAdjacent t a b ↔ G.Adj a b) (color : V → Bool)
       (start finish : Fin segments → V) (p : ∀ i, G.Walk (start i) (finish i))
       (hp : ∀ i, List.IsChain (· ≠ ·) (p i).edges) : ForestPathData N segments := by
   …

   Mentions: OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.forestAdjacent, OAI.TwoPointCorrelations.ForestPathData

3. theorem OAI.TwoPointCorrelations.forestPathDataOfRepresentation_pattern line 67
4. theorem OAI.TwoPointCorrelations.forest_paths_realizable line 84

   Source documentation

   Every finite forest with boundedly many vertices and any family of reduced walks contributes to the single universal code universe.

   theorem forest_paths_realizable (G : SimpleGraph V) (hG : G.IsAcyclic)
       (hN : Fintype.card V ≤ N) (color : V → Bool)
       (start finish : Fin segments → V) (p : ∀ i, G.Walk (start i) (finish i))
       (hp : ∀ i, List.IsChain (· ≠ ·) (p i).edges) :
       ∃ t : BinaryTree V, (forestNodes t).Nodup ∧ (∀ v, v ∈ forestNodes t) ∧
         (fun i => (p i).support.map (fun v => (forestNodes t).idxOf v)) ∈
           Set.range (@ForestPathData.pattern N segments) := by
   …

   Mentions: OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.ForestPathData.pattern