Encyclopedia Foundation Foundation Pair Kernel Lattice3 Pair Min Ge Inv Path Length

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Lattice3 Pair Min Ge Inv Path Length

A machine-checked theorem about costs on a lattice proves a simple geometric fact: the minimum cost between two points grows at least as fast as one over their distance.

Verify this page

The path length bound

Consider a finite graph whose edges are unweighted, meaning every connection has the same cost of 1, and where the graph is undirected, so travel works the same in both directions. The theorem pairMin, the minimum possible cost of a flow between two distinct vertices, is at least 1 divided by the length of any simple path connecting them. In plain terms, if two vertices are connected by a path of m edges, then the cheapest way to move one unit of something between them cannot cost less than 1/m.

The proof is direct. A unit flow along that path spreads its effort across m edges, each carrying at most 1/m of the total. Since the cost of a flow is the sum of the squares of the edge amounts, the total cost is at most m times (1/m)², which equals 1/m. The minimum cost over all flows is therefore at least 1/m. The theorem states this lower bound exactly: for any graph with edge weights 0 or 1, any injective path of length m, and any two distinct endpoints, the inequality 1/m ≤ pairMin holds.

This bound becomes the backbone of a three-dimensional lattice construction in the framework's machine-checked library of formal theorems. The library builds a box of L×L×L sites, connects each site to its six nearest neighbors, and then applies the path bound to show that the minimum cost between two sites separated by r steps along an axis is at least 1/r. That result, pairMin_box_axial_ge_inv, is a direct instance of the general path-length theorem. A stronger bound, 2/(r+1), follows by using two independent routes between the same endpoints.

In Recognition Science, the framework models a discrete ledger of events where the cost of recognition is forced, not chosen. The path-length theorem belongs to that setting: it constrains how cheaply a ledger can move a unit of recognition between two sites. The theorem does not say the bound is tight, and it does not describe the actual cost, only a floor beneath it. It also does not claim anything about continuous space; the lattice is a discrete carrier, and the classical Coulomb 1/(4πr) law is a separate, still-open target for the Green's function, not for this minimum cost.

What the theorem changes is the qualitative picture in three dimensions. The path bound alone allows the minimum cost to decay toward zero as distance grows, as it does in one dimension. But on the 3D box, the framework's analysis shows the cost saturates at a positive constant, a behavior the path bound does not by itself establish. The path-length theorem is the reusable tool; the saturation is the consequence built on top of it.

The honest scope: the theorem is a proved statement about finite graphs with 0/1 weights. It is not a statement about physics, about continuous metrics, or about the actual value of the cost in any specific graph beyond the lower bound. It is a lemma, machine-checked, that the framework then applies to its lattice constructions.

THEOREM pairMin_ge_inv_pathLength · IndisputableMonolith/Foundation/PairKernelLattice3.lean
pairMin_ge_inv_pathLength · IndisputableMonolith/Foundation/PairKernelLattice3.lean:1301 
/-- **The single-path lower bound (graph-generic).** A simple walk `v 0 → ⋯ → v m` of `m` genuine
    edges (`hedge`) in a 0/1-weighted ledger graph certifies `pairMin G (v 0) (v m) ≥ 1/m`: the unit
    current along the walk dissipates energy exactly `m`, and Thomson duality
    (`pairMin_ge_inv_flowEnergy`) inverts it. This is the flow-side proof that reproduces the 1D
    series-resistance rate; parallel walks (next) beat it. -/
