BKAR forest formula — Solution

This file proves the mirror statement below from the repository flagship BKAR.bkar_formula_forestIndex_cube_contributions, through the bridge lemmas of Audit/ForestFormula/SolutionBasic.lean.

The mirror originates in Audit/ForestFormula/Challenge.lean in scottnarmstrong/bkarforestformula, commit a07f44a534240fe6339558951dd78a19e4ef7c51. That upstream statement can be inspected at the pinned revision; its placeholder proof is omitted from Lean Pool. The local statement vocabulary lives in SolutionBasic.lean, and the bridge lemmas and proof below establish the formula for that vocabulary. This port does not maintain an automated comparison with the upstream challenge.

#print axioms gives exactly [propext, Classical.choice, Quot.sound].

theorem BKARMirror.bkar_formula_forestIndex_cube_contributions {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : ContDiffHyp ρ) : (ρ fun (x : Edge V) => 1) = ∑ J : ForestIndex V, cubeContribution J ρ

Challenge statement (Mathlib-only): the BKAR forest interpolation formula.