The all-branches expansion

Defines ActiveExtensionChoice, a global choice of one-edge forest extension at every recursion node (nonempty by construction), and the depth-indexed all-branches expansion allBranchesExpansion with its boundary part and the analytic side conditions allBranchesAnalytic needed to push it one level deeper. The mixed partial of the interpolation family equals the expansion at every depth — the engine driving the proof of the BKAR forest interpolation formula (see BKAR.Formula).

@[reducible, inline]

abbrev BKAR.Forest.ActiveExtensionChoice (V : Type u_2) [Fintype V] [DecidableEq V] : Type u_2

A global choice of one-edge forest extension at every recursion node.

The all-branches induction expands every active edge of every forest it reaches; this is the one piece of structural data needed to name the next forest.

Equations

• BKAR.Forest.ActiveExtensionChoice V = ((F : BKAR.Forest V) → (e : ↥F.activeEdges) → F.ActiveExtension ↑e)

theorem BKAR.Forest.nonempty_activeExtensionChoice (V : Type u_2) [Fintype V] [DecidableEq V] : Nonempty (ActiveExtensionChoice V)

A global active-extension choice exists by noncomputably choosing the Forest representative obtained by inserting each active edge.

noncomputable def BKAR.Forest.allBranchesExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : ℕ → (F : Forest V) → List (Edge V) → List ℝ → ℝ → ((Edge V → ℝ) → ℝ) → ℝ

The level-n all-branches expansion from a recursion node.

At level zero it is the current fill-parameter remainder. At level n + 1 it exposes the current ordered-sector boundary term and recursively expands every active-edge remainder one level deeper.

Equations

• One or more equations did not get rendered due to their size.
• BKAR.Forest.allBranchesExpansion choices 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = BKAR.mixedPartialList x✝³.reverse x✝ (x✝⁴.interpWithFill (x✝⁴.paramsOfOrder x✝³ x✝²) x✝¹)

theorem BKAR.Forest.allBranchesExpansion_zero {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesExpansion choices 0 F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) top)

theorem BKAR.Forest.allBranchesExpansion_succ {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesExpansion choices (n + 1) F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, allBranchesExpansion choices n (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

noncomputable def BKAR.Forest.allBranchesBoundaryExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : ℕ → (F : Forest V) → List (Edge V) → List ℝ → ℝ → ((Edge V → ℝ) → ℝ) → ℝ

The pure boundary-sector tree with the same branching shape as allBranchesExpansion, but with no fill-parameter remainder at the leaves.

Equations

• One or more equations did not get rendered due to their size.
• BKAR.Forest.allBranchesBoundaryExpansion choices 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = BKAR.mixedPartialList x✝³.reverse x✝ (x✝⁴.standardInterp (x✝⁴.paramsOfOrder x✝³ x✝²))

theorem BKAR.Forest.allBranchesBoundaryExpansion_zero {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesBoundaryExpansion choices 0 F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs))

theorem BKAR.Forest.allBranchesBoundaryExpansion_succ {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesBoundaryExpansion choices (n + 1) F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices n (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

def BKAR.Forest.allBranchesAnalytic {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) : ℕ → (F : Forest V) → List (Edge V) → List ℝ → ℝ → ((Edge V → ℝ) → ℝ) → Prop

Analytic assumptions needed by the finite all-branches induction through n further layers from a node.

This is a precise recursion-tree version of the usual smoothness and integrability requirements; the final smoothness API will discharge it in one place rather than weakening the induction theorem.

Equations

• One or more equations did not get rendered due to their size.
• BKAR.Forest.allBranchesAnalytic choices 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = True

theorem BKAR.Forest.allBranchesAnalytic_zero {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesAnalytic choices 0 F pref prefixTs top ρ

theorem BKAR.Forest.allBranchesAnalytic_of_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {m n : ℕ} {F : Forest V} {pref : List (Edge V)} {prefixTs : List ℝ} {top : ℝ} {ρ : (Edge V → ℝ) → ℝ} : m ≤ n → allBranchesAnalytic choices n F pref prefixTs top ρ → allBranchesAnalytic choices m F pref prefixTs top ρ

Analytic recursion-tree hypotheses can be truncated to a shallower depth.

theorem BKAR.Forest.mixedPartialList_interpWithFill_eq_allBranchesExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : pref.toFinset = F.edges → prefixTs.length = pref.length → allBranchesAnalytic choices n F pref prefixTs top ρ → mixedPartialList pref.reverse ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) top) = allBranchesExpansion choices n F pref prefixTs top ρ

The all-branches induction invariant: expanding every active edge for n layers preserves the current fill-parameter remainder.

theorem BKAR.Forest.allBranchesExpansion_succ_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hF : F.activeEdges = ∅) : allBranchesExpansion choices (n + 1) F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs))

