BKAR forest formula — Challenge → repository bridges

Shared statement vocabulary adapted from Audit/ForestFormula/Challenge.lean in scottnarmstrong/bkarforestformula at commit a07f44a534240fe6339558951dd78a19e4ef7c51, together with the bridge lemmas connecting the Mathlib-based mirror to the repository flagship BKAR.bkar_formula_forestIndex_cube_contributions.

Solution.lean proves the formula using this local vocabulary. The upstream challenge placeholder is omitted from Lean Pool; no automated comparison with that upstream statement is maintained here.

Bridge outline

• Q1 acyclic_bridge — Mathlib graph acyclicity SimpleGraph.IsAcyclic on edgeGraph is equivalent to the repository certificate IsAcyclicEdgeSet. Forward reuses AcyclicEdgeSetData.edgeSetGraph_isAcyclic; the reverse builds an AcyclicEdgeSetData from graph acyclicity (the constructor extracted from isAcyclicEdgeSet_insert_of_not_inSameComponent).
• Q2 standardInterp_bridge — the threshold / sSup interpolation point agrees with the repository path-minimum Forest.standardInterp, via le_standardInterp_iff_thresholdConnected and a graph-reachability ↔ threshold-connectivity comparison, closed by csSup antisymmetry (with the sSup ∅ = 0 boundary handled by Real.sSup_nonneg).
• Q3/Q4 mixedPartial_bridge, cubeContribution_bridge — the verbatim mixed partial and the cube integral agree; choice-independence is discharged through cubeContribution_eq_canonicalGrownForestForSupport and cubeContribution_eq_of_edges_eq.
• sum_bridge transports the mirror sum to the repository sum along indexEquiv.

Mirror vocabulary adapted from the pinned upstream challenge

@[reducible, inline]

abbrev BKARMirror.Edge (V : Type u_2) : Type u_2

Off-diagonal unordered pairs = edges of the complete graph on V.

Equations

