IndisputableMonolith.Foundation.PairKernelLocality

   1import Mathlib
   2import IndisputableMonolith.Foundation.PairKernelOnsiteExclusion
   3
   4/-!
   5# Door 2 / L0: the finite-range (locality) hypothesis on the ledger weight graph
   6
   7Pair-kernel provenance lane (`glm/fold_derivation_logs/pairwise_kernel_derive.md`).
   8
   9## Why L0 is needed regardless of L1 / the bridge
  10
  11`PairKernelOnsiteExclusion` proved on-site-mass exclusion conditional on `ShiftInvariant`
  12(difference-only cost), and the bridge (`PairKernelRatioBridge`) closed the last route to
  13making `ShiftInvariant` a THEOREM (it is MODEL-forced, definitional). But even a
  14THEOREM-grade `ShiftInvariant` does NOT exclude a screened (Yukawa-like) kernel: the
  15panel's mean-field counterexample, formalized as `meanFieldLedgerCost`, is difference-only
  16and shift-invariant yet all-to-all coupled, and an all-to-all coupling produces a mass gap
  17away from `k = 0` (the `+μ` screening symbol; the dispersion analysis is MEASURED /
  18numerical in the L2 harness, not re-proved here). Excluding that route needs a SEPARATE
  19locality hypothesis: the weights must vanish beyond a fixed range.
  20
  21A canon scan (2026-07-07) found NO range/locality principle on `WeightedLedgerGraph`
  22anywhere in the Lean surface. `LocalityFromLedger.lean` proves a different locality (the
  23T5→T6 binary-recurrence adjacency between scale *levels*), not a range cutoff on the pair
  24weight kernel. So `L0` is genuinely un-formalized, and the honest move is to name it as an
  25explicit, discriminating **HYPOTHESIS** rather than rest silently on the `4³` lattice's
  26nearest-neighbor adjacency that the L2 harness happened to use.
  27
  28## What this module supplies (honest scope)
  29
  30- `FiniteRange G R`: the named locality hypothesis — the weight between two sites at
  31  index-distance `> R` is zero. This is the postulate; it is NOT derived here.
  32- **Teeth (`meanFieldLedgerCost_not_finiteRange`):** the mean-field graph that carries the
  33  built screening honest-negative violates `FiniteRange` at every fixed radius once the
  34  carrier is large enough. So `FiniteRange` is genuinely load-bearing — it rejects exactly
  35  the counterexample that survives L1.
  36- **Non-vacuity (`bandWeight_finiteRange` + admissibility):** a nearest-neighbor band graph
  37  is an admissible `WeightedLedgerGraph` that satisfies `FiniteRange 1`. So the hypothesis
  38  is not empty; some real cost satisfies it.
  39
  40This module does NOT prove "L0 ⇒ no screening" (that is the dispersion/Fourier step, MEASURED
  41in L2). It formalizes the hypothesis, proves it discriminates, and tags it HYPOTHESIS.
  42
  43## Scoped verdict (`inference-discipline.mdc` form)
  44
  45- CLAIM: `FiniteRange` is a non-vacuous, discriminating locality hypothesis on the ledger
  46  weight graph — satisfiable by a band graph, violated by the mean-field graph that carries
  47  the screening honest-negative.
  48- DOMAIN: `WeightedLedgerGraph` over `Fin n`; index-distance `Nat.dist i.val j.val`.
  49- PREMISES: none beyond the definitions (all statements proved).
  50- REACH: max licensed → "L0 is a real, load-bearing hypothesis, currently HYPOTHESIS-tier
  51  (postulated, not derived from a more primitive RS principle), that rejects the mean-field
  52  screening carrier and is satisfiable." Does NOT license → "L0 excludes screening" (that is
  53  the un-formalized dispersion step), nor "L0 is forced by RS" (its provenance — deriving a
  54  range cutoff from atomic-tick / recognition adjacency — is OPEN, expected-closure), nor any
  55  claim about `1/r` vs. Yukawa from primitives, nor any use of `5/8`, `5/16`, `27/16`,
  56  `Z_eff`, or hydrogenic `F(r)` (none appear here).
  57
  58Zero `sorry`. Zero new `axiom`.
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Foundation
  63namespace PairKernelLocality
  64
  65open SimplicialLedger.ContinuumBridge
  66open PairKernelOnsiteExclusion
  67
  68noncomputable section
  69
  70/-! ## §1. Index distance and the finite-range hypothesis -/
  71
  72/-- The index distance between two sites of a `Fin n` carrier: `|i − j|` via `Nat.dist`.
  73    This is a placeholder geometry for the abstract carrier; the point is only that it
  74    separates far-apart indices, which is all a range cutoff needs. -/
  75def cellDist {n : ℕ} (i j : Fin n) : ℕ := Nat.dist i.val j.val
  76
  77theorem cellDist_comm {n : ℕ} (i j : Fin n) : cellDist i j = cellDist j i := by
  78  simp only [cellDist, Nat.dist_comm]
  79
  80/-- **L0 (finite-range / locality hypothesis).** The weight between two sites more than `R`
  81    index-cells apart is zero: no coupling beyond a fixed range. This is the separate
  82    postulate `L1` / the bridge do not supply; it is stated as a named hypothesis, NOT
  83    derived from anything more primitive in the Lean surface today (its provenance is OPEN,
  84    expected-closure via the atomic-tick / recognition adjacency being nearest-neighbor). -/
  85def FiniteRange {n : ℕ} (G : WeightedLedgerGraph n) (R : ℕ) : Prop :=
  86  ∀ i j : Fin n, R < cellDist i j → G.weight i j = 0
  87
  88/-! ## §2. Teeth: the mean-field screening carrier is NOT finite-range
  89
  90`meanFieldWeight` (uniform all-to-all coupling `1`, the carrier of the built screening
  91honest-negative `meanFieldLedgerCost_shift_invariant`) violates `FiniteRange` at every
  92fixed radius `R` once `n ≥ R + 2`: sites `0` and `R+1` are `R+1 > R` cells apart yet still
  93coupled with weight `1`. So `FiniteRange` genuinely rejects the counterexample L1 could not
  94touch — it is load-bearing, not a null hypothesis. -/
  95
  96theorem meanFieldWeight_not_finiteRange (R n : ℕ) (hn : R + 2 ≤ n) :
  97    ¬ FiniteRange (meanFieldWeight n) R := by
  98  intro hFR
  99  have hi : (0 : ℕ) < n := by omega
 100  have hj : R + 1 < n := by omega
 101  have hrange : R < cellDist (⟨0, hi⟩ : Fin n) (⟨R + 1, hj⟩ : Fin n) := by
 102    show R < Nat.dist 0 (R + 1)
 103    unfold Nat.dist
 104    omega
 105  have h1 := hFR ⟨0, hi⟩ ⟨R + 1, hj⟩ hrange
 106  simp only [meanFieldWeight] at h1
 107  exact one_ne_zero h1
 108
 109/-- The same teeth, stated on the built honest-negative cost `meanFieldLedgerCost`: its
 110    weight graph (`meanFieldWeight`) is not finite-range. This is the direct link — L0 is
 111    exactly the hypothesis that rejects the screening carrier that survives L1. -/
 112theorem meanFieldLedgerCost_not_finiteRange (R n : ℕ) (hn : R + 2 ≤ n) :
 113    ¬ FiniteRange (meanFieldLedgerCost n).G R :=
 114  meanFieldWeight_not_finiteRange R n hn
 115
 116/-! ## §3. Non-vacuity: a nearest-neighbor band graph is admissible and finite-range -/
 117
 118/-- The nearest-neighbor **band** weight graph: coupling `1` between sites at most one cell
 119    apart, `0` otherwise. An admissible `WeightedLedgerGraph` (nonnegative, symmetric). -/
 120def bandWeight (n : ℕ) : WeightedLedgerGraph n where
 121  weight := fun i j => if cellDist i j ≤ 1 then 1 else 0
 122  weight_nonneg := fun i j => by
 123    show (0 : ℝ) ≤ if cellDist i j ≤ 1 then (1 : ℝ) else 0
 124    split <;> norm_num
 125  weight_symm := fun i j => by
 126    show (if cellDist i j ≤ 1 then (1 : ℝ) else 0) = if cellDist j i ≤ 1 then (1 : ℝ) else 0
 127    rw [cellDist_comm i j]
 128
 129/-- The band graph satisfies the locality hypothesis at radius `1`: nothing couples beyond
 130    one cell. So `FiniteRange` is not empty — a real admissible cost lives inside it. -/
 131theorem bandWeight_finiteRange (n : ℕ) : FiniteRange (bandWeight n) 1 := by
 132  intro i j hR
 133  simp only [bandWeight]
 134  exact if_neg (not_le.mpr hR)
 135
 136/-- Sanity: the band graph does couple adjacent sites (weight `1` on the nearest-neighbor
 137    pair `0,1`), so it is not the trivial diagonal graph — the witness carries real content. -/
 138theorem bandWeight_adjacent_coupled (n : ℕ) (hn : 2 ≤ n) :
 139    (bandWeight n).weight ⟨0, by omega⟩ ⟨1, by omega⟩ = 1 := by
 140  have hd : cellDist (⟨0, by omega⟩ : Fin n) (⟨1, by omega⟩ : Fin n) ≤ 1 := by
 141    show Nat.dist 0 1 ≤ 1
 142    unfold Nat.dist
 143    omega
 144  simp only [bandWeight]
 145  exact if_pos hd
 146
 147/-! ## §4. Bundle: `FiniteRange` is a genuine, discriminating hypothesis -/
 148
 149/-- **L0 status bundle.** `FiniteRange` is (a) satisfiable by an admissible non-trivial
 150    graph (the band graph, radius `1`), and (b) violated by the mean-field graph that
 151    carries the built screening honest-negative (at every fixed radius, for large enough
 152    carriers). A hypothesis with both properties is neither vacuous nor trivially true: it
 153    does real work. It remains HYPOTHESIS-tier — its RS provenance (a forced range cutoff)
 154    is OPEN. -/
 155theorem finiteRange_is_discriminating :
 156    (∀ n, FiniteRange (bandWeight n) 1) ∧
 157      (∀ R n, R + 2 ≤ n → ¬ FiniteRange (meanFieldWeight n) R) :=
 158  ⟨bandWeight_finiteRange, meanFieldWeight_not_finiteRange⟩
 159
 160end
 161
 162end PairKernelLocality
 163end Foundation
 164end IndisputableMonolith
 165