theorem pairMin_ge_inv_pathLength {n : ℕ} (G : WeightedLedgerGraph n)
    (hw01 : ∀ i j, G.weight i j = 0 ∨ G.weight i j = 1)
    (v : ℕ → Fin n) (m : ℕ) (hm : 0 < m)
    (hinj : ∀ i ≤ m, ∀ j ≤ m, v i = v j → i = j)
    (hedge : ∀ k, k < m → G.weight (v k) (v (k + 1)) = 1) :
    (1 : ℝ) / m ≤ pairMin G (v 0) (v m) := by
  have hne : v 0 ≠ v m := fun h => by have := hinj 0 (by omega) m (by omega) h; omega
  have hconsec : ∀ k, k < m → v k ≠ v (k + 1) := fun k hk h => by
    have := hinj k (by omega) (k + 1) (by omega) h; omega
  have hsupp : ∀ i j, G.weight i j = 0 → segFlow v m i j = 0 := by
    intro i j hw
    unfold segFlow
    exact Finset.sum_eq_zero (fun k hk => by
      rw [Finset.mem_range] at hk
      exact ep_zero_of_weight_zero G (hconsec k hk) (hedge k hk) i j hw)
  have hdiva : divF (segFlow v m) (v 0) = 1 := by
    rw [segFlow_divF v m hconsec (v 0), if_pos rfl, if_neg hne]; ring
  have hdiv0 : ∀ i, i ≠ v 0 → i ≠ v m → divF (segFlow v m) i = 0 := by
    intro i hi0 him
    rw [segFlow_divF v m hconsec i, if_neg hi0, if_neg him]; ring
  have hEpos : 0 < flowEnergy (segFlow v m) := by
    rw [segFlow_energy v m hinj]; exact_mod_cast hm
  have hbound := pairMin_ge_inv_flowEnergy G hw01 hne (segFlow v m) (segFlow_antisym v m)
    hsupp hdiva hdiv0 hEpos
  rw [segFlow_energy v m hinj] at hbound
  exact hbound
THEOREM pairMin_box_axial_ge_inv · IndisputableMonolith/Foundation/PairKernelLattice3.lean
pairMin_box_axial_ge_inv · IndisputableMonolith/Foundation/PairKernelLattice3.lean:1333 
/-- **Axial single-path bound on the D=3 box.** For `0 < r < L`, the straight axial walk of length
    `r` gives `pairMin (boxWeight L) 0 (r·e₁) ≥ 1/r`. This is the flow-side lower bound on the box
    (reproducing the 1D rate); the parallel-tube flow beats it. -/
