Following a prescribed order through the choice system

Defines ChosenGrowth, the ordered growth that follows exactly the active extensions selected by a fixed ActiveExtensionChoice, and the partial function followOrder attempting to realize a prescribed edge order as such a growth. Every chosen growth arises this way, giving the canonical realization of a support/order fiber used by the fiber bridge.

inductive BKAR.Forest.ChosenGrowth {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : Forest V → List (Edge V) → Forest V → Prop

An ordered growth that follows exactly the active extensions selected by a fixed ActiveExtensionChoice.

• nil {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} (F : Forest V) : ChosenGrowth choices F [] F
• cons {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} {F G : Forest V} {e : Edge V} {order : List (Edge V)} (he : e ∈ F.activeEdges) (tail : ChosenGrowth choices (choices F ⟨e, he⟩).forest order G) : ChosenGrowth choices F (e :: order) G

theorem BKAR.Forest.ChosenGrowth.edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} {F G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices F order G) : G.edges = order.toFinset ∪ F.edges

Edge-set bookkeeping for a chosen growth path.

theorem BKAR.Forest.ChosenGrowth.support_edges_eq_toFinset_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] {choices : ActiveExtensionChoice V} {G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices (empty V) order G) : G.support.edges = order.toFinset

Root-start edge-set bookkeeping for a chosen growth path.

noncomputable def BKAR.Forest.followOrderOption {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : Forest V → List (Edge V) → Option (Forest V)

Follow an edge order through the active extensions selected by choices.

Equations

• BKAR.Forest.followOrderOption choices x✝ [] = some x✝
• BKAR.Forest.followOrderOption choices x✝ (e :: order) = if he : e ∈ x✝.activeEdges then BKAR.Forest.followOrderOption choices (choices x✝ ⟨e, he⟩).forest order else none

theorem BKAR.Forest.chosenGrowth_of_followOrderOption_eq_some {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {F G : Forest V} {order : List (Edge V)} : followOrderOption choices F order = some G → ChosenGrowth choices F order G

theorem BKAR.Forest.exists_followOrderOption_eq_some_of_acyclic_union {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {F : Forest V} {S : Finset (Edge V)} (order : List (Edge V)) : IsAcyclicEdgeSet S → order.toFinset ∪ F.edges = S → order.Nodup → Disjoint order.toFinset F.edges → ∃ (G : Forest V), followOrderOption choices F order = some G ∧ G.edges = S

Canonical orders of an acyclic target support can be followed through any choice of active extensions. The invariant says that the current Forest representative carries the already-consumed prefix, while order is the remaining suffix and S is the final edge set.

theorem BKAR.Forest.exists_followOrderOption_eq_some_support_of_mem_edgeSetOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {I : ForestIndex V} {order : List (Edge V)} (horder : order ∈ edgeSetOrders I.edges) : ∃ (G : Forest V), followOrderOption choices (empty V) order = some G ∧ G.support = I

Every canonical order of a forest index follows to some Forest representative whose support is exactly that index, independently of the extension choices.