Folding sectors into cube contributions

Sums the closed ordered cube-sector contributions over all enumerations of a support and identifies the result with the ordinary cube contribution of the canonical grown forest, which depends only on the underlying edge set and not on the choice system. This is the final fold from per-order sectors to the one-cube-integral-per-forest form of the BKAR forest interpolation formula (see BKAR.Formula).

theorem BKAR.Forest.orderedCubeSectorContribution_eq_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) {order : List (Edge V)} (hForder : order ∈ F.edgeOrders) (hGorder : order ∈ G.edgeOrders) (ρ : (Edge V → ℝ) → ℝ) : F.orderedCubeSectorContribution order ρ = G.orderedCubeSectorContribution order ρ

Closed ordered cube-sector contributions are invariant under replacing a Forest representative by another Forest representative with the same underlying edge set.

theorem BKAR.Forest.sum_edgeOrders_orderedCubeSectorContribution_eq_cubeContribution {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : ∑ order ∈ F.edgeOrders, F.orderedCubeSectorContribution order ρ = F.cubeContribution ρ

The existing cube-partition theorem, folded in the direction needed by support-indexed ordered assembly.

theorem BKAR.Forest.cubeContribution_eq_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : F.cubeContribution ρ = G.cubeContribution ρ

The unordered cube contribution depends only on the edge set, not on the path data stored in the Forest representative.

theorem BKAR.Forest.sum_edgeSetOrders_orderedCubeSectorContribution_eq_cubeContribution_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) (hedges : F.edges = I.edges) : ∑ order ∈ edgeSetOrders I.edges, F.orderedCubeSectorContribution order ρ = F.cubeContribution ρ

Transport the ordered-sector fold from a forest's own edgeOrders to the canonical order set of any support index with the same edge set.

theorem BKAR.Forest.sectorContributionSum_eq_canonicalContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : ∑ order ∈ edgeSetOrders I.edges, (canonicalGrownForestForSupport choices I).orderedCubeSectorContribution order ρ = (canonicalGrownForestForSupport choices I).cubeContribution ρ

The canonical grown forest over a support folds its support-indexed ordered cube sectors back to its unordered cube contribution.

theorem BKAR.Forest.sum_orderedSectorContribution_eq_canonicalContribution {V : Type u_1} [Fintype V] [DecidableEq V] (choices : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : ∑ order ∈ (edgeSetOrders I.edges).attach, (grownForestForSupportOrder choices I order).orderedCubeSectorContribution (↑order) ρ = (canonicalGrownForestForSupport choices I).cubeContribution ρ

After sectorwise canonicalization, the whole support/order sum over grown Forest representatives folds to the ordinary cube contribution of the canonical grown representative.

theorem BKAR.Forest.canonicalGrownForestForSupport_cubeContribution_eq_of_choices {V : Type u_1} [Fintype V] [DecidableEq V] (choices₁ choices₂ : ActiveExtensionChoice V) (I : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : (canonicalGrownForestForSupport choices₁ I).cubeContribution ρ = (canonicalGrownForestForSupport choices₂ I).cubeContribution ρ

For a fixed support, the canonical grown cube contribution is independent of the auxiliary active-extension choice system.