Encyclopedia Foundation Foundation Pair Kernel Lattice3 Box Action Eq Potential Drop Of Posting Source

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Lattice3 Box Action Eq Potential Drop Of Posting Source

A machine-checked library builds a three-dimensional lattice box and proves that its two-body cost does not decay with distance, a fact that depends on the dimension of space.

Verify this page

The three-dimensional carrier

The declaration box_action_eq_potential_drop_of_posting_source belongs to a family of results about a ledger, a discrete record of events and their costs. In this framework, a physical law emerges from the minimal cost of moving between two sites on a graph. The declaration in question establishes a specific fact about a three-dimensional lattice: a box of sites where each site connects to its six nearest neighbors.

The key result is that the minimal cost between two sites does not fall to zero as the distance grows. On a one-dimensional chain, the cost decays like one over the distance, which goes to zero. On the three-dimensional box, the cost saturates at a positive constant. This mirrors the classical distinction between a recurrent random walk, which returns to its start, and a transient one, which wanders off. The dimension of the space sets the qualitative behavior.

The declaration also proves a concrete lower bound: for two sites separated by a distance r along an axis, the cost is at least 2/(r+1). This is a theorem, checked by a machine, with no unproved assumptions. It is part of a larger effort to derive the three-dimensional Coulomb interaction, 1/(4πr), from the ledger picture.

What the declaration does not claim is that the minimal cost itself equals 1/(4πr). That formula describes the lattice Green's function, a different object, which is the response to a unit source. The Green's function asymptotics remain open. The cost saturation is the proved result; the Coulomb form is a target.

In plain terms, the declaration shows that the ledger's two-body cost behaves differently in three dimensions than in one. The cost does not vanish at large separation. This is a structural fact, not a numerical match to experiment.

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
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
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

What this page does not claim

The declaration does not prove that the minimal cost equals the Coulomb potential 1/(4πr). The declaration does not establish the Green's function asymptotics, which remain open. The declaration does not claim a numerical agreement with any measured physical quantity.

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