Once a node has no active edges, every positive all-branches level is just its boundary ordered-sector term.

theorem BKAR.Forest.allBranchesExpansion_stable_of_activeEdges_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → allBranchesExpansion choices (n + 1) F pref prefixTs top ρ = allBranchesExpansion choices n F pref prefixTs top ρ

Once the remaining depth dominates the number of active edges at a node, adding one more all-branches layer does not change the expansion.

theorem BKAR.Forest.allBranchesExpansion_activeEdges_card_add {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (k : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesExpansion choices (F.activeEdges.card + k) F pref prefixTs top ρ = allBranchesExpansion choices F.activeEdges.card F pref prefixTs top ρ

The exact active-edge count is a canonical terminal depth for the all-branches expansion: any extra fuel beyond that depth gives the same value.

theorem BKAR.Forest.allBranchesExpansion_eq_boundaryExpansion_of_activeEdges_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → allBranchesExpansion choices n F pref prefixTs top ρ = allBranchesBoundaryExpansion choices n F pref prefixTs top ρ

At any depth at least the active-edge count, the all-branches expansion has no fill-parameter leaves left: it is exactly the pure boundary-sector tree.

theorem BKAR.Forest.allBranchesExpansion_activeEdges_card_eq_boundaryExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesExpansion choices F.activeEdges.card F pref prefixTs top ρ = allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ

Exact active-depth terminalization of the all-branches expansion.

theorem BKAR.Forest.allBranchesBoundaryExpansion_stable_of_activeEdges_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → allBranchesBoundaryExpansion choices (n + 1) F pref prefixTs top ρ = allBranchesBoundaryExpansion choices n F pref prefixTs top ρ

The pure boundary-sector tree also stabilizes once the remaining depth dominates the active-edge count.

theorem BKAR.Forest.allBranchesBoundaryExpansion_activeEdges_card_add {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (k : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesBoundaryExpansion choices (F.activeEdges.card + k) F pref prefixTs top ρ = allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ

Extra boundary-tree fuel beyond active depth gives the same value.

theorem BKAR.Forest.allBranchesBoundaryExpansion_eq_activeEdges_card_of_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hle : F.activeEdges.card ≤ n) : allBranchesBoundaryExpansion choices n F pref prefixTs top ρ = allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ

Collapse any sufficiently deep boundary tree to exact active depth.

theorem BKAR.Forest.allBranchesBoundaryExpansion_activeEdges_card_eq_standard_add_sum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

Exact-depth unfolding of the boundary-sector tree. Each recursive child is already evaluated at its own exact active depth.

theorem BKAR.Forest.allBranchesBoundaryExpansion_activeEdges_card_of_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hF : F.activeEdges = ∅) : allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs))

Exact-depth boundary expansion at a terminal node is just its boundary term.

theorem BKAR.Forest.mixedPartialList_interpWithFill_eq_allBranchesBoundaryExpansion_activeEdges_card {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : mixedPartialList pref.reverse ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) top) = allBranchesBoundaryExpansion choices F.activeEdges.card F pref prefixTs top ρ

Exact-depth boundary expansion equals the current fill-parameter remainder under the corresponding all-branches analytic hypotheses.

theorem BKAR.Forest.mixedPartialList_cons_interpWithFill_eq_allBranchesBoundaryExpansion_child {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) {t : ℝ} (ht : t ∈ Set.uIcc 0 top) : mixedPartialList (↑e :: pref.reverse) ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) t) = allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

An active-edge summand in the parent fill-parameter remainder is exactly the exact-depth boundary subtree below that active child.

theorem BKAR.Forest.intervalIntegrable_allBranchesBoundaryExpansion_activeEdges_card_child {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : IntervalIntegrable (fun (t : ℝ) => allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ) MeasureTheory.volume 0 top

The exact-depth boundary subtree below an active child is interval-integrable whenever the parent exact-depth all-branches analytic hypotheses hold.

theorem BKAR.Forest.integral_mixedPartial_cons_interpolation_eq_integral_boundaryExpansion_child {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: pref.reverse) ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) t) = ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

