Encyclopedia Foundation Foundation Pair Kernel Lattice3 Pair Min Ge Via Two Disjoint Walks

ARTICLE 1 claim 1 theorem

Foundation Pair Kernel Lattice3 Pair Min Ge Via Two Disjoint Walks

A theorem about the minimum cost of connecting two points in a network, proved by finding two separate routes.

Verify this page

The two-path lower bound

In graph theory, the effective resistance between two nodes is a measure of how hard it is to push current between them through a network of resistors. The Recognition Science framework's ledger, a discrete record of events, treats this resistance as a cost: the minimum energy needed to connect two sites. The declaration pairMin_ge_via_two_paths proves a lower bound on this cost using a simple geometric idea. If two distinct paths connect the same pair of points, and each path is made of unit-cost steps, then the minimum cost is at least 1. The proof constructs a flow that splits evenly between the two paths, and the energy of that flow is exactly 1, so the true minimum cannot be smaller.

The result is a theorem in the machine-checked library of formal theorems, proved without any additional axioms. It applies to any graph whose edge weights are either 0 or 1, and it requires the two paths to share no vertices except their endpoints. The theorem is a sharpening of an earlier bound: a single path of length m only gives the weaker bound 1/m, which shrinks as the path grows. Two disjoint paths give a constant bound that does not shrink, because the flow can be split between them. This is the first step toward a deeper fact: in three dimensions, the minimum cost between distant points stays bounded away from zero, unlike in one dimension where it decays like 1/distance.

The theorem does not claim that two paths always exist, nor that the bound is tight. It only says that if two disjoint unit-cost paths exist, then the cost is at least 1. In the three-dimensional lattice box where this theorem is applied, the two paths are constructed explicitly along two different axes, giving the constant lower bound that the dimension dichotomy requires. The theorem is a tool, not a conclusion: it provides the lower bound, but the full statement about three-dimensional behavior remains an open target.

THEOREM pairMin_ge_one_via_two_paths · IndisputableMonolith/Foundation/PairKernelLattice3.lean
pairMin_ge_one_via_two_paths · IndisputableMonolith/Foundation/PairKernelLattice3.lean:839 
/-- **Two-parallel-paths lower bound (graph-generic).** Let `a, u, v, b` be four distinct sites of
    a 0/1-weighted ledger graph, with the four edges `a—u`, `u—b`, `a—v`, `v—b` all present
    (weight `1`). Then `pairMin G a b ≥ 1`, even though `a, b` need not be adjacent: the unit flow
    that splits `½ : ½` between the two length-2 paths dissipates energy exactly `1`, and Thomson
    duality (`pairMin_ge_inv_flowEnergy`) turns that into the lower bound. Contrast the 1D chain,
    where a distance-2 pair has `pairMin ≤ ½` (`pairMin_band_le_inv_dist`) because no second
    parallel route exists — this is the smallest strict recurrence/transience witness. -/
