IndisputableMonolith.Foundation.PairKernelOnsiteExclusion
IndisputableMonolith/Foundation/PairKernelOnsiteExclusion.lean · 282 lines · 14 declarations
show as:
view math explainer →
1import Mathlib.Data.Real.Basic
2import Mathlib.Analysis.SpecialFunctions.Exp
3import Mathlib.Analysis.SpecialFunctions.Log.Basic
4import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
5import IndisputableMonolith.Cost
6import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
7import IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
8import IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge
9
10/-!
11# Door 2 / L1-hard: onsite-term exclusion from shift invariance
12
13Pair-kernel provenance lane (`glm/fold_derivation_logs/pairwise_kernel_derive.md`).
14L2 (`recognition_fold/screening_law/l2_hessian_dispersion.py`) measured the exact-`J`
15Hessian's dispersion on a `4³ × 8` lattice and found it gapless and second-order, but
16that test **assumed** the cost is a pure function of link/posting differences (no
17on-site term). `exactJCostAction` is *defined* difference-only, so proving its shift
18invariance is a null test (a one-line tautology; it provides zero evidence RS forbids
19an on-site term, since we simply chose not to write one).
20
21This module supplies the genuine, non-vacuous obligation: quantify over a class of
22candidate ledger costs wide enough to *express* an on-site term, and prove that term is
23forced constant by a genuine hypothesis (`ShiftInvariant`), not by construction.
24
25## Panel verdict (2026-07-07, `door2_L1_provenance` panel, judge Fable xhigh)
26
27The panel's decisive finding (Director 3's mean-field counterexample, kept as
28`meanFieldLedgerCost` below) is that **shift invariance alone is necessary but NOT
29sufficient** to exclude a screened (Yukawa-like) kernel: an admissible, shift-invariant,
30purely difference-only cost can still carry an *all-to-all* (spatially non-local)
31weight structure that produces a mass gap away from `k = 0`. Excluding that requires a
32**separate** locality hypothesis (`L0`, finite-range weights), which is not addressed
33here and is not yet anywhere in the Lean surface. `l1_onsite_forced_constant` below is
34exactly the `L1` half of the panel's package (on-site exclusion); it does **not** by
35itself decide `1/r` vs. Yukawa screening, only the on-site-mass branch of that question.
36
37## Scoped verdict (`inference-discipline.mdc` form)
38
39- CLAIM: for a `GeneralLedgerCost` (onsite term FREE, link term a pure function of
40 posting differences, over any admissible weighted graph), global shift invariance of
41 the total cost forces the onsite term to be a constant function of its argument.
42- DOMAIN: any finite carrier `Fin n`, `n ≥ 1`; any nonneg-symmetric weight graph; any
43 `link : ℝ → ℝ`.
44- PREMISES: `ShiftInvariant C` (R1) [**HYPOTHESIS**. The 2026-07-07 `MP ⇒ Axiom R` canon audit
45 resolved its provenance: it is NOT forced by the Meta-Principle. Canonical MP is
46 `Recognition.MP := ¬∃ _ : Recognize Nothing Nothing, True` (`Empty` is uninhabited); it rejects only
47 the uninhabited `Nothing`, so it cannot reject an inhabited frozen anchor (the value-0 vacuum an
48 on-site mass term prices against). The `MP ⇒ Axiom R` live bet is CLOSED NEGATIVE. What the canon
49 actually has is ratio-only cost primitives with no on-site slot: `LedgerForcing.event_cost e =
50 J e.ratio` (`reciprocity`, `conservation_from_balance` proved) and
51 `ConstraintForcing.RecognitionLogCost A B = (log A − log B)²` (`recognition_exchange_invariance_axiom`,
52 `recognition_identity_axiom` proved). So `ShiftInvariant` holds definitionally on that ratio-carrier;
53 on the `Recognition.Ledger` debit/credit carrier mirrored here (where an on-site slot IS expressible)
54 its honest tier is MODEL-forced (definitional: a recognition is a two-party ratio), not MP-THEOREM.
55 It stays a named, load-bearing assumption of this theorem]; `0 < n` [trivial].
56- REACH: max licensed → "IF the ledger cost is admissible-shift-invariant, THEN no
57 on-site mass term is writable, which is exactly what the L2 decoy `+m² Σ φᵢ²` violates
58 and what the numeric harness correctly flagged Yukawa." Does NOT license → exclusion of
59 *non-local* (all-to-all / mean-field) screening (`meanFieldLedgerCost` below is an
60 explicit admissible counterexample to that stronger claim), nor any claim about
61 `5/8`, `5/16`, `27/16`, `Z_eff`, or the hydrogenic `F(r)` carrier (none appear here).
62
63Zero `sorry`. Zero new `axiom`.
64-/
65
66namespace IndisputableMonolith
67namespace Foundation
68namespace PairKernelOnsiteExclusion
69
70open SimplicialLedger.ContinuumBridge
71open SimplicialLedger.EdgeLengthFromPsi
72open SimplicialLedger.NonlinearBridge
73
74noncomputable section
75
76/-! ## §1. The candidate class: onsite term is FREE
77
78This is the anti-cheat. `exactJCostAction` has no on-site slot at all, so no proof about
79it can typecheck against the theorem below. `GeneralLedgerCost.onsite` is an arbitrary
80`ℝ → ℝ`; the theorem must rule out its non-constant instances by hypothesis, not by the
81shape of the definition. -/
82
83/-- A general ledger cost on `n` log-potential carriers: a (possibly nonzero) absolute
84 per-site term `onsite`, plus a per-link term `link` evaluated on posting differences
85 over an admissible weighted graph. `onsite` is a genuinely free parameter — nothing
86 in this structure forces it to vanish or to be constant; that is exactly the content
87 the forcing theorem below must supply from an extra hypothesis. -/
88structure GeneralLedgerCost (n : ℕ) where
89 /-- The underlying admissible (nonneg, symmetric) weighted ledger graph. -/
90 G : WeightedLedgerGraph n
91 /-- The absolute per-site cost term (the thing whose admissibility is in question). -/
92 onsite : ℝ → ℝ
93 /-- The per-link (posting-difference) cost term. -/
94 link : ℝ → ℝ
95
96/-- The total cost of a log-potential assignment under a general ledger cost:
97 `Σᵢ onsite(εᵢ) + Σᵢⱼ wᵢⱼ · link(εᵢ − εⱼ)`. -/
98def GeneralLedgerCost.eval {n : ℕ} (C : GeneralLedgerCost n) (ε : LogPotential n) : ℝ :=
99 (∑ i : Fin n, C.onsite (ε i)) +
100 ∑ i : Fin n, ∑ j : Fin n, C.G.weight i j * C.link (ε i - ε j)
101
102/-- **R1 (global shift invariance).** Adding an arbitrary constant to every log-potential
103 leaves the total ledger cost unchanged. This is the candidate double-entry gauge
104 symmetry under investigation: absolute account *levels* carry no cost, only the
105 *relations* between them do. It is stated here as a named hypothesis, not derived. -/
106def ShiftInvariant {n : ℕ} (C : GeneralLedgerCost n) : Prop :=
107 ∀ (ε : LogPotential n) (c : ℝ), C.eval (fun i => ε i + c) = C.eval ε
108
109/-! ## §2. The link term is automatically shift-invariant (this is the null test to reject
110 as a standalone deliverable — it carries zero content about the onsite term). -/
111
112/-- The link (difference-only) part of `eval` never changes under a global shift, for
113 *any* `link` function and *any* weight graph — a pure consequence of the fact that
114 `(εᵢ + c) − (εⱼ + c) = εᵢ − εⱼ`. This is the tautological half of `ShiftInvariant`;
115 it is exactly what makes `exactJCostAction`'s own shift invariance a null test (it
116 has no onsite slot, so it only ever exercises this half). -/
117theorem link_part_shift_invariant {n : ℕ} (C : GeneralLedgerCost n)
118 (ε : LogPotential n) (c : ℝ) :
119 (∑ i : Fin n, ∑ j : Fin n, C.G.weight i j * C.link ((ε i + c) - (ε j + c)))
120 = ∑ i : Fin n, ∑ j : Fin n, C.G.weight i j * C.link (ε i - ε j) := by
121 apply Finset.sum_congr rfl
122 intro i _
123 apply Finset.sum_congr rfl
124 intro j _
125 have : (ε i + c) - (ε j + c) = ε i - ε j := by ring
126 rw [this]
127
128/-- Consequently, `ShiftInvariant C` is *equivalent* to the onsite sum alone being
129 shift-invariant. This isolates exactly the non-vacuous content: `ShiftInvariant`
130 only has teeth against the onsite term, never against `link`. -/
131theorem shiftInvariant_iff_onsite_sum {n : ℕ} (C : GeneralLedgerCost n) :
132 ShiftInvariant C ↔
133 ∀ (ε : LogPotential n) (c : ℝ),
134 (∑ i : Fin n, C.onsite (ε i + c)) = ∑ i : Fin n, C.onsite (ε i) := by
135 constructor
136 · intro hR1 ε c
137 have h := hR1 ε c
138 unfold GeneralLedgerCost.eval at h
139 rw [link_part_shift_invariant C ε c] at h
140 linarith
141 · intro honsite ε c
142 unfold GeneralLedgerCost.eval
143 rw [link_part_shift_invariant C ε c, honsite ε c]
144
145/-! ## §3. L1-FORCE: the non-vacuous target -/
146
147/-- **L1-FORCE (`l1_onsite_forced_constant`).** Under `ShiftInvariant` and `n ≥ 1`, the
148 onsite part of an admissible `GeneralLedgerCost` is forced to be a constant
149 function of its real argument — i.e. no on-site mass/absolute term is writable.
150
151 Non-vacuity: this is FALSE without `ShiftInvariant`. Take `onsite u = u²` (the exact
152 shape of the L2 decoy `+m² Σ φᵢ²`, which the numeric harness correctly flagged
153 Yukawa): `yukawaOnsiteDecoy_not_shift_invariant` below shows this instance fails
154 the hypothesis, so deleting `hR1` lets it stand as a live counterexample to the
155 conclusion. -/
156theorem l1_onsite_forced_constant {n : ℕ} (C : GeneralLedgerCost n) (hn : 0 < n)
157 (hR1 : ShiftInvariant C) :
158 ∃ k : ℝ, ∀ u : ℝ, C.onsite u = k := by
159 refine ⟨C.onsite 0, fun u => ?_⟩
160 have honsite := (shiftInvariant_iff_onsite_sum C).mp hR1 (fun _ => (0 : ℝ)) u
161 simp only [zero_add] at honsite
162 have hL : (∑ _i : Fin n, C.onsite u) = (n : ℝ) * C.onsite u := by
163 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
164 have hR : (∑ _i : Fin n, C.onsite 0) = (n : ℝ) * C.onsite 0 := by
165 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
166 rw [hL, hR] at honsite
167 have hnr : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
168 exact mul_left_cancel₀ hnr honsite
169
170/-! ## §4. Decoy 1 (R1 fails): the on-site mass term, byte-for-byte the L2 decoy -/
171
172/-- The decoy on-site "mass" cost, `onsite u = u²`, `link ≡ 0` — the exact shape of the
173 `+m² Σ φᵢ²` operator the L2 Python harness flagged `DEAD_YUKAWA`. It is a perfectly
174 well-formed `GeneralLedgerCost` (the structure does not forbid it), which is the
175 point: nothing rules it out except a genuine hypothesis. -/
176def yukawaOnsiteDecoy {n : ℕ} (G : WeightedLedgerGraph n) : GeneralLedgerCost n where
177 G := G
178 onsite := fun u => u ^ 2
179 link := fun _ => 0
180
181/-- **Anti-cheat witness.** The on-site mass decoy does NOT satisfy `ShiftInvariant`
182 (for `n ≥ 1`): shifting the flat vacuum by `1` changes the total cost from `0` to
183 `n`. So `ShiftInvariant` is genuinely load-bearing — the theorem above has teeth,
184 and is not a restatement of something already true of every `GeneralLedgerCost`. -/
185theorem yukawaOnsiteDecoy_not_shift_invariant {n : ℕ} (G : WeightedLedgerGraph n)
186 (hn : 0 < n) :
187 ¬ ShiftInvariant (yukawaOnsiteDecoy G) := by
188 intro hR1
189 have h := (shiftInvariant_iff_onsite_sum (yukawaOnsiteDecoy G)).mp hR1 (fun _ => (0 : ℝ)) 1
190 simp only [yukawaOnsiteDecoy, zero_add] at h
191 have hL : (∑ _i : Fin n, (1 : ℝ) ^ 2) = (n : ℝ) := by
192 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
193 ring
194 have hR : (∑ _i : Fin n, (0 : ℝ) ^ 2) = (0 : ℝ) := by simp
195 rw [hL, hR] at h
196 exact (Nat.cast_ne_zero.mpr hn.ne') h
197
198/-! ## §5. Witness 2 (the honest negative): admissible + shift-invariant does not imply
199 locality. `ShiftInvariant` alone is necessary but NOT sufficient to exclude a
200 screened kernel; the panel's mean-field counterexample lands here, formalized as an
201 explicit non-local instance that is admissible and trivially shift-invariant. -/
202
203/-- The **mean-field / all-to-all** weight graph: uniform coupling `1` between *every*
204 pair of sites, including maximally separated ones. This is a perfectly admissible
205 `WeightedLedgerGraph` (nonnegative, symmetric) — nothing in the graph axioms demands
206 finite range. -/
207def meanFieldWeight (n : ℕ) : WeightedLedgerGraph n where
208 weight := fun _ _ => 1
209 weight_nonneg := fun _ _ => zero_le_one
210 weight_symm := fun _ _ => rfl
211
212/-- The mean-field weight has full support: every pair, including every distinct pair,
213 is coupled with nonzero weight. This is the formal shape of "not finite-range" — a
214 genuinely local weight graph must vanish outside a bounded neighborhood as `n`
215 grows, and this one never does. -/
216theorem meanFieldWeight_full_support (n : ℕ) (i j : Fin n) :
217 (meanFieldWeight n).weight i j ≠ 0 := by
218 simp [meanFieldWeight]
219
220/-- The mean-field ledger cost: NO on-site term at all (`onsite ≡ 0`, so it trivially
221 satisfies the conclusion of `l1_onsite_forced_constant` with `k = 0`), link term a
222 plain quadratic, and the non-local mean-field weight graph. -/
223def meanFieldLedgerCost (n : ℕ) : GeneralLedgerCost n where
224 G := meanFieldWeight n
225 onsite := fun _ => 0
226 link := fun u => u ^ 2
227
228/-- **The honest negative.** The mean-field ledger cost is shift-invariant (it has no
229 onsite term, so `ShiftInvariant` holds for the shape reason isolated in
230 `shiftInvariant_iff_onsite_sum`, not because locality was ever assumed), yet its
231 weight graph is non-local (`meanFieldWeight_full_support`). So `L1`
232 (`l1_onsite_forced_constant`), even fully proved and even fully forced from
233 first principles, does NOT by itself exclude a screened kernel: excluding the
234 mean-field / all-to-all route needs a SEPARATE locality hypothesis `L0`
235 (finite-range weights), which is not addressed in this module and, per the panel
236 audit, is currently nowhere in the Lean surface. This is the scoped, honest residual
237 of Door 2 / L1-hard: on-site exclusion is real and forced (conditional on
238 `ShiftInvariant`), but on-site exclusion alone is not the whole story. -/
239theorem meanFieldLedgerCost_shift_invariant (n : ℕ) :
240 ShiftInvariant (meanFieldLedgerCost n) := by
241 rw [shiftInvariant_iff_onsite_sum]
242 intro ε c
243 simp [meanFieldLedgerCost]
244
245/-! ## §6. Positive control: `exactJCostAction` sits in the `onsite ≡ 0` slice
246
247This connects the abstract exclusion theorem back to the real RS Lean object cited in
248the Door 2 log. It is explicitly NOT the forcing result — proving `exactJCostAction`'s
249own shift invariance directly (skipping `GeneralLedgerCost` entirely) is exactly the
250null test the panel and the Door 2 log both flag and reject; it is recorded here only as
251a consistency anchor, and the anti-cheat is that `l1_onsite_forced_constant` never
252unfolds `exactJCostAction` at all. -/
253
254/-- `exactJCostAction` re-expressed as a `GeneralLedgerCost` with the onsite slot
255 identically the zero function — RS's actual cost primitive has never carried a
256 writable onsite term in the first place. -/
257def exactJCostAsGeneralLedgerCost {n : ℕ} (G : WeightedLedgerGraph n) : GeneralLedgerCost n where
258 G := G
259 onsite := fun _ => 0
260 link := fun u => Real.cosh u - 1
261
262/-- The re-expression agrees with `exactJCostAction` exactly. -/
263theorem exactJCostAsGeneralLedgerCost_eval {n : ℕ} (G : WeightedLedgerGraph n)
264 (ε : LogPotential n) :
265 (exactJCostAsGeneralLedgerCost G).eval ε = exactJCostAction G ε := by
266 unfold GeneralLedgerCost.eval exactJCostAsGeneralLedgerCost exactJCostAction
267 simp
268
269/-- Sanity corollary: applying the general forcing theorem to the `exactJCostAction`
270 slice recovers `k = 0` (the onsite term was already zero, not merely forced to be
271 some unknown constant). Consistency check, not new content. -/
272theorem exactJCostAsGeneralLedgerCost_onsite_zero {n : ℕ} (G : WeightedLedgerGraph n)
273 (_hn : 0 < n) :
274 ∃ k : ℝ, k = 0 ∧ ∀ u : ℝ, (exactJCostAsGeneralLedgerCost G).onsite u = k := by
275 refine ⟨0, rfl, fun u => rfl⟩
276
277end
278
279end PairKernelOnsiteExclusion
280end Foundation
281end IndisputableMonolith
282