Integral form of the parent-summand/child-boundary identification.

theorem BKAR.Forest.mixedPartial_eq_standard_add_sum_boundaryExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : mixedPartialList pref.reverse ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) top) = mixedPartialList pref.reverse ρ (F.standardInterp (F.paramsOfOrder pref prefixTs)) + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ

Arbitrary-node exact-depth recursion: the current fill-parameter remainder is the local boundary sector plus exact-depth boundary subtrees below all active children.

theorem BKAR.Forest.rho_oneConfig_eq_allBranchesExpansion_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices n (empty V) [] [] 1 ρ) : ρ oneConfig = allBranchesExpansion choices n (empty V) [] [] 1 ρ

Root form of the all-branches induction, specialized to the empty forest and the all-one endpoint.

theorem BKAR.Forest.rho_oneConfig_eq_allBranchesBoundaryExpansion_empty_activeEdges_card {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = allBranchesBoundaryExpansion choices (empty V).activeEdges.card (empty V) [] [] 1 ρ

Root all-branches identity at the canonical active depth, with the expansion already rewritten as the pure boundary-sector tree.

theorem BKAR.Forest.rho_oneConfig_eq_orderedSectorSum_empty_add_sum_allBranchesBoundaryExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = (empty V).orderedSectorSum ρ + ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, allBranchesBoundaryExpansion choices (choices (empty V) e).forest.activeEdges.card (choices (empty V) e).forest [↑e] [t] t ρ

Root exact-depth recursion in boundary-sector form: the BKAR value is the empty sector plus the exact-depth boundary trees below each first active edge.

theorem BKAR.Forest.integral_prefixed_standardInterp_singleton_eq_orderedSimplexIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (G : Forest V) (e : Edge V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : ∫ (t : ℝ) in 0..top, mixedPartialList (pref ++ [e]).reverse ρ (G.standardInterp (G.paramsOfOrder (pref ++ [e]) (prefixTs ++ [t]))) = orderedSimplexIntegralAux top [e] fun (ts : List ℝ) => mixedPartialList (pref ++ [e]).reverse ρ (G.standardInterp (G.paramsOfOrder (pref ++ [e]) (prefixTs ++ ts)))

The first boundary sector of a prefixed one-edge child is its one-edge ordered simplex integral.

theorem BKAR.Forest.integral_standardInterp_empty_singleton_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (G : Forest V) (e : Edge V) (ρ : (Edge V → ℝ) → ℝ) : ∫ (t : ℝ) in 0..1, mixedPartialList [e].reverse ρ (G.standardInterp (G.paramsOfOrder [e] [t])) = G.orderedContribution [e] ρ

The first boundary sector of any one-edge child from the empty forest is the corresponding one-edge ordered contribution. No terminality is needed here.

theorem BKAR.Forest.integral_allBranchesBoundaryExpansion_child_eq_integral_standard_add_sum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ = ∫ (t : ℝ) in 0..top, mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t]))) + ∑ e' ∈ (choices F e).forest.activeEdges.attach, ∫ (s : ℝ) in 0..t, allBranchesBoundaryExpansion choices (choices (choices F e).forest e').forest.activeEdges.card (choices (choices F e).forest e').forest (pref ++ [↑e] ++ [↑e']) (prefixTs ++ [t] ++ [s]) s ρ

Unfold one child exact-depth boundary subtree under its parent integral. This is the nonterminal regrouping shape before applying interval-integral linearity.

theorem BKAR.Forest.integral_mixedPartialList_cons_interpWithFill_eq_integral_child_standard_add_sum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : ∫ (t : ℝ) in 0..top, mixedPartialList (↑e :: pref.reverse) ρ (F.interpWithFill (F.paramsOfOrder pref prefixTs) t) = ∫ (t : ℝ) in 0..top, mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t]))) + ∑ e' ∈ (choices F e).forest.activeEdges.attach, ∫ (s : ℝ) in 0..t, allBranchesBoundaryExpansion choices (choices (choices F e).forest e').forest.activeEdges.card (choices (choices F e).forest e').forest (pref ++ [↑e] ++ [↑e']) (prefixTs ++ [t] ++ [s]) s ρ

One active-edge summand, after exact-depth all-branches expansion below that edge, is the integral of the child's local boundary sector plus its recursive exact-depth child subtrees.

