Regrouping the all-branches expansion by support and order

Regroups one level of the all-branches expansion by the support grown and the order followed: defines the local boundary support and support/order contributions and proves the finite regrouping identities expressing the expansion's boundary terms as sums over supports and their enumerating orders.

theorem BKAR.Forest.activeExtension_forest_support_eq_singleton_empty {V : Type u_1} [Fintype V] [DecidableEq V] {e : Edge V} (h : (empty V).ActiveExtension e) : h.forest.support = ForestIndex.singleton e

A one-edge active extension from the empty forest has singleton support.

theorem BKAR.Forest.activeExtension_singleton_order_mem_edgeSetOrders_of_support_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] {e : Edge V} (h : (empty V).ActiveExtension e) {I : ForestIndex V} (hsupport : h.forest.support = I) : [e] ∈ edgeSetOrders I.edges

The singleton order attached to an empty-start active extension is canonical in any support fiber containing that extension.

theorem BKAR.Forest.activeExtension_prefixed_order_mem_edgeSetOrders_of_support_eq {V : Type u_1} [Fintype V] [DecidableEq V] {F : Forest V} {e : Edge V} (h : F.ActiveExtension e) {pref : List (Edge V)} (hpref : pref.toFinset = F.edges) (hnodup : pref.Nodup) {I : ForestIndex V} (hsupport : h.forest.support = I) : pref ++ [e] ∈ edgeSetOrders I.edges

At an arbitrary recursion node, appending the chosen active edge to an existing canonical prefix gives a canonical order of the child support.

noncomputable def BKAR.Forest.localBoundarySupportContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Local active-boundary sectors from a recursion node whose child forest has a fixed support.

Equations

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

theorem BKAR.Forest.localBoundarySupportContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : localBoundarySupportContribution choices F pref prefixTs top I ρ = ∑ e ∈ F.activeEdges.attach with (choices F e).forest.support = I, orderedSimplexIntegralAux top [↑e] fun (ts : List ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ ts)))

noncomputable def BKAR.Forest.localBoundarySupportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Local active-boundary sectors from a recursion node with fixed child support and fixed canonical order.

Equations

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

theorem BKAR.Forest.localBoundarySupportOrderContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ = ∑ e ∈ F.activeEdges.attach with (choices F e).forest.support = I ∧ pref ++ [↑e] = order, orderedSimplexIntegralAux top [↑e] fun (ts : List ℝ) => mixedPartialList order.reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder order (prefixTs ++ ts)))

theorem BKAR.Forest.localBoundarySupportOrderContribution_eq_zero_of_length_ne {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (hne : order.length ≠ pref.length + 1) : localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ = 0

A local support/order boundary sector can contribute only when the requested order is obtained by appending exactly one edge to the current prefix.

theorem BKAR.Forest.sum_localBoundarySupportContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : (∑ e ∈ F.activeEdges.attach, orderedSimplexIntegralAux top [↑e] fun (ts : List ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ ts)))) = ∑ I : ForestIndex V, localBoundarySupportContribution choices F pref prefixTs top I ρ

Local active-boundary sectors regroup by child support.

theorem BKAR.Forest.localBoundarySupportContribution_eq_sum_supportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (hpref : pref.toFinset = F.edges) (hnodup : pref.Nodup) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : localBoundarySupportContribution choices F pref prefixTs top I ρ = ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ

A local support fiber splits by canonical child order.

theorem BKAR.Forest.sum_localBoundarySupportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (hpref : pref.toFinset = F.edges) (hnodup : pref.Nodup) (ρ : (Edge V → ℝ) → ℝ) : (∑ e ∈ F.activeEdges.attach, orderedSimplexIntegralAux top [↑e] fun (ts : List ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ ts)))) = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ

Local active-boundary sectors regroup by child support and order.

noncomputable def BKAR.Forest.firstBoundarySupportContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Contribution of exposed one-edge boundary sectors whose child forest has a fixed finite support.

Equations

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

theorem BKAR.Forest.firstBoundarySupportContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : firstBoundarySupportContribution choices I ρ = ∑ e ∈ (empty V).activeEdges.attach with (choices (empty V) e).forest.support = I, (choices (empty V) e).forest.orderedContribution [↑e] ρ

noncomputable def BKAR.Forest.firstBoundarySupportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Contribution of exposed one-edge boundary sectors with fixed support and fixed canonical edge order.

Equations

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

theorem BKAR.Forest.firstBoundarySupportOrderContribution_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : firstBoundarySupportOrderContribution choices I order ρ = ∑ e ∈ (empty V).activeEdges.attach with (choices (empty V) e).forest.support = I ∧ [↑e] = order, (choices (empty V) e).forest.orderedContribution order ρ

