Ordered forest growth certificates

Defines OrderedGrowth F order G, the certificate that the forest G is obtained from F by adding the edges of the list order one at a time, each step being a valid one-edge forest extension. Provides accessors for the first step and tail growth and the basic bookkeeping (edge sets, cardinalities) used throughout the ordered expansion of the BKAR forest interpolation formula (see BKAR.Formula).

inductive BKAR.Forest.OrderedGrowth {V : Type u_1} [Fintype V] [DecidableEq V] : Forest V → List (Edge V) → Forest V → Type u_1

Certificate that G is obtained from F by adding the edges in order, one at a time, with a valid one-edge forest extension at each step.

• nil {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.OrderedGrowth [] F
• cons {V : Type u_1} [Fintype V] [DecidableEq V] {F F' G : Forest V} {e : Edge V} {order : List (Edge V)} (step : F.EdgeExtension F' e) (tail : F'.OrderedGrowth order G) : F.OrderedGrowth (e :: order) G

structure BKAR.Forest.OrderedGrowth.ConsData {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (e : Edge V) (order : List (Edge V)) (G : Forest V) : Type u_1

The intermediate forest, first extension, and tail of a nonempty ordered growth.

• forest : Forest V

  The intermediate forest after the first edge is adjoined.

• step : F.EdgeExtension self.forest e
• tail : self.forest.OrderedGrowth order G

  The remaining ordered growth from the intermediate forest to the final forest.

def BKAR.Forest.OrderedGrowth.consData {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : ConsData F e order G

Decompose a nonempty ordered growth into its first step and tail growth.

Equations

• One or more equations did not get rendered due to their size.

def BKAR.Forest.OrderedGrowth.tailForest {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : Forest V

The intermediate forest after the first step of a nonempty ordered growth.

Equations

• h.tailForest = h.consData.forest

theorem BKAR.Forest.OrderedGrowth.firstStep {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : F.EdgeExtension h.tailForest e

The first one-edge extension in a nonempty ordered growth.

def BKAR.Forest.OrderedGrowth.tailGrowth {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : h.tailForest.OrderedGrowth order G

The remaining ordered growth after the first step.

Equations

• h.tailGrowth = h.consData.tail

def BKAR.Forest.OrderedGrowth.firstActiveExtension {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : F.ActiveExtension e

The first edge of a nonempty ordered growth is active for the starting forest.

Equations

• h.firstActiveExtension = { forest := h.tailForest, extension := ⋯ }

theorem BKAR.Forest.OrderedGrowth.first_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : e ∈ F.activeEdges

theorem BKAR.Forest.OrderedGrowth.first_not_mem_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : e ∉ F.edges

theorem BKAR.Forest.OrderedGrowth.tailForest_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : h.tailForest.edges = insert e F.edges

theorem BKAR.Forest.OrderedGrowth.tailForest_card_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : h.tailForest.edges.card = F.edges.card + 1

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

Edge-set bookkeeping for an ordered growth certificate.

theorem BKAR.Forest.OrderedGrowth.tailGrowth_edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : G.edges = order.toFinset ∪ h.tailForest.edges

def BKAR.Forest.OrderedGrowth.support {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (_h : F.OrderedGrowth order G) : ForestIndex V

The finite forest index grown by an ordered growth.

Equations

• _h.support = G.support

theorem BKAR.Forest.OrderedGrowth.support_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : h.support.edges = G.edges

theorem BKAR.Forest.OrderedGrowth.support_edges_eq_toFinset_union {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : h.support.edges = order.toFinset ∪ F.edges

theorem BKAR.Forest.OrderedGrowth.order_toFinset_subset_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : order.toFinset ⊆ G.edges

theorem BKAR.Forest.OrderedGrowth.initial_edges_subset_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : F.edges ⊆ G.edges

theorem BKAR.Forest.OrderedGrowth.mem_edges_of_mem_order {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) {e : Edge V} (he : e ∈ order) : e ∈ G.edges

theorem BKAR.Forest.OrderedGrowth.order_toFinset_disjoint_initial_edges {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : Disjoint order.toFinset F.edges

The ordered-growth list is disjoint from the starting forest's edge set.

theorem BKAR.Forest.OrderedGrowth.order_nodup {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : order.Nodup

An ordered-growth list never repeats an edge.

theorem BKAR.Forest.OrderedGrowth.order_toFinset_card_eq_length {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : order.toFinset.card = order.length

theorem BKAR.Forest.OrderedGrowth.card_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) : G.edges.card = F.edges.card + order.length

The final forest has exactly order.length more edges than the start.

theorem BKAR.Forest.OrderedGrowth.tailGrowth_card_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {e : Edge V} {order : List (Edge V)} (h : F.OrderedGrowth (e :: order) G) : G.edges.card = h.tailForest.edges.card + order.length