The fiber bridge: order sums and low-rank cases

Sums the fiber bridge over all orders of a fixed support: the summed root fiber contribution equals the ordered contribution of the grown forest when followOrder succeeds and vanishes otherwise, with the empty, singleton, and pair supports worked out explicitly.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_nil_eq_zero_of_edges_ne_empty {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (hI : I.edges ≠ ∅) : rootBoundarySupportOrderContribution choices ρ I [] = 0

The empty order contributes only to the empty support.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_nil {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, rootBoundarySupportOrderContribution choices ρ I [] = (empty V).orderedContribution [] ρ

The empty support sector sums to the ordered contribution of the empty forest.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_chosenGrowth {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices (empty V) order G) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, rootBoundarySupportOrderContribution choices ρ I order = G.orderedContribution order ρ

For any chosen root growth path, summing the fixed order over all support indices leaves exactly the ordered contribution of the path's terminal forest.

theorem BKAR.Forest.sum_rootContribution_eq_orderedContribution_of_followOrder_eq_some {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {G : Forest V} {order : List (Edge V)} (hG : followOrderOption choices (empty V) order = some G) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, rootBoundarySupportOrderContribution choices ρ I order = G.orderedContribution order ρ

Deterministic finite-order form of the chosen-growth bridge: if following an order through the selected active extensions reaches G, the support-summed root fiber is exactly the ordered sector of G with that order.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_eq_zero_of_followOrder_eq_none {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {order : List (Edge V)} (horder : followOrderOption choices (empty V) order = none) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, rootBoundarySupportOrderContribution choices ρ I order = 0

Complementary deterministic finite-order form: if the selected extensions cannot follow the requested root order, then that fixed order has zero total root fiber after summing over supports.

theorem BKAR.Forest.exists_rootContribution_eq_orderedContribution_of_mem_edgeSetOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {I : ForestIndex V} {order : List (Edge V)} (horder : order ∈ edgeSetOrders I.edges) (ρ : (Edge V → ℝ) → ℝ) : ∃ (G : Forest V), G.support = I ∧ rootBoundarySupportOrderContribution choices ρ I order = G.orderedContribution order ρ

For a canonical support order, the root fiber is an ordered sector of the Forest representative grown by following that order. This isolates the only remaining choice dependence in the sector integrand: the grown Forest representative data.

theorem BKAR.Forest.exists_sum_rootContribution_eq_orderedContribution_of_mem_edgeSetOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {I : ForestIndex V} {order : List (Edge V)} (horder : order ∈ edgeSetOrders I.edges) (ρ : (Edge V → ℝ) → ℝ) : ∃ (G : Forest V), G.support = I ∧ ∑ J : ForestIndex V, rootBoundarySupportOrderContribution choices ρ J order = G.orderedContribution order ρ

After summing over all support indices, a canonical order leaves the ordered sector of the Forest representative grown by following that order.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_emptySupport {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) : ∑ order ∈ edgeSetOrders (empty V).support.edges, rootBoundarySupportOrderContribution choices ρ (empty V).support order = (empty V).orderedContribution [] ρ

The empty support inner sum is the empty forest ordered contribution.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_singleton_eq_zero_of_edges_ne_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (a : Edge V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (hI : I.edges ≠ {a}) : rootBoundarySupportOrderContribution choices ρ I [a] = 0

A singleton order contributes only over the matching singleton support.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (a : Edge V) (ρ : (Edge V → ℝ) → ℝ) : ∑ I : ForestIndex V, rootBoundarySupportOrderContribution choices ρ I [a] = (choices (empty V) (emptyActiveEdge a)).forest.orderedContribution [a] ρ

Summing a fixed singleton order over all support indices leaves exactly the matching one-edge ordered contribution.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_singletonSupport {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (a : Edge V) (ρ : (Edge V → ℝ) → ℝ) : ∑ order ∈ edgeSetOrders (ForestIndex.singleton a).edges, rootBoundarySupportOrderContribution choices ρ (ForestIndex.singleton a) order = (choices (empty V) (emptyActiveEdge a)).forest.orderedContribution [a] ρ

The singleton support inner sum has already collapsed to the unique singleton order and is the matching one-edge ordered contribution.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_pair_eq_orderedContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (a b : Edge V) (ρ : (Edge V → ℝ) → ℝ) (hb : b ∈ (choices (empty V) (emptyActiveEdge a)).forest.activeEdges) : rootBoundarySupportOrderContribution choices ρ (choices (choices (empty V) (emptyActiveEdge a)).forest ⟨b, hb⟩).forest.support [a, b] = (choices (choices (empty V) (emptyActiveEdge a)).forest ⟨b, hb⟩).forest.orderedContribution [a, b] ρ

The length-two root fiber follows the chosen first edge, then the chosen second edge, and is exactly the corresponding ordered contribution.

theorem BKAR.Forest.sum_rootBoundarySupportOrderContribution_pair {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (a b : Edge V) (ρ : (Edge V → ℝ) → ℝ) (hb : b ∈ (choices (empty V) (emptyActiveEdge a)).forest.activeEdges) : ∑ I : ForestIndex V, rootBoundarySupportOrderContribution choices ρ I [a, b] = (choices (choices (empty V) (emptyActiveEdge a)).forest ⟨b, hb⟩).forest.orderedContribution [a, b] ρ

After summing over all support indices, a fixed active two-edge order leaves only the support grown by the corresponding two chosen extensions.