theorem BKAR.Forest.firstBoundarySupportContribution_eq_localBoundarySupportContribution_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : firstBoundarySupportContribution choices I ρ = localBoundarySupportContribution choices (empty V) [] [] 1 I ρ

The root support fiber is the empty-prefix instance of the local API.

theorem BKAR.Forest.firstContribution_eq_boundaryContribution_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : firstBoundarySupportOrderContribution choices I order ρ = localBoundarySupportOrderContribution choices (empty V) [] [] 1 I order ρ

The root support/order fiber is the empty-prefix instance of the local API.

theorem BKAR.Forest.sum_firstBoundarySupportContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ∑ e ∈ (empty V).activeEdges.attach, (choices (empty V) e).forest.orderedContribution [↑e] ρ = ∑ I : ForestIndex V, firstBoundarySupportContribution choices I ρ

Exposed first boundary sectors regroup by finite support.

theorem BKAR.Forest.firstBoundarySupportContribution_eq_sum_supportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : firstBoundarySupportContribution choices I ρ = ∑ order ∈ edgeSetOrders I.edges, firstBoundarySupportOrderContribution choices I order ρ

A support fiber of exposed first sectors splits by canonical edge order.

theorem BKAR.Forest.sum_firstBoundarySupportOrderContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ∑ e ∈ (empty V).activeEdges.attach, (choices (empty V) e).forest.orderedContribution [↑e] ρ = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, firstBoundarySupportOrderContribution choices I order ρ

Exposed first boundary sectors regroup by support and canonical order.

noncomputable def BKAR.Forest.firstRecursiveBoundaryRemainder {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

The first recursive boundary remainder after exposing and regrouping all one-edge sectors below the empty forest.

Equations

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

theorem BKAR.Forest.firstRecursiveBoundaryRemainder_def {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : firstRecursiveBoundaryRemainder choices ρ = ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, ∑ 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 ρ

theorem BKAR.Forest.firstRecursiveBoundaryRemainder_eq_zero_of_forall_child_activeEdges_eq_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hterm : ∀ (e : ↥(empty V).activeEdges), (choices (empty V) e).forest.activeEdges = ∅) : firstRecursiveBoundaryRemainder choices ρ = 0

If every first child is already terminal, the recursive boundary remainder is zero.

theorem BKAR.Forest.allBranchesAnalytic.child_standard_intervalIntegrable {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 → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : IntervalIntegrable (fun (t : ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t])))) MeasureTheory.volume 0 top

The child first-sector integrability contained in allBranchesAnalytic.

theorem BKAR.Forest.allBranchesAnalytic.child_recursive_sum_intervalIntegrable {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 → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : IntervalIntegrable (fun (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 ρ) MeasureTheory.volume 0 top

The recursive child-sum integrability contained in allBranchesAnalytic.

theorem BKAR.Forest.integral_allBranchesBoundaryExpansion_child_eq_integral_standard_add_integral_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 → ℝ) → ℝ) (hstd : IntervalIntegrable (fun (t : ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t])))) MeasureTheory.volume 0 top) (hrec : IntervalIntegrable (fun (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 ρ) MeasureTheory.volume 0 top) : ∫ (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])))) + ∫ (t : ℝ) in 0..top, ∑ 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 ρ

Linearity bridge for one nonterminal child of the exact-depth boundary tree.

The theorem is intentionally local: it separates the boundary subtree into the child's first ordered sector and the recursive exact-depth grandchildren once those two functions are known to be interval-integrable.

theorem BKAR.Forest.childIntegral_eq_prefixedSimplex_add_integralSum {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 → ℝ) → ℝ) (hstd : IntervalIntegrable (fun (t : ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ [t])))) MeasureTheory.volume 0 top) (hrec : IntervalIntegrable (fun (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 ρ) MeasureTheory.volume 0 top) : ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ = (orderedSimplexIntegralAux top [↑e] fun (ts : List ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ ts)))) + ∫ (t : ℝ) in 0..top, ∑ 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 ρ

Prefixed ordered-simplex form of the nonterminal child split.

