Encyclopedia Foundation Foundation Pair Kernel Lattice3 Wpair Box Adjacent Ge One
ARTICLE 3 claims 2 theorems 1 open
Foundation Pair Kernel Lattice3 Wpair Box Adjacent Ge One
A machine-checked theorem shows that in a three-dimensional lattice, two neighboring sites always carry a recognition cost of at least one.
The three-dimensional box
In the Recognition Science framework, a ledger is a discrete record of events, and each event carries a forced cost. The declaration Wpair_box_adjacent_ge_one is a proved theorem about a specific kind of ledger: a three-dimensional box of sites, where each site connects to its six nearest neighbors. The theorem states that for any two adjacent sites in this box, the minimal recognition cost between them is at least one. This is not a numerical coincidence; it is a consequence of the graph structure itself, verified by a machine-checked library of formal theorems.
The box is built as an L by L by L grid of sites. A metric called the taxicab distance measures how many steps apart two sites are, moving only along the grid lines. Two sites are adjacent when this distance is exactly one. The theorem applies to this adjacency: the cost is always at least one. This result is transported from a more general theorem about any graph with weights of zero or one, where an edge of weight one forces the cost to be at least one. The three-dimensional box is a special case, and the theorem shows that its structure is rich enough to support this non-vacuous cost.
This result matters because it is a concrete step toward understanding how two-body interactions emerge from the ledger. In one dimension, the cost between two sites decays as one over the distance, approaching zero. In three dimensions, the situation is different: the cost saturates at a positive constant, a difference rooted in the random walk behavior of the lattice. The theorem Wpair_box_adjacent_ge_one is the first link in this three-dimensional story, showing that the box carrier is not empty but has genuine structure.
What the theorem does not claim is equally important. It does not establish the full three-dimensional Green's function, the source-coupled interaction that decays as one over four pi times the distance. That remains an open target. It also does not prove the dimension dichotomy, the structural theorem that would show the box energy collapses to three axis-sums. The theorem is a single, precise fact about adjacent sites, not a complete theory of three-dimensional recognition.
THEOREM Wpair_box_adjacent_ge_one · IndisputableMonolith/Foundation/PairKernelLattice3.lean
/-- **The pinned-pair kernel is non-vacuous on the D=3 box.** An ℓ¹-adjacent pair costs `≥ 1`. This
transports for free from L3's graph-generic `pairMin_ge_weight`, and is the concrete link from
the D=3 carrier back to the Door 2 two-body cost `Wpair`. -/
theorem Wpair_box_adjacent_ge_one {L : ℕ} (hL : 2 ≤ L) :
(1:ℝ) ≤ Wpair (boxWeight L)
(enc3 L ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩))
(enc3 L ((⟨1, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)) := by
rw [Wpair_eq_pairMin]
set o : Site3 L := ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) with ho
set e : Site3 L := ((⟨1, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) with he
have hne : enc3 L o ≠ enc3 L e := by
intro h
have h2 := (enc3 L).injective h
rw [ho, he] at h2
simp only [Prod.mk.injEq, Fin.mk.injEq] at h2
omega
have hw : (boxWeight L).weight (enc3 L o) (enc3 L e) = 1 := by
rw [boxWeight_enc, if_pos]
rw [ho, he]
simp only [dist3, Nat.dist]
decide
calc (1:ℝ) = (boxWeight L).weight (enc3 L o) (enc3 L e) := hw.symm
_ ≤ pairMin (boxWeight L) (enc3 L o) (enc3 L e) := pairMin_ge_weight (boxWeight L) hne
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 prove the full Green's function asymptotics, which remain open. The theorem does not establish the dimension dichotomy for the box energy. The theorem does not apply to non-adjacent sites.
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 structure theorem for the box Dirichlet energy?
- How does the three-dimensional Green's function emerge from the source-coupled formulation?
- What is the precise relationship between the random walk transience and the saturation of the cost?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM Wpair_box_adjacent_ge_one · IndisputableMonolith/Foundation/PairKernelLattice3.lean
/-- **The pinned-pair kernel is non-vacuous on the D=3 box.** An ℓ¹-adjacent pair costs `≥ 1`. This transports for free from L3's graph-generic `pairMin_ge_weight`, and is the concrete link from the D=3 carrier back to the Door 2 two-body cost `Wpair`. -/ theorem Wpair_box_adjacent_ge_one {L : ℕ} (hL : 2 ≤ L) : (1:ℝ) ≤ Wpair (boxWeight L) (enc3 L ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)) (enc3 L ((⟨1, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩)) := by rw [Wpair_eq_pairMin] set o : Site3 L := ((⟨0, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) with ho set e : Site3 L := ((⟨1, by omega⟩, ⟨0, by omega⟩), ⟨0, by omega⟩) with he have hne : enc3 L o ≠ enc3 L e := by intro h have h2 := (enc3 L).injective h rw [ho, he] at h2 simp only [Prod.mk.injEq, Fin.mk.injEq] at h2 omega have hw : (boxWeight L).weight (enc3 L o) (enc3 L e) = 1 := by rw [boxWeight_enc, if_pos] rw [ho, he] simp only [dist3, Nat.dist] decide calc (1:ℝ) = (boxWeight L).weight (enc3 L o) (enc3 L e) := hw.symm _ ≤ pairMin (boxWeight L) (enc3 L o) (enc3 L e) := pairMin_ge_weight (boxWeight L) hneThe theorem states that for any two adjacent sites in this box, the minimal recognition cost between them is at least one. Wpair_box_adjacent_ge_one · IndisputableMonolith/Foundation/PairKernelLattice3.leanTHEOREM 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 hboundThis result is transported from a more general theorem about any graph with weights of zero or one, where an edge of weight one forces the cost to be at least one. pairMin_ge_one_via_edge_flow · IndisputableMonolith/Foundation/PairKernelLattice3.lean- OPENIt does not establish the full three-dimensional Green's function, the source-coupled interaction that decays as one over four pi times the distance.