Growth-order bookkeeping for terminal branches

For the terminal branch data of the recursion started at the empty forest, records how the growth order relates to the final support: the order enumerates the support edge set, its tail enumerates the support minus the first edge, and growthOrderTail packages this decomposition. These facts index the regrouping of branch contributions by support and order in the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order_mem_edgeOrders_of_initial_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.ActiveTerminalBranchData) (hF : F.edges = ∅) (e : ↥F.activeEdges) : ↑e :: (data.tail e).order ∈ (data.growth e).terminal.edgeOrders

Every full branch selected by active-terminal branch data from an initially empty edge set carries a canonical ordering of its terminal forest.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order_mem_edgeOrders_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : ↑e :: (data.tail e).order ∈ (data.growth e).terminal.edgeOrders

theorem BKAR.Forest.ActiveTerminalBranchData.growth_terminal_edges_eq_toFinset_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (data.growth e).terminal.edges = (↑e :: (data.tail e).order).toFinset

For an active-terminal branch from the empty forest, the terminal edge set is exactly the edge set represented by the selected first edge and tail order.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_support_edges_eq_toFinset_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (data.growth e).support.edges = (↑e :: (data.tail e).order).toFinset

The support index of an active-terminal branch from the empty forest carries the same edge set as its selected first-edge/tail order.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_order_toFinset_eq_terminal_edges_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (↑e :: (data.tail e).order).toFinset = (data.growth e).terminal.edges

theorem BKAR.Forest.ActiveTerminalBranchData.growth_terminal_edges_nonempty_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (data.growth e).terminal.edges.Nonempty

Every active-terminal branch selected from the empty forest has a nonempty terminal edge set: it contains the first active edge of the branch.

theorem BKAR.Forest.ActiveTerminalBranchData.tail_order_mem_edgeSetOrders_terminal_erase_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (data.tail e).order ∈ edgeSetOrders ((data.growth e).terminal.edges.erase ↑e)

The tail order selected after the first active edge of an empty-start active-terminal branch is a canonical ordering of the terminal edge set with that first edge erased.

theorem BKAR.Forest.ActiveTerminalBranchData.growth_orderTail_mem_edgeSetOrderTails_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : ∃ (he : ↑e ∈ (data.growth e).terminal.edges), ⟨⟨↑e, he⟩, (data.tail e).order⟩ ∈ edgeSetOrderTails (data.growth e).terminal.edges

Each selected active-terminal branch from the empty forest determines a member of the terminal first-edge/tail-order indexing set.

def BKAR.Forest.ActiveTerminalBranchData.growthOrderTail {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (_ : ↥(data.growth e).terminal.edges) × List (Edge V)

The terminal first-edge/tail sector selected by one active-terminal branch from the empty forest.

Equations

• data.growthOrderTail e = ⟨⟨↑e, ⋯⟩, (data.tail e).order⟩

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrderTail_first {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : ↑(data.growthOrderTail e).fst = ↑e

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrderTail_tail {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : (data.growthOrderTail e).snd = (data.tail e).order

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrderTail_order {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : ↑(data.growthOrderTail e).fst :: (data.growthOrderTail e).snd = ↑e :: (data.tail e).order

def BKAR.Forest.ActiveTerminalBranchData.growthOrder {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : List (Edge V)

The selected terminal edge order of one active-terminal branch.

Equations

• data.growthOrder e = ↑(data.growthOrderTail e).fst :: (data.growthOrderTail e).snd

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrder_eq {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : data.growthOrder e = ↑e :: (data.tail e).order

theorem BKAR.Forest.ActiveTerminalBranchData.growthOrderTail_mem_edgeSetOrderTails_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) : data.growthOrderTail e ∈ edgeSetOrderTails (data.growth e).terminal.edges

theorem BKAR.Forest.ActiveTerminalBranchData.growth_terminal_orderedSectorSum_eq_sum_orderTails_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (e : ↥(empty V).activeEdges) (ρ : (Edge V → ℝ) → ℝ) : (data.growth e).terminal.orderedSectorSum ρ = ∑ x ∈ edgeSetOrderTails (data.growth e).terminal.edges, (data.growth e).terminal.orderedContribution (↑x.fst :: x.snd) ρ

Each selected terminal forest admits the same first-edge/tail ordered-sector decomposition as any nonempty forest.

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegral_empty_eq_sum_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = ∑ e ∈ (empty V).activeEdges.attach, (data.growth e).terminal.orderedContribution (↑e :: (data.tail e).order) ρ

The active-terminal branch sum from the empty forest is a finite sum of canonical ordered-sector contributions, one for each selected terminal branch.

theorem BKAR.Forest.ActiveTerminalBranchData.branchIntegral_empty_eq_sum_growthOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).ActiveTerminalBranchData) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = ∑ e ∈ (empty V).activeEdges.attach, (data.growth e).terminal.orderedContribution (data.growthOrder e) ρ

Version of ActiveTerminalBranchData.branchIntegral_empty_eq_sum_orderedContribution using the packaged terminal edge order.