theorem BKAR.Forest.childIntegral_eq_prefixedSimplex_add_integralSum_of_analytic {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 → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : ∫ (t : ℝ) in 0..top, allBranchesBoundaryExpansion choices (choices F e).forest.activeEdges.card (choices F e).forest (pref ++ [↑e]) (prefixTs ++ [t]) t ρ = (orderedSimplexIntegralAux top [↑e] fun (ts : List ℝ) => mixedPartialList (pref ++ [↑e]).reverse ρ ((choices F e).forest.standardInterp ((choices F e).forest.paramsOfOrder (pref ++ [↑e]) (prefixTs ++ ts)))) + ∫ (t : ℝ) in 0..top, ∑ 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 ρ

Nonterminal child split with the linearity hypotheses read from allBranchesAnalytic.

theorem BKAR.Forest.childIntegralSum_eq_boundarySum_add_childIntegral_of_analytic {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) (hnodup : pref.Nodup) (hanalytic : allBranchesAnalytic choices F.activeEdges.card F pref prefixTs top ρ) : ∑ 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 ρ = ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ + ∑ e ∈ F.activeEdges.attach, ∫ (t : ℝ) in 0..top, ∑ 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 ρ

Arbitrary-node nonterminal regrouping step. After summing over all active children, the first child sectors regroup by support and canonical order, and the only remaining term is the exact recursive child-boundary sum.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_boundarySum_add_childIntegral {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 ρ + (∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, localBoundarySupportOrderContribution choices (empty V) [] [] 1 I order ρ + ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, ∑ 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 specialization of the arbitrary-node nonterminal regrouping step.

theorem BKAR.Forest.integral_boundaryExpansion_empty_child_eq_orderedContribution_add_integral_sum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (e : ↥(empty V).activeEdges) (ρ : (Edge V → ℝ) → ℝ) (hstd : IntervalIntegrable (fun (t : ℝ) => mixedPartialList [↑e].reverse ρ ((choices (empty V) e).forest.standardInterp ((choices (empty V) e).forest.paramsOfOrder [↑e] [t]))) MeasureTheory.volume 0 1) (hrec : IntervalIntegrable (fun (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 ρ) MeasureTheory.volume 0 1) : ∫ (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] ρ + ∫ (t : ℝ) in 0..1, ∑ 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 ρ

Empty-start form of the nonterminal child split: the first child sector is the one-edge ordered contribution of the child forest.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_orderedContributionSum_add_childIntegralSum {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hstd : ∀ (e : ↥(empty V).activeEdges), IntervalIntegrable (fun (t : ℝ) => mixedPartialList [↑e].reverse ρ ((choices (empty V) e).forest.standardInterp ((choices (empty V) e).forest.paramsOfOrder [↑e] [t]))) MeasureTheory.volume 0 1) (hrec : ∀ (e : ↥(empty V).activeEdges), IntervalIntegrable (fun (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 ρ) MeasureTheory.volume 0 1) : ρ oneConfig = (empty V).orderedSectorSum ρ + ∑ e ∈ (empty V).activeEdges.attach, ((choices (empty V) e).forest.orderedContribution [↑e] ρ + ∫ (t : ℝ) in 0..1, ∑ 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 first-layer nonterminal regrouping bridge. Each first active edge now contributes its one-edge ordered sector plus the exact recursive boundary subtrees below the child.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_orderedContributionSum_add_childIntegral {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hanalytic : allBranchesAnalytic choices (empty V).activeEdges.card (empty V) [] [] 1 ρ) (hstd : ∀ (e : ↥(empty V).activeEdges), IntervalIntegrable (fun (t : ℝ) => mixedPartialList [↑e].reverse ρ ((choices (empty V) e).forest.standardInterp ((choices (empty V) e).forest.paramsOfOrder [↑e] [t]))) MeasureTheory.volume 0 1) (hrec : ∀ (e : ↥(empty V).activeEdges), IntervalIntegrable (fun (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 ρ) MeasureTheory.volume 0 1) : ρ oneConfig = (empty V).orderedSectorSum ρ + (∑ e ∈ (empty V).activeEdges.attach, (choices (empty V) e).forest.orderedContribution [↑e] ρ + ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, ∑ 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 ρ)

Separated finite-sum form of the root nonterminal bridge: exposed one-edge sectors and recursive child sums are now two distinct finite sums.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_orderedContributionSum_add_childIntegral_of_analytic {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, (choices (empty V) e).forest.orderedContribution [↑e] ρ + ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, ∑ 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 nonterminal regrouping with the first sectors split from the recursive child sums, using only the strengthened all-branches analytic hypothesis.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_sum_firstContribution_add_childIntegral {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 ρ + (∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, firstBoundarySupportOrderContribution choices I order ρ + ∑ e ∈ (empty V).activeEdges.attach, ∫ (t : ℝ) in 0..1, ∑ 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 nonterminal regrouping with exposed one-edge sectors already fibered by support and canonical order. The remaining summand is the exact recursive child-boundary contribution.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_sum_firstContribution_add_recursiveRemainder {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 ρ + (∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, firstBoundarySupportOrderContribution choices I order ρ + firstRecursiveBoundaryRemainder choices ρ)

Root nonterminal regrouping with the recursive contribution packaged as the first recursive boundary remainder.

theorem BKAR.Forest.oneConfig_eq_initialSectorSum_add_sum_firstContribution_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 ρ + ∑ I : ForestIndex V, ∑ order ∈ edgeSetOrders I.edges, firstBoundarySupportOrderContribution choices I order ρ

Terminal-child base case of the regrouped all-branches identity.