theorem BKAR.Forest.rho_oneConfig_eq_orderedSectorSum_empty_add_sum_integral_child_standard_add_sum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) : ρ oneConfig = (empty V).orderedSectorSum ρ + ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, mixedPartialList [↑e].reverse ρ ((choices (empty V) e).forest.standardInterp ((choices (empty V) e).forest.paramsOfOrder [↑e] [t])) + ∑ e' ∈ (choices (empty V) e).forest.activeEdges.attach, ∫ (s : ℝ) in 0..t, allBranchesBoundaryExpansion choices (choices (choices (empty V) e).forest e').forest.activeEdges.card (choices (choices (empty V) e).forest e').forest ([↑e] ++ [↑e']) ([t] ++ [s]) s ρ

Root boundary-tree identity with every first child unfolded once. The recursive grandchildren are still exact-depth boundary subtrees.

theorem BKAR.Forest.integral_boundaryExpansion_singleton_eq_prefixed_simplexIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (G : Forest V) (e : Edge V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hG : G.activeEdges = ∅) : ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices G.activeEdges.card G (pref ++ [e]) (prefixTs ++ [t]) t ρ = orderedSimplexIntegralAux top [e] fun (ts : List ℝ) => mixedPartialList (pref ++ [e]).reverse ρ (G.standardInterp (G.paramsOfOrder (pref ++ [e]) (prefixTs ++ ts)))

Terminal one-edge children at any prefixed recursion node are exactly the corresponding prefixed one-edge ordered simplex.

theorem BKAR.Forest.integral_allBranchesBoundaryExpansion_eq_terminalSingletonBranchIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (e : ↥F.activeEdges) (pref : List (Edge V)) (prefixTs : List ℝ) (hpref : pref.toFinset = F.edges) (hprefixTs : prefixTs.length = pref.length) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) (hterm : (choices F e).forest.activeEdges = ∅) : ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ = (TerminalGrowth.cons (choices F e) (TerminalGrowth.ofActiveEdgesEqEmpty (choices F e).forest hterm)).branchIntegralAux top (F.paramsOfOrder pref prefixTs) (mixedPartialList pref.reverse ρ)

A terminal child of the all-branches boundary tree is the singleton terminal branch integral already used by the ordered-assembly API.

theorem BKAR.Forest.integral_allBranchesBoundaryExpansion_empty_singleton_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (e : ↥(empty V).activeEdges) (ρ : (Edge V → ℝ) → ℝ) (hterm : (choices (empty V) e).forest.activeEdges = ∅) : ∫ (t : ℝ) in 0..1, allBranchesBoundaryExpansion choices (choices (empty V) e).forest.activeEdges.card (choices (empty V) e).forest [↑e] [t] t ρ = (choices (empty V) e).forest.orderedContribution [↑e] ρ

Terminal first-edge children in the boundary tree are exactly the corresponding one-edge ordered-sector contributions.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_orderedContributionSum_of_terminalChildren {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hterm : ∀ (e : ↥(empty V).activeEdges), (choices (empty V) e).forest.activeEdges = ∅) : ρ oneConfig = (empty V).orderedSectorSum ρ + ∑ e ∈ (empty V).activeEdges.attach, (choices (empty V) e).forest.orderedContribution [↑e] ρ

Root base case for the support/order regrouping: if every first active-edge child is already terminal, the boundary tree has only empty and one-edge ordered sectors.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_singleton_branchIntegral_of_terminalChildren {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hterm : ∀ (e : ↥(empty V).activeEdges), (choices (empty V) e).forest.activeEdges = ∅) : ρ oneConfig = (empty V).orderedSectorSum ρ + (ActiveTerminalBranchData.singleton (fun (e : ↥(empty V).activeEdges) => choices (empty V) e) hterm).branchIntegral emptyParam ρ

Root terminal-child base case, expressed through the singleton ActiveTerminalBranchData branch sum.

theorem BKAR.Forest.rho_oneConfig_eq_orderedSectorSum_empty_add_singleton_supportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hterm : ∀ (e : ↥(empty V).activeEdges), (choices (empty V) e).forest.activeEdges = ∅) : ρ oneConfig = (empty V).orderedSectorSum ρ + ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, (ActiveTerminalBranchData.singleton (fun (e : ↥(empty V).activeEdges) => choices (empty V) e) hterm).supportOrderContribution I order ρ

Root terminal-child base case, already regrouped by finite support and canonical edge order.