theorem pairMin_box_axial_ge_inv {L r : ℕ} (hr : r < L) (hr0 : 0 < r) :
    (1:ℝ) / r ≤ pairMin (boxWeight L)
      (enc3 L ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩))
      (enc3 L ((⟨r, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)) := by
  have hL : 0 < L := by omega
  set v : ℕ → Fin (L * L * L) :=
    fun k => enc3 L ((⟨k % L, Nat.mod_lt k hL⟩, ⟨0, hL⟩), ⟨0, hL⟩) with hv
  have hw01 : ∀ i j, (boxWeight L).weight i j = 0 ∨ (boxWeight L).weight i j = 1 := by
    intro i j
    show (if dist3 ((enc3 L).symm i) ((enc3 L).symm j) ≤ 1 then (1:ℝ) else 0) = 0
        ∨ (if dist3 ((enc3 L).symm i) ((enc3 L).symm j) ≤ 1 then (1:ℝ) else 0) = 1
    split_ifs
    · exact Or.inr rfl
    · exact Or.inl rfl
  have hinj : ∀ i ≤ r, ∀ j ≤ r, v i = v j → i = j := by
    intro i hi j hj h
    have h2 := (enc3 L).injective h
    simp only [Prod.mk.injEq, Fin.mk.injEq] at h2
    have := h2.1.1
    rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at this
    exact this
  have hedge : ∀ k, k < r → (boxWeight L).weight (v k) (v (k + 1)) = 1 := by
    intro k hk
    simp only [hv]
    rw [boxWeight_enc, if_pos]
    show dist3 ((⟨k % L, Nat.mod_lt k hL⟩, (⟨0, hL⟩ : Fin L)), (⟨0, hL⟩ : Fin L))
        ((⟨(k + 1) % L, Nat.mod_lt (k + 1) hL⟩, (⟨0, hL⟩ : Fin L)), (⟨0, hL⟩ : Fin L)) ≤ 1
    show Nat.dist (k % L) ((k + 1) % L) + Nat.dist 0 0 + Nat.dist 0 0 ≤ 1
    rw [Nat.mod_eq_of_lt (by omega : k < L), Nat.mod_eq_of_lt (by omega : k + 1 < L)]
    simp only [Nat.dist_self, Nat.add_zero]
    show Nat.dist k (k + 1) ≤ 1
    unfold Nat.dist; omega
  have h0 : v 0 = enc3 L ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) := by
    simp only [hv]
    apply congrArg
    simp only [Prod.mk.injEq, Fin.mk.injEq]
    exact ⟨⟨Nat.zero_mod L, trivial⟩, trivial⟩
  have hrr : v r = enc3 L ((⟨r, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) := by
    simp only [hv]
    apply congrArg
    simp only [Prod.mk.injEq, Fin.mk.injEq]
    exact ⟨⟨Nat.mod_eq_of_lt hr, trivial⟩, trivial⟩
  rw [← h0, ← hrr]
  exact pairMin_ge_inv_pathLength (boxWeight L) hw01 v r hr0 hinj hedge
THEOREM pairMin_box_two_route_ge · IndisputableMonolith/Foundation/PairKernelLattice3.lean
pairMin_box_two_route_ge · IndisputableMonolith/Foundation/PairKernelLattice3.lean:1514 
/-- **The strict dichotomy at every distance on the D=3 box.** For `0 < r < L`, the axial pair
    `(0,0,0)`, `(r,0,0)` has `pairMin (boxWeight L) ≥ 2/(r+1)`, certified by the ½:½ current over
    the straight axial route (length `r`) and the edge-disjoint `y`-detour
    `(0,0,0) → (0,1,0) → (1,1,0) → ⋯ → (r,1,0) → (r,0,0)` (length `r+2`). Since the proved 1D
    ceiling is `pairMin ≤ 1/d` (`pairMin_band_le_inv_dist`) and `2/(r+1) > 1/r` for all `r ≥ 2`,
    the 1D decay law FAILS on the box at every separation: the second dimension strictly lowers the
    pair resistance everywhere, not just at distance 2. (The `r`-independent lower bound — full
    transience — still needs the radial shell flow; this is the every-distance strict witness.) -/
theorem pairMin_box_two_route_ge {L r : ℕ} (hr : r < L) (hr0 : 0 < r) :
    (2:ℝ) / (r + 1) ≤ pairMin (boxWeight L)
      (enc3 L ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩))
      (enc3 L ((⟨r, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)) := by
  have hL : 0 < L := by omega
  have hx2lt : ∀ k : ℕ, (if k = 0 then 0 else if k ≤ r + 1 then k - 1 else r) < L := by
    intro k; split_ifs <;> omega
  have hy2lt : ∀ k : ℕ, (if k = 0 then 0 else if k ≤ r + 1 then 1 else 0) < L := by
    intro k; split_ifs <;> omega
  set v₁ : ℕ → Fin (L * L * L) :=
    fun k => enc3 L ((⟨k % L, Nat.mod_lt k hL⟩, ⟨0, hL⟩), ⟨0, hL⟩) with hv₁
  set v₂ : ℕ → Fin (L * L * L) :=
    fun k => enc3 L ((⟨_, hx2lt k⟩, ⟨_, hy2lt k⟩), ⟨0, hL⟩) with hv₂
  have hw01 : ∀ i j, (boxWeight L).weight i j = 0 ∨ (boxWeight L).weight i j = 1 := by
    intro i j
    show (if dist3 ((enc3 L).symm i) ((enc3 L).symm j) ≤ 1 then (1:ℝ) else 0) = 0
        ∨ (if dist3 ((enc3 L).symm i) ((enc3 L).symm j) ≤ 1 then (1:ℝ) else 0) = 1
    split_ifs
    · exact Or.inr rfl
    · exact Or.inl rfl
  have hinj₁ : ∀ i ≤ r, ∀ j ≤ r, v₁ i = v₁ j → i = j := by
    intro i hi j hj h
    simp only [hv₁] at h
    obtain ⟨hx, -, -⟩ := enc3_mk_inj h
    rw [Nat.mod_eq_of_lt (by omega), Nat.mod_eq_of_lt (by omega)] at hx
    exact hx
  have hinj₂ : ∀ i ≤ r + 2, ∀ j ≤ r + 2, v₂ i = v₂ j → i = j := by
    intro i hi j hj h
    simp only [hv₂] at h
    obtain ⟨hx, hy, -⟩ := enc3_mk_inj h
    split_ifs at hx hy <;> omega
  have hedge₁ : ∀ k, k < r → (boxWeight L).weight (v₁ k) (v₁ (k + 1)) = 1 := by
    intro k hk
    simp only [hv₁]
    apply boxWeight_mk_one
    rw [Nat.mod_eq_of_lt (by omega : k < L), Nat.mod_eq_of_lt (by omega : k + 1 < L)]
    unfold Nat.dist
    omega
  have hedge₂ : ∀ k, k < r + 2 → (boxWeight L).weight (v₂ k) (v₂ (k + 1)) = 1 := by
    intro k hk
    simp only [hv₂]
    apply boxWeight_mk_one
    unfold Nat.dist
    split_ifs <;> first | contradiction | omega
  have h0 : v₂ 0 = v₁ 0 := by
    simp only [hv₁, hv₂]
    apply congrArg
    simp only [Prod.mk.injEq, Fin.mk.injEq]
    exact ⟨⟨by rw [if_true, Nat.zero_mod], by rw [if_true]⟩, trivial⟩
  have hm : v₂ (r + 2) = v₁ r := by
    simp only [hv₁, hv₂]
    apply congrArg
    simp only [Prod.mk.injEq, Fin.mk.injEq]
    refine ⟨⟨?_, ?_⟩, trivial⟩
    · rw [if_neg (by omega : ¬(r + 2 = 0)), if_neg (by omega : ¬(r + 2 ≤ r + 1)),
          Nat.mod_eq_of_lt hr]
    · rw [if_neg (by omega : ¬(r + 2 = 0)), if_neg (by omega : ¬(r + 2 ≤ r + 1))]
  have hdisj : ∀ k, k < r → ∀ k', k' < r + 2 →
      ¬(v₁ k = v₂ k' ∧ v₁ (k + 1) = v₂ (k' + 1))
      ∧ ¬(v₁ k = v₂ (k' + 1) ∧ v₁ (k + 1) = v₂ k') := by
    intro k hk k' hk'
    constructor
    · rintro ⟨h1, h2⟩
      simp only [hv₁, hv₂] at h1 h2
      obtain ⟨hx1, hy1, -⟩ := enc3_mk_inj h1
      obtain ⟨hx2, hy2, -⟩ := enc3_mk_inj h2
      rw [Nat.mod_eq_of_lt (by omega)] at hx1
      rw [Nat.mod_eq_of_lt (by omega)] at hx2
      split_ifs at hx1 hy1 hx2 hy2 <;> first | contradiction | omega
    · rintro ⟨h1, h2⟩
      simp only [hv₁, hv₂] at h1 h2
      obtain ⟨hx1, hy1, -⟩ := enc3_mk_inj h1
      obtain ⟨hx2, hy2, -⟩ := enc3_mk_inj h2
      rw [Nat.mod_eq_of_lt (by omega)] at hx1
      rw [Nat.mod_eq_of_lt (by omega)] at hx2
      split_ifs at hx1 hy1 hx2 hy2 <;> first | contradiction | omega
  have hgen := pairMin_ge_via_two_disjoint_walks (boxWeight L) hw01 v₁ v₂ r (r + 2) hr0
    hinj₁ hinj₂ hedge₁ hedge₂ h0 hm hdisj
  push_cast at hgen
  have h0v : v₁ 0 = enc3 L ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) := by
    simp only [hv₁]
    apply congrArg
    simp only [Prod.mk.injEq, Fin.mk.injEq]
    exact ⟨⟨Nat.zero_mod L, trivial⟩, trivial⟩
  have hrv : v₁ r = enc3 L ((⟨r, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) := by
    simp only [hv₁]
    apply congrArg
    simp only [Prod.mk.injEq, Fin.mk.injEq]
    exact ⟨⟨Nat.mod_eq_of_lt hr, trivial⟩, trivial⟩
  have hcast : (2:ℝ) / ((r:ℝ) + 1) = 4 / ((r:ℝ) + ((r:ℝ) + 2)) := by
    rw [div_eq_div_iff (by positivity) (by positivity)]
    ring
  rw [hcast, ← h0v, ← hrv]
  exact hgen

What this page does not claim

The theorem does not claim the bound is tight; it gives only a lower bound. The theorem does not claim anything about continuous space or the Coulomb 1/(4πr) law. The theorem does not claim the minimum cost saturates in three dimensions; that is a separate result.

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