Branch integrals and ordered contributions from the empty forest

For ordered growths starting at the empty forest, identifies the recursion's branch integrals with the intrinsic ordered contributions of the grown forest, and records how the growth order and its tail sit inside the enumerations of the final edge set. This links the recursion's bookkeeping to the per-order sector integrals of the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.Forest.OrderedGrowth.order_mem_edgeOrders_of_initial_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} (h : F.OrderedGrowth order G) (hF : F.edges = ∅) : order ∈ G.edgeOrders

An ordered growth from an initially empty edge set carries one of the canonical edge orderings of its terminal forest.

theorem BKAR.Forest.OrderedGrowth.order_mem_edgeOrders_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] {G : Forest V} {order : List (Edge V)} (h : (empty V).OrderedGrowth order G) : order ∈ G.edgeOrders

theorem BKAR.Forest.OrderedGrowth.tail_order_mem_edgeSetOrders_erase_of_initial_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F G : Forest V} {order : List (Edge V)} {e : Edge V} (h : F.OrderedGrowth (e :: order) G) (hF : F.edges = ∅) : order ∈ edgeSetOrders (G.edges.erase e)

If an ordered growth starts from an empty edge set and has a first edge, then the remaining growth order is a canonical ordering of the terminal edge set with that first edge erased.

theorem BKAR.Forest.OrderedGrowth.tail_order_mem_edgeSetOrders_erase_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] {G : Forest V} {order : List (Edge V)} {e : Edge V} (h : (empty V).OrderedGrowth (e :: order) G) : order ∈ edgeSetOrders (G.edges.erase e)

theorem BKAR.Forest.TerminalGrowth.order_mem_edgeOrders_of_initial_edges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (hF : F.edges = ∅) : data.order ∈ data.terminal.edgeOrders

A terminal branch grown from an initially empty edge set carries one of the canonical edge orderings of its terminal forest.

theorem BKAR.Forest.TerminalGrowth.order_mem_edgeOrders_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) : data.order ∈ data.terminal.edgeOrders

theorem BKAR.Forest.TerminalGrowth.tail_order_mem_edgeSetOrders_erase_of_order_eq_cons {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) {e : Edge V} {order : List (Edge V)} (horder : data.order = e :: order) : order ∈ edgeSetOrders (data.terminal.edges.erase e)

If an empty-start terminal branch order is nonempty, its tail is one of the canonical orders of the terminal edge set with the first edge erased.

theorem BKAR.Forest.TerminalGrowth.orderTail_mem_edgeSetOrderTails_of_order_eq_cons {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) {e : Edge V} {order : List (Edge V)} (horder : data.order = e :: order) : ∃ (he : e ∈ data.terminal.edges), ⟨⟨e, he⟩, order⟩ ∈ edgeSetOrderTails data.terminal.edges

A nonempty empty-start terminal branch gives a member of the terminal first-edge/tail-order indexing set.

theorem BKAR.Forest.TerminalGrowth.branchIntegral_emptyStart_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (data : (empty V).TerminalGrowth) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegral emptyParam ρ = data.terminal.orderedContribution data.order ρ

An empty-start terminal branch integral is the canonical ordered-sector contribution of its terminal forest and terminal edge order.

theorem BKAR.Forest.TerminalGrowth.branchIntegralAux_mixedPartial_eq_simplexIntegralAux_paramsOfOrder_append {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} (data : F.TerminalGrowth) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : data.branchIntegralAux top (F.paramsOfOrder pref prefixTs) (mixedPartialList pref.reverse ρ) = orderedSimplexIntegralAux top data.order fun (ts : List ℝ) => mixedPartialList (pref ++ data.order).reverse ρ (data.terminal.standardInterp (data.terminal.paramsOfOrder (pref ++ data.order) (prefixTs ++ ts)))

A terminal tail integral at a nonempty recursion node can be read as the ordered simplex for the accumulated prefix followed by the tail order.

theorem BKAR.Forest.TerminalGrowth.cons_orderedContribution_eq_integral_tail_branchIntegralAux_emptyStart {V : Type u_1} [Fintype V] [DecidableEq V] {e : Edge V} (h : (empty V).ActiveExtension e) (tail : h.forest.TerminalGrowth) (ρ : (Edge V → ℝ) → ℝ) : tail.terminal.orderedContribution (e :: tail.order) ρ = ∫ (t : ℝ) in 0..1, tail.branchIntegralAux t (⋯.extendParam emptyParam t) (partialDeriv e ρ)

For a terminal branch obtained by first adding e from the empty forest, the corresponding ordered-sector contribution is exactly the recursive tail integral after that first edge.