Forests on a finite vertex set

Combinatorial foundation for the BKAR forest interpolation formula (see BKAR.Formula). Defines Edge V, the off-diagonal unordered pairs of a finite vertex type V (edges of the complete graph on V); simple paths along an edge set; the acyclicity predicate IsAcyclicEdgeSet; the acyclicity API AcyclicEdgeSetData (component relation, canonical simple paths, path uniqueness); the index type ForestIndex V of acyclic edge sets, over which the final forest sum ranges; and the working type Forest V, an acyclic edge set packaged with its path API and the one-edge extension characterization.

@[reducible, inline]

abbrev BKAR.Edge (V : Type u_1) : Type u_1

Edges of the complete graph on V, represented as off-diagonal unordered pairs.

Equations

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

@[instance_reducible]

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

Equations

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

def BKAR.Edge.mk {V : Type u_1} (i j : V) (hij : i ≠ j) : Edge V

The edge with endpoints i and j.

Equations

• BKAR.Edge.mk i j hij = ⟨s(i, j), ⋯⟩

@[simp]

theorem BKAR.Edge.mk_val {V : Type u_1} (i j : V) (hij : i ≠ j) : ↑(mk i j hij) = s(i, j)

theorem BKAR.Edge.not_isDiag {V : Type u_1} (e : Edge V) : ¬(↑e).IsDiag

def BKAR.Edge.Between {V : Type u_1} (e : Edge V) (i j : V) : Prop

e.Between i j says that e is the unordered pair {i, j}.

Equations

• e.Between i j = (↑e = s(i, j))

theorem BKAR.Edge.mk_between {V : Type u_1} (i j : V) (hij : i ≠ j) : (mk i j hij).Between i j

theorem BKAR.Edge.mk_comm {V : Type u_1} (i j : V) (hij : i ≠ j) : mk i j hij = mk j i ⋯

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

A fixed first endpoint of an unordered edge.

Equations

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

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

A fixed second endpoint of an unordered edge.

Equations

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

theorem BKAR.Edge.mk_left_right_eq {V : Type u_1} (e : Edge V) : s(e.left, e.right) = ↑e

theorem BKAR.Edge.between_left_right {V : Type u_1} (e : Edge V) : e.Between e.left e.right

theorem BKAR.Edge.left_ne_right {V : Type u_1} (e : Edge V) : e.left ≠ e.right

theorem BKAR.Edge.not_between_self {V : Type u_1} (e : Edge V) (i : V) : ¬e.Between i i

theorem BKAR.Edge.Between.symm {V : Type u_1} {e : Edge V} {i j : V} (h : e.Between i j) : e.Between j i

inductive BKAR.EdgePath.IsPath {V : Type u_1} (S : Finset (Edge V)) : List (Edge V) → V → V → Prop

A list of edges forms an oriented walk from i to j inside S.

• nil {V : Type u_1} {S : Finset (Edge V)} (i : V) : IsPath S [] i i
• cons {V : Type u_1} {S : Finset (Edge V)} {i j k : V} {e : Edge V} {γ : List (Edge V)} : e ∈ S → e.Between i j → IsPath S γ j k → IsPath S (e :: γ) i k

def BKAR.EdgePath.IsSimplePath {V : Type u_1} (S : Finset (Edge V)) (γ : List (Edge V)) (i j : V) : Prop

A graph-level simple path: an edge walk with no repeated edges.

Equations

• BKAR.EdgePath.IsSimplePath S γ i j = (BKAR.EdgePath.IsPath S γ i j ∧ γ.Nodup)

theorem BKAR.EdgePath.IsPath.mono {V : Type u_1} {S T : Finset (Edge V)} (hsub : S ⊆ T) {γ : List (Edge V)} {i j : V} : IsPath S γ i j → IsPath T γ i j

theorem BKAR.EdgePath.IsPath.mono_of_forall_mem {V : Type u_1} {S T : Finset (Edge V)} {γ : List (Edge V)} {i j : V} : IsPath S γ i j → (∀ e ∈ γ, e ∈ T) → IsPath T γ i j

theorem BKAR.EdgePath.IsPath.edge_mem {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} : IsPath S γ i j → ∀ e ∈ γ, e ∈ S

theorem BKAR.EdgePath.IsPath.append {V : Type u_1} {S : Finset (Edge V)} {γ₁ γ₂ : List (Edge V)} {i j k : V} : IsPath S γ₁ i j → IsPath S γ₂ j k → IsPath S (γ₁ ++ γ₂) i k

