Encyclopedia Foundation Foundation Pair Kernel Lattice3 Pair Min Ge One Via Edge Flow
Foundation Pair Kernel Lattice3 Pair Min Ge One Via Edge Flow
A machine-checked theorem shows that in a graph where every connection costs either zero or one, any direct link forces the minimum flow cost between its endpoints to be at least one.
The edge-flow bound
In graph theory, a common question is how cheaply one can move a unit of something between two points, given that moving along an edge has a cost. The ledger, a discrete record of such movements, assigns a cost to each possible flow. The theorem pairMin_ge_one_via_edge_flow answers this for a specific class of graphs: when every edge has a weight of either 0 or 1, and two distinct sites are directly connected by an edge of weight 1, then the minimum cost to send one unit from one site to the other is at least 1.
This is a lower bound, not an exact value. It says the cost cannot be less than 1, but it does not say it equals 1. The proof works by considering a flow that uses the direct edge, which has cost 1, and showing that any valid flow must have at least that much energy. The theorem is proved in the machine-checked library of formal theorems, meaning the reasoning is verified by a computer and requires no unproven assumptions.
The bound is a stepping stone for a larger project: building a three-dimensional lattice model. In that model, sites are arranged in a box, and the weight of an edge is 1 if two sites are adjacent in the ℓ¹ (taxicab) metric, and 0 otherwise. The theorem applies directly to this box, guaranteeing that the minimum flow cost between any two directly adjacent sites is at least 1. This is a concrete, verified fact about the cost structure of the three-dimensional carrier, distinct from the broader, still-open question of how this cost behaves at large distances.
THEOREM pairMin_ge_one_via_edge_flow · IndisputableMonolith/Foundation/PairKernelLattice3.lean
/-- The single-edge unit flow certifies `pairMin ≥ 1` across any weight-1 edge, purely through
`pairMin_ge_inv_flowEnergy`. Consistency witness: same conclusion as `pairMin_ge_weight`. -/
theorem pairMin_ge_one_via_edge_flow {n : ℕ} (G : WeightedLedgerGraph n)
(hw01 : ∀ i j, G.weight i j = 0 ∨ G.weight i j = 1)
{a b : Fin n} (hab : a ≠ b) (hedge : G.weight a b = 1) :
1 ≤ pairMin G a b := by
set θ : Fin n → Fin n → ℝ := fun i j =>
if i = a ∧ j = b then (1 : ℝ) else if i = b ∧ j = a then (-1 : ℝ) else 0 with hθ
have hθval : ∀ i j : Fin n, θ i j
= if i = a ∧ j = b then (1 : ℝ) else if i = b ∧ j = a then (-1 : ℝ) else 0 := by
intro i j
simp only [hθ]
-- Pointwise case analysis of the current: one outgoing, one incoming, else zero.
have hval_ab : θ a b = 1 := by rw [hθval, if_pos ⟨rfl, rfl⟩]
have hval_ba : θ b a = -1 := by
rw [hθval, if_neg (by rintro ⟨h1, _⟩; exact hab h1.symm), if_pos ⟨rfl, rfl⟩]
have hval_a_off : ∀ j : Fin n, j ≠ b → θ a j = 0 := by
intro j hj
rw [hθval, if_neg (by rintro ⟨_, h2⟩; exact hj h2),
if_neg (by rintro ⟨h1, _⟩; exact hab h1)]
have hval_b_off : ∀ j : Fin n, j ≠ a → θ b j = 0 := by
intro j hj
rw [hθval, if_neg (by rintro ⟨h1, _⟩; exact hab h1.symm),
if_neg (by rintro ⟨_, h2⟩; exact hj h2)]
have hval_off : ∀ i j : Fin n, i ≠ a → i ≠ b → θ i j = 0 := by
intro i j hia hib
rw [hθval, if_neg (by rintro ⟨h1, _⟩; exact hia h1),
if_neg (by rintro ⟨h1, _⟩; exact hib h1)]
-- Row sums of the current.
have hrow_a : (∑ j : Fin n, θ a j) = 1 := by
rw [Finset.sum_eq_single_of_mem b (Finset.mem_univ b)
(fun j _ hj => hval_a_off j hj), hval_ab]
have hrow_b : (∑ j : Fin n, θ b j) = -1 := by
rw [Finset.sum_eq_single_of_mem a (Finset.mem_univ a)
(fun j _ hj => hval_b_off j hj), hval_ba]
-- Antisymmetry: exhaustive case split on membership of i, j in {a, b}.
have hanti : IsAntisym θ := by
intro i j
by_cases hia : i = a
· by_cases hjb : j = b
· rw [hia, hjb]; norm_num [hval_ab, hval_ba]
· by_cases hja : j = a
· rw [hia, hja]; norm_num [hval_a_off a hab]
· rw [hia]; norm_num [hval_a_off j hjb, hval_off j a hja hjb]
· by_cases hib : i = b
· by_cases hja : j = a
· rw [hib, hja]; norm_num [hval_ba, hval_ab]
· by_cases hjb : j = b
· rw [hib, hjb]; norm_num [hval_b_off b (Ne.symm hab)]
· rw [hib]; norm_num [hval_b_off j hja, hval_off j b hja hjb]
· by_cases hja : j = a
· rw [hja]; norm_num [hval_off i a hia hib, hval_a_off i hib]
· by_cases hjb : j = b
· rw [hjb]; norm_num [hval_off i b hia hib, hval_b_off i hia]
· norm_num [hval_off i j hia hib, hval_off j i hja hjb]
-- Edge support: θ vanishes off the (weight-1) edge a—b, so weight 0 forces θ = 0.
have hsupp : ∀ i j, G.weight i j = 0 → θ i j = 0 := by
intro i j hw
by_cases hia : i = a
· by_cases hjb : j = b
· exfalso
rw [hia, hjb, hedge] at hw
norm_num at hw
· rw [hia]; exact hval_a_off j hjb
· by_cases hib : i = b
· by_cases hja : j = a
· exfalso
rw [hib, hja, G.weight_symm, hedge] at hw
norm_num at hw
· rw [hib]; exact hval_b_off j hja
· exact hval_off i j hia hib
have hdiva : divF θ a = 1 := hrow_a
have hdiv0 : ∀ i, i ≠ a → i ≠ b → divF θ i = 0 := by
intro i hia hib
exact Finset.sum_eq_zero (fun j _ => hval_off i j hia hib)
-- The dissipation energy of the single-edge unit flow is exactly 1.
have hE_val : flowEnergy θ = 1 := by
have hsq : ∀ i : Fin n, (∑ j : Fin n, θ i j ^ 2)
= if i = a then (1 : ℝ) else if i = b then (1 : ℝ) else 0 := by
intro i
by_cases hia : i = a
· rw [if_pos hia, hia]
rw [Finset.sum_eq_single_of_mem b (Finset.mem_univ b)
(fun j _ hj => by rw [hval_a_off j hj]; norm_num), hval_ab]
norm_num
· by_cases hib : i = b
· rw [if_neg hia, if_pos hib, hib]
rw [Finset.sum_eq_single_of_mem a (Finset.mem_univ a)
(fun j _ hj => by rw [hval_b_off j hj]; norm_num), hval_ba]
norm_num
· rw [if_neg hia, if_neg hib]
exact Finset.sum_eq_zero (fun j _ => by rw [hval_off i j hia hib]; norm_num)
show (1 / 2 : ℝ) * (∑ i : Fin n, ∑ j : Fin n, θ i j ^ 2) = 1
rw [Finset.sum_congr rfl (fun i _ => hsq i)]
have hpair : (∑ i : Fin n, if i = a then (1:ℝ) else if i = b then (1:ℝ) else 0)
= 2 := by
have hzero : ∀ i ∈ (Finset.univ : Finset (Fin n)), i ∉ ({a, b} : Finset (Fin n)) →
(if i = a then (1:ℝ) else if i = b then (1:ℝ) else 0) = 0 := by
intro i _ hi
simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hi
rw [if_neg hi.1, if_neg hi.2]
rw [← Finset.sum_subset (Finset.subset_univ ({a, b} : Finset (Fin n))) hzero]
rw [Finset.sum_pair hab, if_pos rfl, if_neg (Ne.symm hab), if_pos rfl]
norm_num
rw [hpair]
norm_num
have hbound := pairMin_ge_inv_flowEnergy G hw01 hab θ hanti hsupp hdiva hdiv0
(by rw [hE_val]; norm_num)
rw [hE_val] at hbound
norm_num at hbound
exact hbound
What this page does not claim
The theorem does not provide an upper bound on the minimum flow cost. The theorem does not establish the value of the minimum flow cost for sites that are not directly adjacent. The theorem does not claim that the three-dimensional box model is physically realized.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Foundation/PairKernelLattice3.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What is the exact minimum flow cost between two sites in the three-dimensional box, not just the lower bound?
- How does this edge-flow bound relate to the effective resistance between two points in a lattice?
- Does the minimum flow cost in three dimensions decay with distance, or does it approach a positive constant?
- What is the continuum limit of this discrete flow cost model?
- How does this discrete model connect to the physical Coulomb potential in three dimensions?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM pairMin_ge_one_via_edge_flow · IndisputableMonolith/Foundation/PairKernelLattice3.lean
/-- The single-edge unit flow certifies `pairMin ≥ 1` across any weight-1 edge, purely through `pairMin_ge_inv_flowEnergy`. Consistency witness: same conclusion as `pairMin_ge_weight`. -/ theorem pairMin_ge_one_via_edge_flow {n : ℕ} (G : WeightedLedgerGraph n) (hw01 : ∀ i j, G.weight i j = 0 ∨ G.weight i j = 1) {a b : Fin n} (hab : a ≠ b) (hedge : G.weight a b = 1) : 1 ≤ pairMin G a b := by set θ : Fin n → Fin n → ℝ := fun i j => if i = a ∧ j = b then (1 : ℝ) else if i = b ∧ j = a then (-1 : ℝ) else 0 with hθ have hθval : ∀ i j : Fin n, θ i j = if i = a ∧ j = b then (1 : ℝ) else if i = b ∧ j = a then (-1 : ℝ) else 0 := by intro i j simp only [hθ] -- Pointwise case analysis of the current: one outgoing, one incoming, else zero. have hval_ab : θ a b = 1 := by rw [hθval, if_pos ⟨rfl, rfl⟩] have hval_ba : θ b a = -1 := by rw [hθval, if_neg (by rintro ⟨h1, _⟩; exact hab h1.symm), if_pos ⟨rfl, rfl⟩] have hval_a_off : ∀ j : Fin n, j ≠ b → θ a j = 0 := by intro j hj rw [hθval, if_neg (by rintro ⟨_, h2⟩; exact hj h2), if_neg (by rintro ⟨h1, _⟩; exact hab h1)] have hval_b_off : ∀ j : Fin n, j ≠ a → θ b j = 0 := by intro j hj rw [hθval, if_neg (by rintro ⟨h1, _⟩; exact hab h1.symm), if_neg (by rintro ⟨_, h2⟩; exact hj h2)] have hval_off : ∀ i j : Fin n, i ≠ a → i ≠ b → θ i j = 0 := by intro i j hia hib rw [hθval, if_neg (by rintro ⟨h1, _⟩; exact hia h1), if_neg (by rintro ⟨h1, _⟩; exact hib h1)] -- Row sums of the current. have hrow_a : (∑ j : Fin n, θ a j) = 1 := by rw [Finset.sum_eq_single_of_mem b (Finset.mem_univ b) (fun j _ hj => hval_a_off j hj), hval_ab] have hrow_b : (∑ j : Fin n, θ b j) = -1 := by rw [Finset.sum_eq_single_of_mem a (Finset.mem_univ a) (fun j _ hj => hval_b_off j hj), hval_ba] -- Antisymmetry: exhaustive case split on membership of i, j in {a, b}. have hanti : IsAntisym θ := by intro i j by_cases hia : i = a · by_cases hjb : j = b · rw [hia, hjb]; norm_num [hval_ab, hval_ba] · by_cases hja : j = a · rw [hia, hja]; norm_num [hval_a_off a hab] · rw [hia]; norm_num [hval_a_off j hjb, hval_off j a hja hjb] · by_cases hib : i = b · by_cases hja : j = a · rw [hib, hja]; norm_num [hval_ba, hval_ab] · by_cases hjb : j = b · rw [hib, hjb]; norm_num [hval_b_off b (Ne.symm hab)] · rw [hib]; norm_num [hval_b_off j hja, hval_off j b hja hjb] · by_cases hja : j = a · rw [hja]; norm_num [hval_off i a hia hib, hval_a_off i hib] · by_cases hjb : j = b · rw [hjb]; norm_num [hval_off i b hia hib, hval_b_off i hia] · norm_num [hval_off i j hia hib, hval_off j i hja hjb] -- Edge support: θ vanishes off the (weight-1) edge a—b, so weight 0 forces θ = 0. have hsupp : ∀ i j, G.weight i j = 0 → θ i j = 0 := by intro i j hw by_cases hia : i = a · by_cases hjb : j = b · exfalso rw [hia, hjb, hedge] at hw norm_num at hw · rw [hia]; exact hval_a_off j hjb · by_cases hib : i = b · by_cases hja : j = a · exfalso rw [hib, hja, G.weight_symm, hedge] at hw norm_num at hw · rw [hib]; exact hval_b_off j hja · exact hval_off i j hia hib have hdiva : divF θ a = 1 := hrow_a have hdiv0 : ∀ i, i ≠ a → i ≠ b → divF θ i = 0 := by intro i hia hib exact Finset.sum_eq_zero (fun j _ => hval_off i j hia hib) -- The dissipation energy of the single-edge unit flow is exactly 1. have hE_val : flowEnergy θ = 1 := by have hsq : ∀ i : Fin n, (∑ j : Fin n, θ i j ^ 2) = if i = a then (1 : ℝ) else if i = b then (1 : ℝ) else 0 := by intro i by_cases hia : i = a · rw [if_pos hia, hia] rw [Finset.sum_eq_single_of_mem b (Finset.mem_univ b) (fun j _ hj => by rw [hval_a_off j hj]; norm_num), hval_ab] norm_num · by_cases hib : i = b · rw [if_neg hia, if_pos hib, hib] rw [Finset.sum_eq_single_of_mem a (Finset.mem_univ a) (fun j _ hj => by rw [hval_b_off j hj]; norm_num), hval_ba] norm_num · rw [if_neg hia, if_neg hib] exact Finset.sum_eq_zero (fun j _ => by rw [hval_off i j hia hib]; norm_num) show (1 / 2 : ℝ) * (∑ i : Fin n, ∑ j : Fin n, θ i j ^ 2) = 1 rw [Finset.sum_congr rfl (fun i _ => hsq i)] have hpair : (∑ i : Fin n, if i = a then (1:ℝ) else if i = b then (1:ℝ) else 0) = 2 := by have hzero : ∀ i ∈ (Finset.univ : Finset (Fin n)), i ∉ ({a, b} : Finset (Fin n)) → (if i = a then (1:ℝ) else if i = b then (1:ℝ) else 0) = 0 := by intro i _ hi simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hi rw [if_neg hi.1, if_neg hi.2] rw [← Finset.sum_subset (Finset.subset_univ ({a, b} : Finset (Fin n))) hzero] rw [Finset.sum_pair hab, if_pos rfl, if_neg (Ne.symm hab), if_pos rfl] norm_num rw [hpair] norm_num have hbound := pairMin_ge_inv_flowEnergy G hw01 hab θ hanti hsupp hdiva hdiv0 (by rw [hE_val]; norm_num) rw [hE_val] at hbound norm_num at hbound exact hboundwhen every edge has a weight of either 0 or 1, and two distinct sites are directly connected by an edge of weight 1, then the minimum cost to send one unit from one site to the other is at least 1. pairMin_ge_one_via_edge_flow · IndisputableMonolith/Foundation/PairKernelLattice3.lean