• BKARMirror.Edge V = { e : Sym2 V // ¬e.IsDiag }

@[instance_reducible]

noncomputable instance BKARMirror.instFintypeEdge {V : Type u_1} [Fintype V] : Fintype (Edge V)

Equations

• BKARMirror.instFintypeEdge = Fintype.ofFinite (BKARMirror.Edge V)

noncomputable def BKARMirror.Edge.left {V : Type u_1} (e : Edge V) : V

A fixed orientation of an edge (Mathlib Sym2.out).

Equations

• e.left = (Quot.out ↑e).1

noncomputable def BKARMirror.Edge.right {V : Type u_1} (e : Edge V) : V

The second endpoint in the chosen representative of an unordered edge.

Equations

• e.right = (Quot.out ↑e).2

def BKARMirror.edgeGraph {V : Type u_1} (S : Finset (Edge V)) : SimpleGraph V

The simple graph carried by a finite edge set.

Equations

• BKARMirror.edgeGraph S = SimpleGraph.fromEdgeSet {x : Sym2 V | ∃ e ∈ S, ↑e = x}

structure BKARMirror.ForestIndex (V : Type u_2) [Fintype V] [DecidableEq V] : Type u_2

Q1: the forest index, indexed by an edge set whose carried graph is acyclic.

• edges : Finset (Edge V)

  The finite edge set indexing a term of the forest formula.

• acyclic : (edgeGraph self.edges).IsAcyclic

@[instance_reducible]

noncomputable instance BKARMirror.ForestIndex.instFintype {V : Type u_1} [Fintype V] [DecidableEq V] : Fintype (ForestIndex V)

ForestIndex V is a Fintype (mirrors the repo's Classical-decidable route).

Equations

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

def BKARMirror.paramValue {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (u : ↥J.edges → ℝ) (e : Edge V) : ℝ

Look up an edge parameter, defaulting to 1 off the forest.

Equations

• BKARMirror.paramValue J u e = if h : e ∈ J.edges then u ⟨e, h⟩ else 1

def BKARMirror.thresholdGraph {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (u : ↥J.edges → ℝ) (s : ℝ) : SimpleGraph V

The threshold subgraph: edges of J whose parameter is ≥ s.

Equations

• BKARMirror.thresholdGraph J u s = SimpleGraph.fromEdgeSet {x : Sym2 V | ∃ e ∈ J.edges, ↑e = x ∧ s ≤ BKARMirror.paramValue J u e}

noncomputable def BKARMirror.standardInterp {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (u : ↥J.edges → ℝ) : Edge V → ℝ

Q2: the BKAR interpolation point x^F(u)_e, as the largest threshold s ∈ [0,1] at which the endpoints of e remain connected using only couplings ≥ s (the bottleneck / max-min connectivity value; sSup ∅ = 0 handles disconnection).

Equations

• BKARMirror.standardInterp J u e = sSup {s : ℝ | 0 ≤ s ∧ s ≤ 1 ∧ (BKARMirror.thresholdGraph J u s).Reachable e.left e.right}

def BKARMirror.updateCoord {V : Type u_1} [DecidableEq V] (x : Edge V → ℝ) (e : Edge V) (t : ℝ) : Edge V → ℝ

Replace one edge coordinate (verbatim).

Equations

• BKARMirror.updateCoord x e t = Function.update x e t

noncomputable def BKARMirror.partialDeriv {V : Type u_1} [DecidableEq V] (e : Edge V) (ρ : (Edge V → ℝ) → ℝ) (x : Edge V → ℝ) : ℝ

Partial derivative along one edge coordinate (verbatim).

Equations

• BKARMirror.partialDeriv e ρ x = deriv (fun (t : ℝ) => ρ (BKARMirror.updateCoord x e t)) (x e)

def BKARMirror.mixedPartialList {V : Type u_1} [DecidableEq V] : List (Edge V) → ((Edge V → ℝ) → ℝ) → (Edge V → ℝ) → ℝ

Q3: iterated mixed partial along a list of edges (verbatim).

Equations

• BKARMirror.mixedPartialList [] x✝ = x✝
• BKARMirror.mixedPartialList (e :: es) x✝ = BKARMirror.partialDeriv e (BKARMirror.mixedPartialList es x✝)

noncomputable def BKARMirror.mixedPartial {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : (Edge V → ℝ) → ℝ

The forest-indexed mixed partial (verbatim: over Finset.toList).

Equations

• BKARMirror.mixedPartial J ρ = BKARMirror.mixedPartialList J.edges.toList ρ

def BKARMirror.unitCube {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) : Set (↥J.edges → ℝ)

Q4: the unit cube [0,1]^{E(J)}.

Equations

• BKARMirror.unitCube J = Set.univ.pi fun (x : ↥J.edges) => Set.Icc 0 1

noncomputable def BKARMirror.cubeContribution {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) : ℝ

Q4: the ordinary BKAR cube contribution of a forest index (direct, choice-free).

Equations

• BKARMirror.cubeContribution J ρ = ∫ (u : ↥J.edges → ℝ) in BKARMirror.unitCube J, BKARMirror.mixedPartial J ρ (BKARMirror.standardInterp J u)

def BKARMirror.ContDiffHyp {V : Type u_1} [Fintype V] (ρ : (Edge V → ℝ) → ℝ) : Prop

BKAR smoothness hypothesis (mirror of BKARContDiff).

Equations

• BKARMirror.ContDiffHyp ρ = ContDiff ℝ (↑⊤) ρ

Q1 bridge: mirror graph acyclicity ↔ repository certificate

theorem BKARMirror.edgeGraph_eq {V : Type u_1} (S : Finset (Edge V)) : edgeGraph S = BKAR.EdgePath.edgeSetGraph S

The mirror graph on an edge set is definitionally equal to the repository's EdgePath.edgeSetGraph.

theorem BKARMirror.acyclic_bridge {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset (Edge V)) : (edgeGraph S).IsAcyclic ↔ BKAR.IsAcyclicEdgeSet S

Q1 bridge. Mirror graph acyclicity ↔ repository acyclicity certificate.

def BKARMirror.indexEquiv {V : Type u_1} [Fintype V] [DecidableEq V] : ForestIndex V ≃ BKAR.ForestIndex V

The forest-index types are equivalent (from the acyclicity iff).

Equations

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

Q2 bridge: threshold sSup interpolation ↔ repository path-minimum

theorem BKARMirror.edgeSetGraph_reachable_iff_exists_isSimplePath {V : Type u_1} (S : Finset (Edge V)) (i j : V) : (BKAR.EdgePath.edgeSetGraph S).Reachable i j ↔ ∃ (γ : List (BKAR.Edge V)), BKAR.EdgePath.IsSimplePath S γ i j

Reachability in edgeSetGraph S is the existence of a simple edge path.

theorem BKARMirror.thresholdConnected_iff_exists_isSimplePath {V : Type u_1} [Fintype V] [DecidableEq V] (G : BKAR.Forest V) (u : G.EdgeParam → ℝ) (s : ℝ) (i j : V) : G.thresholdConnected u s i j ↔ ∃ (γ : List (BKAR.Edge V)), BKAR.EdgePath.IsSimplePath (G.thresholdEdges u s) γ i j

Threshold connectivity is the existence of a simple path in the threshold edge set.

theorem BKARMirror.thresholdGraph_eq {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (data : BKAR.AcyclicEdgeSetData J.edges) (u : ↥J.edges → ℝ) (s : ℝ) : thresholdGraph J u s = BKAR.EdgePath.edgeSetGraph (data.toForest.thresholdEdges u s)

The mirror threshold graph coincides with the repository threshold-edge graph.

theorem BKARMirror.reachable_thresholdGraph_iff {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (data : BKAR.AcyclicEdgeSetData J.edges) (u : ↥J.edges → ℝ) (s : ℝ) (e : Edge V) : (thresholdGraph J u s).Reachable e.left e.right ↔ data.toForest.thresholdConnected u s e.left e.right

Threshold-graph reachability matches repository threshold connectivity.

theorem BKARMirror.standardInterp_bridge {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (data : BKAR.AcyclicEdgeSetData J.edges) (u : ↥J.edges → ℝ) (hu : ∀ (e : ↥J.edges), 0 ≤ u e ∧ u e ≤ 1) : standardInterp J u = data.toForest.standardInterp u

Q2 bridge. The mirror threshold / sSup interpolation point agrees with the repository path-minimum Forest.standardInterp, on the unit cube.

Q3/Q4 bridges and choice removal

theorem BKARMirror.mixedPartialList_bridge {V : Type u_1} [DecidableEq V] (l : List (Edge V)) (ρ : (Edge V → ℝ) → ℝ) : mixedPartialList l ρ = BKAR.mixedPartialList l ρ

Q3: the mirror iterated mixed partial coincides with the repository one.

theorem BKARMirror.mixedPartial_bridge {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (data : BKAR.AcyclicEdgeSetData J.edges) (ρ : (Edge V → ℝ) → ℝ) : mixedPartial J ρ = data.toForest.mixedPartial ρ

The forest mixed partial agrees with the mirror mixed partial.

theorem BKARMirror.cubeContribution_bridge {V : Type u_1} [Fintype V] [DecidableEq V] (J : ForestIndex V) (ρ : (Edge V → ℝ) → ℝ) (hρ : ContDiffHyp ρ) : cubeContribution J ρ = (indexEquiv J).cubeContribution ρ

Q2 + Q3 + Q4 bridge. The mirror direct cube contribution equals the repository choice-routed ForestIndex.cubeContribution.

Configuration and sum bridges

theorem BKARMirror.oneConfig_bridge {V : Type u_1} : (fun (x : Edge V) => 1) = BKAR.oneConfig

The all-ones config agrees (definitional).

theorem BKARMirror.sum_bridge {V : Type u_1} [Fintype V] [DecidableEq V] (ρ : (Edge V → ℝ) → ℝ) (hρ : ContDiffHyp ρ) : ∑ J : ForestIndex V, cubeContribution J ρ = ∑ I : BKAR.ForestIndex V, I.cubeContribution ρ

Sum bridge. Transport the mirror sum to the repository sum via indexEquiv.