theorem BKAR.EdgePath.IsPath.reverse {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} : IsPath S γ i j → IsPath S γ.reverse j i

theorem BKAR.EdgePath.IsSimplePath.mono {V : Type u_1} {S T : Finset (Edge V)} (hsub : S ⊆ T) {γ : List (Edge V)} {i j : V} (h : IsSimplePath S γ i j) : IsSimplePath T γ i j

theorem BKAR.EdgePath.IsSimplePath.mono_of_forall_mem {V : Type u_1} {S T : Finset (Edge V)} {γ : List (Edge V)} {i j : V} (h : IsSimplePath S γ i j) (hmem : ∀ e ∈ γ, e ∈ T) : IsSimplePath T γ i j

theorem BKAR.EdgePath.IsSimplePath.edge_mem {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} (h : IsSimplePath S γ i j) (e : Edge V) : e ∈ γ → e ∈ S

theorem BKAR.EdgePath.IsSimplePath.reverse {V : Type u_1} {S : Finset (Edge V)} {γ : List (Edge V)} {i j : V} (h : IsSimplePath S γ i j) : IsSimplePath S γ.reverse j i

theorem BKAR.EdgePath.isSimplePath_empty_iff {V : Type u_1} {γ : List (Edge V)} {i j : V} : IsSimplePath ∅ γ i j ↔ γ = [] ∧ i = j

theorem BKAR.EdgePath.isPath_singleton_tail_nil {V : Type u_1} {e₀ : Edge V} {γ : List (Edge V)} {i j : V} : IsSimplePath {e₀} γ i j → γ = [] ∨ γ = [e₀]

theorem BKAR.EdgePath.isSimplePath_singleton_iff {V : Type u_1} {e₀ : Edge V} {γ : List (Edge V)} {i j : V} : IsSimplePath {e₀} γ i j ↔ γ = [] ∧ i = j ∨ γ = [e₀] ∧ e₀.Between i j

structure BKAR.AcyclicEdgeSetData {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset (Edge V)) : Type u_1

Data carried by an acyclic edge set.

The primitive representation is intentionally thin: later files consume the component relation, the canonical simple path, and path uniqueness, so these are the API exposed by the acyclicity certificate.

• inSameComponent : V → V → Prop

  The relation of belonging to the same connected component.

• isSimplePath : List (Edge V) → V → V → Prop

  The predicate that an edge list is a simple path between the given vertices.

• pathIn (i j : V) : self.inSameComponent i j → List (Edge V)

  The canonical simple path between vertices in the same component.

• pathIn_isSimple {i j : V} (h : self.inSameComponent i j) : self.isSimplePath (self.pathIn i j h) i j
• isSimplePath_iff {i j : V} {γ : List (Edge V)} : self.isSimplePath γ i j ↔ EdgePath.IsSimplePath S γ i j
• sameComponent_of_simplePath {i j : V} {γ : List (Edge V)} : self.isSimplePath γ i j → self.inSameComponent i j
• path_unique {i j : V} {γ₁ γ₂ : List (Edge V)} : self.isSimplePath γ₁ i j → self.isSimplePath γ₂ i j → γ₁ = γ₂
• path_edges_mem {i j : V} {γ : List (Edge V)} : self.isSimplePath γ i j → ∀ e ∈ γ, e ∈ S
• edge_isSimplePath {e : Edge V} : e ∈ S → self.isSimplePath [e] e.left e.right

def BKAR.IsAcyclicEdgeSet {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset (Edge V)) : Prop

A custom acyclicity predicate for finite edge sets.

Equations

• BKAR.IsAcyclicEdgeSet S = Nonempty (BKAR.AcyclicEdgeSetData S)

theorem BKAR.IsAcyclicEdgeSet.mono {V : Type u_1} [Fintype V] [DecidableEq V] {S T : Finset (Edge V)} (hS : IsAcyclicEdgeSet S) (hsub : T ⊆ S) : IsAcyclicEdgeSet T

Acyclicity is inherited by finite edge subsets.

theorem BKAR.AcyclicEdgeSetData.inSameComponent_iff_exists_isSimplePath {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {i j : V} : data.inSameComponent i j ↔ ∃ (γ : List (Edge V)), EdgePath.IsSimplePath S γ i j

theorem BKAR.AcyclicEdgeSetData.inSameComponent_refl {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) (i : V) : data.inSameComponent i i

theorem BKAR.AcyclicEdgeSetData.inSameComponent_symm {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {i j : V} (h : data.inSameComponent i j) : data.inSameComponent j i

theorem BKAR.AcyclicEdgeSetData.not_isAcyclicEdgeSet_insert_of_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] {S : Finset (Edge V)} (data : AcyclicEdgeSetData S) {e : Edge V} (heS : e ∉ S) (hcomp : data.inSameComponent e.left e.right) : ¬IsAcyclicEdgeSet (insert e S)

Adding an absent edge whose endpoints are already connected cannot preserve acyclicity: the old component path and the new singleton edge would be two distinct simple paths.

structure BKAR.ForestIndex (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

The finite edge-set index over which the final BKAR forest sum ranges.

• edges : Finset (Edge V)

  The finite acyclic edge set indexing a forest summand.

• acyclic : IsAcyclicEdgeSet self.edges

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• BKAR.ForestIndex.instDecidableEq = Classical.decEq (BKAR.ForestIndex V)

theorem BKAR.ForestIndex.ext {V : Type u_1} [Fintype V] [DecidableEq V] {I J : ForestIndex V} (h : I.edges = J.edges) : I = J

theorem BKAR.ForestIndex.ext_iff {V : Type u_1} [Fintype V] [DecidableEq V] {I J : ForestIndex V} : I = J ↔ I.edges = J.edges

structure BKAR.Forest (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

A forest is a finite edge set with the path API needed for BKAR interpolation.

• edges : Finset (Edge V)

  The finite edge set of the forest.

• acyclic : AcyclicEdgeSetData self.edges

  The component and unique-path data witnessing acyclicity of the edge set.

• acyclic_insert_iff' {i j : V} (hij : i ≠ j) : Edge.mk i j hij ∉ self.edges → (IsAcyclicEdgeSet (insert (Edge.mk i j hij) self.edges) ↔ ¬self.acyclic.inSameComponent i j)

def BKAR.Forest.emptyAcyclicEdgeSetData {V : Type u_1} [Fintype V] [DecidableEq V] : AcyclicEdgeSetData ∅

Acyclicity data for the empty edge set.

Equations

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

def BKAR.Forest.singletonAcyclicEdgeSetData {V : Type u_1} [Fintype V] [DecidableEq V] (e₀ : Edge V) : AcyclicEdgeSetData {e₀}

Acyclicity data for a singleton edge set.

Equations

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

def BKAR.Forest.empty (V : Type u_1) [Fintype V] [DecidableEq V] : Forest V

The empty forest, with equality as its component relation.

Equations

• BKAR.Forest.empty V = { edges := ∅, acyclic := BKAR.Forest.emptyAcyclicEdgeSetData, acyclic_insert_iff' := ⋯ }

theorem BKAR.Forest.empty_edges (V : Type u_1) [Fintype V] [DecidableEq V] : (empty V).edges = ∅

theorem BKAR.Forest.isAcyclicEdgeSet {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : IsAcyclicEdgeSet F.edges

def BKAR.Forest.support {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : ForestIndex V

Forget the path data of a Forest representative, retaining only its finite edge-set index.

Equations

• F.support = { edges := F.edges, acyclic := ⋯ }

theorem BKAR.Forest.support_edges {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) : F.support.edges = F.edges

theorem BKAR.Forest.empty_support {V : Type u_1} [Fintype V] [DecidableEq V] : (empty V).support = { edges := ∅, acyclic := ⋯ }

def BKAR.Forest.inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (i j : V) : Prop

The component relation of a forest.

Equations

• F.inSameComponent i j = F.acyclic.inSameComponent i j

theorem BKAR.Forest.empty_inSameComponent_iff {V : Type u_1} [Fintype V] [DecidableEq V] {i j : V} : (empty V).inSameComponent i j ↔ i = j

@[instance_reducible]

noncomputable instance BKAR.Forest.instDecidableInSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (i j : V) : Decidable (F.inSameComponent i j)

Equations

• F.instDecidableInSameComponent i j = Classical.propDecidable (F.inSameComponent i j)

def BKAR.Forest.pathInF {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (i j : V) (h : F.inSameComponent i j) : List (Edge V)

The canonical path between vertices known to be in the same component.

Equations

• F.pathInF i j h = F.acyclic.pathIn i j h

def BKAR.IsSimplePath {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) (γ : List (Edge V)) (i j : V) : Prop

Simple paths in a forest, as exposed by its acyclicity certificate.

Equations

• BKAR.IsSimplePath F γ i j = F.acyclic.isSimplePath γ i j

theorem BKAR.Forest.pathInF_isSimple {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {i j : V} (h : F.inSameComponent i j) : IsSimplePath F (F.pathInF i j h) i j

theorem BKAR.Forest.inSameComponent_of_isSimplePath {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {i j : V} {γ : List (Edge V)} (hγ : IsSimplePath F γ i j) : F.inSameComponent i j

theorem BKAR.Forest.edge_mem_of_isSimplePath {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {i j : V} {γ : List (Edge V)} (hγ : IsSimplePath F γ i j) (e : Edge V) : e ∈ γ → e ∈ F.edges

theorem BKAR.Forest.edge_isSimplePath {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.edges) : IsSimplePath F [e] e.left e.right

theorem BKAR.Forest.edge_inSameComponent {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.edges) : F.inSameComponent e.left e.right

theorem BKAR.Forest.pathInF_unique {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {i j : V} (h : F.inSameComponent i j) (γ : List (Edge V)) (hγ : IsSimplePath F γ i j) : γ = F.pathInF i j h

Lemma A1: the simple path in a forest is unique.

theorem BKAR.Forest.pathInF_eq_singleton_of_edge_mem {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {e : Edge V} (he : e ∈ F.edges) : F.pathInF e.left e.right ⋯ = [e]

theorem BKAR.Forest.isSimplePath_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) {γ : List (Edge V)} {i j : V} (hγ : IsSimplePath F γ i j) : IsSimplePath G γ i j

Simple paths are invariant under replacing the Forest representative data by another forest with the same underlying edge set.

theorem BKAR.Forest.inSameComponent_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) {i j : V} (h : F.inSameComponent i j) : G.inSameComponent i j

The component relation is invariant under changing only the auxiliary path data.

theorem BKAR.Forest.inSameComponent_iff_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) {i j : V} : F.inSameComponent i j ↔ G.inSameComponent i j

theorem BKAR.Forest.pathInF_eq_of_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (F G : Forest V) (hedges : F.edges = G.edges) {i j : V} (hF : F.inSameComponent i j) (hG : G.inSameComponent i j) : F.pathInF i j hF = G.pathInF i j hG

Canonical paths are invariant under changing only the Forest representative data, once the underlying edge set is fixed.

theorem BKAR.Forest.acyclic_insert_iff {V : Type u_1} [Fintype V] [DecidableEq V] (F : Forest V) {i j : V} (hij : i ≠ j) (he : Edge.mk i j hij ∉ F.edges) : IsAcyclicEdgeSet (insert (Edge.mk i j hij) F.edges) ↔ ¬F.inSameComponent i j

Lemma A2: adding an absent edge preserves acyclicity exactly across components.

structure BKAR.Forest.EdgeExtension {V : Type u_1} [Fintype V] [DecidableEq V] (F F' : Forest V) (e₀ : Edge V) : Prop

Certificate that F' is obtained from F by adding one edge and that the canonical paths behave as expected under this extension.

• new_not_mem : e₀ ∉ F.edges
• edges_eq : F'.edges = insert e₀ F.edges
• old_component {i j : V} : F.inSameComponent i j → F'.inSameComponent i j
• old_path {i j : V} (h : F.inSameComponent i j) : F'.pathInF i j ⋯ = F.pathInF i j h
• new_path_uses {i j : V} : ¬F.inSameComponent i j → ∀ (hF' : F'.inSameComponent i j), e₀ ∈ F'.pathInF i j hF'

theorem BKAR.Forest.EdgeExtension.new_mem {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ : Edge V} (h : F.EdgeExtension F' e₀) : e₀ ∈ F'.edges

theorem BKAR.Forest.EdgeExtension.old_mem {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ e : Edge V} (h : F.EdgeExtension F' e₀) (he : e ∈ F.edges) : e ∈ F'.edges

theorem BKAR.Forest.EdgeExtension.mem_old_of_mem_of_ne {V : Type u_1} [Fintype V] [DecidableEq V] {F F' : Forest V} {e₀ e : Edge V} (h : F.EdgeExtension F' e₀) (he : e ∈ F'.edges) (hne : e ≠ e₀) : e ∈ F.edges

def BKAR.ForestIndex.singleton {V : Type u_1} [Fintype V] [DecidableEq V] (e : Edge V) : ForestIndex V

The finite forest index consisting of one edge.

Equations

• BKAR.ForestIndex.singleton e = { edges := {e}, acyclic := ⋯ }

theorem BKAR.ForestIndex.singleton_edges {V : Type u_1} [Fintype V] [DecidableEq V] (e : Edge V) : (singleton e).edges = {e}