OAI/Combinatorics/HoneycombChords/PathComponents.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.ncard_neighbors line 22
2. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.ports_reachable line 26
3. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.path_neighbor_eq line 48
4. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.path_closed line 74
5. lemma OAI.CriticalHoneycomb.Transfer.PathComponents.residual_isCycles line 85
6. theorem OAI.CriticalHoneycomb.Transfer.PathComponents.path_and_cycles line 130

   Source documentation

   Every finite nonbranching two-port configuration is a path plus cycles. The path has no edge to the residual cycle graph.

   theorem path_and_cycles {a b : V} (hab : a ≠ b)
       (ha : G.degree a = 1) (hb : G.degree b = 1)
       (other : ∀ v, v ≠ a → v ≠ b → G.degree v = 0 ∨ G.degree v = 2) :
       ∃ p : G.Walk a b, p.IsPath ∧ (G \ p.toSubgraph.spanningCoe).IsCycles ∧
         ∀ v ∈ p.support, p.toSubgraph.neighborSet v = G.neighborSet v := by
   …

   Mentions: OAI.CriticalHoneycomb.Transfer.a, OAI.CriticalHoneycomb.Transfer.v

7. def OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.portRel line 154

   Source documentation

   The hard-wall two-port graph: the two exterior markers have only their prescribed incident edge; internal adjacency remains unchanged.

   def portRel (R : α → α → Prop) (a b : α) : (α ⊕ Bool) → (α ⊕ Bool) → Prop
     | .inl x, .inl y => R x y
     | .inr false, .inl y | .inl y, .inr false => y=a
     | .inr true, .inl y | .inl y, .inr true => y=b
     | .inr _, .inr _ => False

   Mentions: OAI.CriticalHoneycomb.Transfer.a

8. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.chain_snoc_ports line 160
9. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.chain_ports line 166
10. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.list_all_inl line 183
11. lemma OAI.CriticalHoneycomb.Transfer.FiniteConfigurations.support_decomposition line 195