The BKAR forest interpolation formula

Main results. For a finite vertex set V and ρ : (Edge V → ℝ) → ℝ smooth on the edge-coupling space (BKARContDiff), the flagship theorem bkar_formula_forestIndex_cube_contributions states

ρ oneConfig = ∑ I : ForestIndex V, I.cubeContribution ρ,

that is: the value of ρ at the all-ones coupling is the sum, over all acyclic edge sets F on V, of ∫_{[0,1]^{E(F)}} ∂_{E(F)} ρ (x^F(u)) du, where ∂_{E(F)} is the mixed partial derivative in the edge variables of F and the interpolation point x^F(u) assigns to each edge the minimum of u along the unique forest path between its endpoints (0 across components); the empty forest contributes ρ zeroConfig. Variants: support/order sector forms, grown-forest sector forms with proved choice-independence, and the form with the empty sector split off (bkar_formula_nonempty).

The formalization assumes C^∞ smoothness where the classical statement needs only C^{|V|-1} — a deliberate strengthening of the hypothesis.

References

• D. Brydges, T. Kennedy, Mayer expansions and the Hamilton–Jacobi equation, J. Statist. Phys. 48 (1987) 19–49.
• A. Abdesselam, V. Rivasseau, Trees, forests and jungles: a botanical garden for cluster expansions, in Constructive Physics (Palaiseau 1994), Lecture Notes in Physics 446, Springer, 1995. arXiv:hep-th/9409094.

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

The final closed-sector right-hand side, still written using the Forest representative grown by the chosen active-extension system in each support/order sector.

Equations

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

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

Canonical grown-representative cube contribution sum: one ordinary cube integral for the canonical Forest representative over each support.

Equations

• BKAR.canonicalGrownForestCubeContributionSum choices ρ = ∑ I : BKAR.ForestIndex V, (BKAR.Forest.canonicalGrownForestForSupport choices I).cubeContribution ρ

theorem BKAR.grownForestCubeSectorSum_choice_independent {V : Type u_1} [Fintype V] [DecidableEq V] (choices₁ choices₂ : Forest.ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : grownForestCubeSectorSum choices₁ ρ = grownForestCubeSectorSum choices₂ ρ

The total grown-representative closed-sector sum is independent of the auxiliary active-extension choices. This is the honest global choice-independence fact available from the proved BKAR identity without assuming path-data proof-irrelevance for individual same-edge Forest representatives.

theorem BKAR.canonicalGrownForestCubeContributionSum_choice_independent {V : Type u_1} [Fintype V] [DecidableEq V] (choices₁ choices₂ : Forest.ActiveExtensionChoice V) (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : canonicalGrownForestCubeContributionSum choices₁ ρ = canonicalGrownForestCubeContributionSum choices₂ ρ

The folded canonical grown-representative cube contribution sum is also independent of the auxiliary active-extension choices.

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

For a fixed choice system and support, the canonical grown representative's usual cube contribution is exactly the sum over all ordered sectors of that same representative.

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

Public scalar BKAR theorem. The statement is uniform in the auxiliary forest-extension choices made by the ordered assembly.

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

Public canonical-representative sector form. This removes the existential Forest-representative bridge from each sector by choosing the forest grown by the canonical order follower.

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

Public canonical-representative closed-sector form. The Forest representative choice remaining in the sector integrand is removed by the canonicalized forms below (see bkar_formula_forestIndex_cube_contributions).

theorem BKAR.bkar_formula_grown_forest_cube_sector_sum {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) : ρ oneConfig = grownForestCubeSectorSum choices ρ

Public compact grown-representative closed-sector form. The accompanying theorem grownForestCubeSectorSum_choice_independent proves that the right-hand side is independent of the auxiliary active-extension choices.

theorem BKAR.bkar_formula_canonical_grown_cube_contributions {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) : ρ oneConfig = canonicalGrownForestCubeContributionSum choices ρ

Public folded canonical-representative cube-contribution BKAR form. This is the support-indexed sum, modulo the still-explicit choice of Forest representatives used to realize each abstract forest support.

theorem BKAR.bkar_formula_forestIndex_cube_contributions {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) : ρ oneConfig = ∑ I : ForestIndex V, I.cubeContribution ρ

Main scalar BKAR theorem — the forest interpolation formula: the value at the all-ones configuration is the support-indexed sum of ordinary cube contributions over abstract forest edge sets.

theorem BKAR.bkar_formula_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : BKARContDiff ρ) (choices : Forest.ActiveExtensionChoice V) : ρ oneConfig = ρ zeroConfig + ∑ I : ForestIndex V with I.edges ≠ ∅, ∑ order ∈ Forest.edgeSetOrders I.edges, Forest.boundarySupportOrderTreeFiber choices (Forest.empty V) [] [] 1 I order ρ

Public scalar BKAR theorem with the empty forest sector split off explicitly as ρ zeroConfig.