theorem pairMin_ge_one_via_two_paths {n : ℕ} (G : WeightedLedgerGraph n)
    (hw01 : ∀ i j, G.weight i j = 0 ∨ G.weight i j = 1)
    {a u v b : Fin n}
    (hau : a ≠ u) (hav : a ≠ v) (hab : a ≠ b)
    (hub : u ≠ b) (hvb : v ≠ b) (huv : u ≠ v)
    (wau : G.weight a u = 1) (wub : G.weight u b = 1)
    (wav : G.weight a v = 1) (wvb : G.weight v b = 1) :
    (1:ℝ) ≤ pairMin G a b := by
  have hua := hau.symm
  have hva := hav.symm
  have hba := hab.symm
  have hbu := hub.symm
  have hbv := hvb.symm
  have hvu := huv.symm
  have htheta : ∀ i j : Fin n, twoPathFlow a u v b i j
      = (1 / 2) * ((if i = a ∧ j = u then (1:ℝ) else if i = u ∧ j = a then (-1:ℝ) else 0)
                 + (if i = u ∧ j = b then (1:ℝ) else if i = b ∧ j = u then (-1:ℝ) else 0)
                 + (if i = a ∧ j = v then (1:ℝ) else if i = v ∧ j = a then (-1:ℝ) else 0)
                 + (if i = v ∧ j = b then (1:ℝ) else if i = b ∧ j = v then (-1:ℝ) else 0)) := by
    intro i j
    unfold twoPathFlow fourEdgeSum
    rw [ep_val hau i j, ep_val hub i j, ep_val hav i j, ep_val hvb i j]
  have tau_au : twoPathFlow a u v b a u = 1 / 2 := by
    rw [htheta a u, if_pos (⟨rfl, rfl⟩ : a = a ∧ u = u),
        if_neg (fun h => hau h.1), if_neg (fun h => hab h.1),
        if_neg (fun h => huv h.2), if_neg (fun h => hav h.1),
        if_neg (fun h => hav h.1), if_neg (fun h => hab h.1)]
    norm_num
  have tau_av : twoPathFlow a u v b a v = 1 / 2 := by
    rw [htheta a v,
        if_neg (fun h => hvu h.2), if_neg (fun h => hau h.1),
        if_neg (fun h => hau h.1), if_neg (fun h => hab h.1),
        if_pos (⟨rfl, rfl⟩ : a = a ∧ v = v),
        if_neg (fun h => hav h.1), if_neg (fun h => hab h.1)]
    norm_num
  have tau_ua : twoPathFlow a u v b u a = -1 / 2 := by
    rw [htheta u a,
        if_neg (fun h => hua h.1), if_pos (⟨rfl, rfl⟩ : u = u ∧ a = a),
        if_neg (fun h => hab h.2), if_neg (fun h => hub h.1),
        if_neg (fun h => hua h.1), if_neg (fun h => huv h.1),
        if_neg (fun h => huv h.1), if_neg (fun h => hub h.1)]
    norm_num
  have tau_ub : twoPathFlow a u v b u b = 1 / 2 := by
    rw [htheta u b,
        if_neg (fun h => hua h.1), if_neg (fun h => hba h.2),
        if_pos (⟨rfl, rfl⟩ : u = u ∧ b = b),
        if_neg (fun h => hua h.1), if_neg (fun h => huv h.1),
        if_neg (fun h => huv h.1), if_neg (fun h => hub h.1)]
    norm_num
  have tau_va : twoPathFlow a u v b v a = -1 / 2 := by
    rw [htheta v a,
        if_neg (fun h => hva h.1), if_neg (fun h => hvu h.1),
        if_neg (fun h => hvu h.1), if_neg (fun h => hvb h.1),
        if_neg (fun h => hva h.1), if_pos (⟨rfl, rfl⟩ : v = v ∧ a = a),
        if_neg (fun h => hab h.2), if_neg (fun h => hvb h.1)]
    norm_num
  have tau_vb : twoPathFlow a u v b v b = 1 / 2 := by
    rw [htheta v b,
        if_neg (fun h => hva h.1), if_neg (fun h => hvu h.1),
        if_neg (fun h => hvu h.1), if_neg (fun h => hvb h.1),
        if_neg (fun h => hva h.1), if_neg (fun h => hba h.2),
        if_pos (⟨rfl, rfl⟩ : v = v ∧ b = b)]
    norm_num
  have tau_bu : twoPathFlow a u v b b u = -1 / 2 := by
    rw [htheta b u,
        if_neg (fun h => hba h.1), if_neg (fun h => hbu h.1),
        if_neg (fun h => hbu h.1), if_pos (⟨rfl, rfl⟩ : b = b ∧ u = u),
        if_neg (fun h => hba h.1), if_neg (fun h => hbv h.1),
        if_neg (fun h => hbv h.1), if_neg (fun h => huv h.2)]
    norm_num
  have tau_bv : twoPathFlow a u v b b v = -1 / 2 := by
    rw [htheta b v,
        if_neg (fun h => hba h.1), if_neg (fun h => hbu h.1),
        if_neg (fun h => hbu h.1), if_neg (fun h => hvu h.2),
        if_neg (fun h => hba h.1), if_neg (fun h => hbv h.1),
        if_neg (fun h => hbv h.1), if_pos (⟨rfl, rfl⟩ : b = b ∧ v = v)]
    norm_num
  have theta_a_off : ∀ j : Fin n, j ≠ u → j ≠ v → twoPathFlow a u v b a j = 0 := by
    intro j hju hjv
    rw [htheta a j,
        if_neg (fun h => hju h.2), if_neg (fun h => hau h.1),
        if_neg (fun h => hau h.1), if_neg (fun h => hab h.1),
        if_neg (fun h => hjv h.2), if_neg (fun h => hav h.1),
        if_neg (fun h => hav h.1), if_neg (fun h => hab h.1)]
    norm_num
  have theta_u_off : ∀ j : Fin n, j ≠ a → j ≠ b → twoPathFlow a u v b u j = 0 := by
    intro j hja hjb
    rw [htheta u j,
        if_neg (fun h => hua h.1), if_neg (fun h => hja h.2),
        if_neg (fun h => hjb h.2), if_neg (fun h => hub h.1),
        if_neg (fun h => hua h.1), if_neg (fun h => huv h.1),
        if_neg (fun h => huv h.1), if_neg (fun h => hub h.1)]
    norm_num
  have theta_v_off : ∀ j : Fin n, j ≠ a → j ≠ b → twoPathFlow a u v b v j = 0 := by
    intro j hja hjb
    rw [htheta v j,
        if_neg (fun h => hva h.1), if_neg (fun h => hvu h.1),
        if_neg (fun h => hvu h.1), if_neg (fun h => hvb h.1),
        if_neg (fun h => hva h.1), if_neg (fun h => hja h.2),
        if_neg (fun h => hjb h.2), if_neg (fun h => hvb h.1)]
    norm_num
  have theta_b_off : ∀ j : Fin n, j ≠ u → j ≠ v → twoPathFlow a u v b b j = 0 := by
    intro j hju hjv
    rw [htheta b j,
        if_neg (fun h => hba h.1), if_neg (fun h => hbu h.1),
        if_neg (fun h => hbu h.1), if_neg (fun h => hju h.2),
        if_neg (fun h => hba h.1), if_neg (fun h => hbv h.1),
        if_neg (fun h => hbv h.1), if_neg (fun h => hjv h.2)]
    norm_num
  have theta_row_zero : ∀ i j : Fin n, i ≠ a → i ≠ u → i ≠ v → i ≠ b →
      twoPathFlow a u v b i j = 0 := by
    intro i j hia hiu hiv hib
    rw [htheta i j,
        if_neg (fun h => hia h.1), if_neg (fun h => hiu h.1),
        if_neg (fun h => hiu h.1), if_neg (fun h => hib h.1),
        if_neg (fun h => hia h.1), if_neg (fun h => hiv h.1),
        if_neg (fun h => hiv h.1), if_neg (fun h => hib h.1)]
    norm_num
  have rowa : (∑ j : Fin n, twoPathFlow a u v b a j ^ 2) = 1 / 2 := by
    have hz : ∀ j ∈ (Finset.univ : Finset (Fin n)), j ∉ ({u, v} : Finset (Fin n)) →
        twoPathFlow a u v b a j ^ 2 = 0 := by
      intro j _ hj
      simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hj
      rw [theta_a_off j hj.1 hj.2]; norm_num
    rw [← Finset.sum_subset (Finset.subset_univ ({u, v} : Finset (Fin n))) hz,
        Finset.sum_pair huv, tau_au, tau_av]
    norm_num
  have rowu : (∑ j : Fin n, twoPathFlow a u v b u j ^ 2) = 1 / 2 := by
    have hz : ∀ j ∈ (Finset.univ : Finset (Fin n)), j ∉ ({a, b} : Finset (Fin n)) →
        twoPathFlow a u v b u j ^ 2 = 0 := by
      intro j _ hj
      simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hj
      rw [theta_u_off j hj.1 hj.2]; norm_num
    rw [← Finset.sum_subset (Finset.subset_univ ({a, b} : Finset (Fin n))) hz,
        Finset.sum_pair hab, tau_ua, tau_ub]
    norm_num
  have rowv : (∑ j : Fin n, twoPathFlow a u v b v j ^ 2) = 1 / 2 := by
    have hz : ∀ j ∈ (Finset.univ : Finset (Fin n)), j ∉ ({a, b} : Finset (Fin n)) →
        twoPathFlow a u v b v j ^ 2 = 0 := by
      intro j _ hj
      simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hj
      rw [theta_v_off j hj.1 hj.2]; norm_num
    rw [← Finset.sum_subset (Finset.subset_univ ({a, b} : Finset (Fin n))) hz,
        Finset.sum_pair hab, tau_va, tau_vb]
    norm_num
  have rowb : (∑ j : Fin n, twoPathFlow a u v b b j ^ 2) = 1 / 2 := by
    have hz : ∀ j ∈ (Finset.univ : Finset (Fin n)), j ∉ ({u, v} : Finset (Fin n)) →
        twoPathFlow a u v b b j ^ 2 = 0 := by
      intro j _ hj
      simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hj
      rw [theta_b_off j hj.1 hj.2]; norm_num
    rw [← Finset.sum_subset (Finset.subset_univ ({u, v} : Finset (Fin n))) hz,
        Finset.sum_pair huv, tau_bu, tau_bv]
    norm_num
  have hset : (∑ i ∈ ({a, u, v, b} : Finset (Fin n)), ∑ j : Fin n, twoPathFlow a u v b i j ^ 2)
      = (∑ j : Fin n, twoPathFlow a u v b a j ^ 2)
        + (∑ j : Fin n, twoPathFlow a u v b u j ^ 2)
        + (∑ j : Fin n, twoPathFlow a u v b v j ^ 2)
        + (∑ j : Fin n, twoPathFlow a u v b b j ^ 2) := by
    rw [Finset.sum_insert (by
          simp only [Finset.mem_insert, Finset.mem_singleton, not_or]; exact ⟨hau, hav, hab⟩),
        Finset.sum_insert (by
          simp only [Finset.mem_insert, Finset.mem_singleton, not_or]; exact ⟨huv, hub⟩),
        Finset.sum_insert (by
          simp only [Finset.mem_singleton]; exact hvb),
        Finset.sum_singleton]
    ring
  have hE : flowEnergy (twoPathFlow a u v b) = 1 := by
    unfold flowEnergy
    have hz : ∀ i ∈ (Finset.univ : Finset (Fin n)), i ∉ ({a, u, v, b} : Finset (Fin n)) →
        (∑ j : Fin n, twoPathFlow a u v b i j ^ 2) = 0 := by
      intro i _ hi
      simp only [Finset.mem_insert, Finset.mem_singleton, not_or] at hi
      exact Finset.sum_eq_zero (fun j _ => by
        rw [theta_row_zero i j hi.1 hi.2.1 hi.2.2.1 hi.2.2.2]; norm_num)
    rw [← Finset.sum_subset (Finset.subset_univ ({a, u, v, b} : Finset (Fin n))) hz,
        hset, rowa, rowu, rowv, rowb]
    norm_num
  have hsupp : ∀ i j, G.weight i j = 0 → twoPathFlow a u v b i j = 0 := by
    intro i j hw
    unfold twoPathFlow fourEdgeSum
    rw [ep_zero_of_weight_zero G hau wau i j hw, ep_zero_of_weight_zero G hub wub i j hw,
        ep_zero_of_weight_zero G hav wav i j hw, ep_zero_of_weight_zero G hvb wvb i j hw]
    ring
  have hdiva : divF (twoPathFlow a u v b) a = 1 := by
    rw [twoPathFlow_divF, elementaryPosting_div_source a u hau, ep_div_off u b a hau hab,
        elementaryPosting_div_source a v hav, ep_div_off v b a hav hab]
    norm_num
  have hdiv0 : ∀ i, i ≠ a → i ≠ b → divF (twoPathFlow a u v b) i = 0 := by
    intro i hia hib
    rw [twoPathFlow_divF]
    by_cases hiu : i = u
    · rw [hiu, elementaryPosting_div_sink a u hau, elementaryPosting_div_source u b hub,
          ep_div_off a v u hua huv, ep_div_off v b u huv hub]
      norm_num
    · by_cases hiv : i = v
      · rw [hiv, ep_div_off a u v hva hvu, ep_div_off u b v hvu hvb,
            elementaryPosting_div_sink a v hav, elementaryPosting_div_source v b hvb]
        norm_num
      · rw [ep_div_off a u i hia hiu, ep_div_off u b i hiu hib,
            ep_div_off a v i hia hiv, ep_div_off v b i hiv hib]
        norm_num
  have hEpos : 0 < flowEnergy (twoPathFlow a u v b) := by rw [hE]; norm_num
  have hbound := pairMin_ge_inv_flowEnergy G hw01 hab (twoPathFlow a u v b)
    (twoPathFlow_antisym a u v b) hsupp hdiva hdiv0 hEpos
  rw [hE] at hbound
  norm_num at hbound
  exact hbound

What this page does not claim

The theorem does not prove that two disjoint paths always exist in any given graph. The theorem does not establish the three-dimensional dimension dichotomy, which remains an open target. The theorem does not claim the bound is tight or that the minimum cost equals 1.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND