The fiber bridge: core identities

Identifies the boundary support/order tree fibers with intrinsic ordered contributions: a fiber unfolds into an integral over its child fibers, vanishes unless the order enumerates the support and follows active extensions, and, when followOrder succeeds, the root fiber equals the recursive ordered contribution of the grown forest.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_localBoundary_of_order_length_eq_succ {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 → ℝ) → ℝ) (hlen : order.length = pref.length + 1) : boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = localBoundarySupportOrderContribution choices F pref prefixTs top I order ρ

At a node whose requested global order is exactly one edge longer than the current prefix, the recursive fiber has no child remainder: every child has already consumed the whole requested order.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_order_toFinset_ne_edges {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → pref.toFinset = F.edges → order.toFinset ≠ I.edges → boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = 0

A support/order fiber can contribute only when the requested order has exactly the requested support edge set.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_not_exists_pref_append {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → (¬∃ (tail : List (Edge V)), pref ++ tail = order) → boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = 0

A support/order fiber can only contribute along branches whose accumulated prefix is still a prefix of the requested global order.

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

Root fibers vanish unless the requested order has the requested support.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_order_not_mem_edgeSetOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (n : ℕ) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (order : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : F.activeEdges.card ≤ n → pref.toFinset = F.edges → pref.Nodup → order ∉ edgeSetOrders I.edges → boundarySupportOrderTreeFiber choices F pref prefixTs top I order ρ = 0

A support/order fiber can contribute only for canonical orders of the requested support.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_eq_zero_of_order_not_mem_edgeSetOrders {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (I : ForestIndex V) (order : List (Edge V)) (horder : order ∉ edgeSetOrders I.edges) : rootBoundarySupportOrderContribution choices ρ I order = 0

Root fibers vanish off the canonical order set of the requested support.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_integral_child_of_tail_ne_nil {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (e₀ : Edge V) (tail : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (he₀ : e₀ ∈ F.activeEdges) (htail : tail ≠ []) : boundarySupportOrderTreeFiber choices F pref prefixTs top I (pref ++ e₀ :: tail) ρ = ∫ (t : ℝ) in 0..top, boundarySupportOrderTreeFiber choices (choices F ⟨e₀, he₀⟩).forest (pref ++ [e₀]) (prefixTs ++ [t]) t I (pref ++ e₀ :: tail) ρ

If the requested order continues with a nonempty tail after the next edge, then the tree fiber follows exactly the child indexed by that next edge.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_next_not_mem_activeEdges {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (e₀ : Edge V) (tail : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) (he₀ : e₀ ∉ F.activeEdges) : boundarySupportOrderTreeFiber choices F pref prefixTs top I (pref ++ e₀ :: tail) ρ = 0

If the next requested edge is not active, the whole fiber is zero.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_eq_zero_of_followOrder_eq_none {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (order : List (Edge V)) (F : Forest V) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : followOrderOption choices F order = none → boundarySupportOrderTreeFiber choices F pref prefixTs top I (pref ++ order) ρ = 0

If a requested suffix cannot be followed through the selected active extensions, the corresponding fixed support/order fiber is zero.

theorem BKAR.Forest.boundarySupportOrderTreeFiber_chosenGrowth_eq_orderedSimplexIntegralAux {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) {F G : Forest V} {order : List (Edge V)} (path : ChosenGrowth choices F order G) (pref : List (Edge V)) (prefixTs : List ℝ) (top : ℝ) (ρ : (Edge V → ℝ) → ℝ) : order ≠ [] → boundarySupportOrderTreeFiber choices F pref prefixTs top G.support (pref ++ order) ρ = orderedSimplexIntegralAux top order fun (ts : List ℝ) => mixedPartialList (pref ++ order).reverse ρ (G.standardInterp (G.paramsOfOrder (pref ++ order) (prefixTs ++ ts)))

Along a chosen growth path, the fixed support/order tree fiber is exactly the corresponding ordered simplex integral. This is the arbitrary finite-order version of the explicit one- and two-edge bridge lemmas below.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_chosenGrowth_eq_orderedContribution {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 → ℝ) → ℝ) (horder : order ≠ []) : rootBoundarySupportOrderContribution choices ρ G.support order = G.orderedContribution order ρ

Root specialization of boundarySupportOrderTreeFiber_chosenGrowth_eq_orderedSimplexIntegralAux.

theorem BKAR.Forest.rootBoundarySupportOrderContribution_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 → ℝ) → ℝ) (horder : order ≠ []) : rootBoundarySupportOrderContribution choices ρ G.support order = G.orderedContribution order ρ

Root fiber bridge stated in terms of the deterministic order follower.

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

A failed deterministic root order has zero contribution in every support fiber.