Foundation Pair Kernel Onsite Exclusion Exact Jcost As General Ledger Cost Onsit

/-- Sanity corollary: applying the general forcing theorem to the `exactJCostAction`
    slice recovers `k = 0` (the onsite term was already zero, not merely forced to be
    some unknown constant). Consistency check, not new content. -/
theorem exactJCostAsGeneralLedgerCost_onsite_zero {n : ℕ} (G : WeightedLedgerGraph n)
    (_hn : 0 < n) :
    ∃ k : ℝ, k = 0 ∧ ∀ u : ℝ, (exactJCostAsGeneralLedgerCost G).onsite u = k := by
  refine ⟨0, rfl, fun u => rfl⟩

/-- **L1-FORCE (`l1_onsite_forced_constant`).** Under `ShiftInvariant` and `n ≥ 1`, the
    onsite part of an admissible `GeneralLedgerCost` is forced to be a constant
    function of its real argument — i.e. no on-site mass/absolute term is writable.

    Non-vacuity: this is FALSE without `ShiftInvariant`. Take `onsite u = u²` (the exact
    shape of the L2 decoy `+m² Σ φᵢ²`, which the numeric harness correctly flagged
    Yukawa): `yukawaOnsiteDecoy_not_shift_invariant` below shows this instance fails
    the hypothesis, so deleting `hR1` lets it stand as a live counterexample to the
    conclusion. -/
theorem l1_onsite_forced_constant {n : ℕ} (C : GeneralLedgerCost n) (hn : 0 < n)
    (hR1 : ShiftInvariant C) :
    ∃ k : ℝ, ∀ u : ℝ, C.onsite u = k := by
  refine ⟨C.onsite 0, fun u => ?_⟩
  have honsite := (shiftInvariant_iff_onsite_sum C).mp hR1 (fun _ => (0 : ℝ)) u
  simp only [zero_add] at honsite
  have hL : (∑ _i : Fin n, C.onsite u) = (n : ℝ) * C.onsite u := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hR : (∑ _i : Fin n, C.onsite 0) = (n : ℝ) * C.onsite 0 := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  rw [hL, hR] at honsite
  have hnr : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  exact mul_left_cancel₀ hnr honsite

/-- **R1 (global shift invariance).** Adding an arbitrary constant to every log-potential
    leaves the total ledger cost unchanged. This is the candidate double-entry gauge
    symmetry under investigation: absolute account *levels* carry no cost, only the
    *relations* between them do. It is stated here as a named hypothesis, not derived. -/
def ShiftInvariant {n : ℕ} (C : GeneralLedgerCost n) : Prop :=
  ∀ (ε : LogPotential n) (c : ℝ), C.eval (fun i => ε i + c) = C.eval ε

/-- **The honest negative.** The mean-field ledger cost is shift-invariant (it has no
    onsite term, so `ShiftInvariant` holds for the shape reason isolated in
    `shiftInvariant_iff_onsite_sum`, not because locality was ever assumed), yet its
    weight graph is non-local (`meanFieldWeight_full_support`). So `L1`
    (`l1_onsite_forced_constant`), even fully proved and even fully forced from
    first principles, does NOT by itself exclude a screened kernel: excluding the
    mean-field / all-to-all route needs a SEPARATE locality hypothesis `L0`
    (finite-range weights), which is not addressed in this module and, per the panel
    audit, is currently nowhere in the Lean surface. This is the scoped, honest residual
    of Door 2 / L1-hard: on-site exclusion is real and forced (conditional on
    `ShiftInvariant`), but on-site exclusion alone is not the whole story. -/
theorem meanFieldLedgerCost_shift_invariant (n : ℕ) :
    ShiftInvariant (meanFieldLedgerCost n) := by
  rw [shiftInvariant_iff_onsite_sum]
  intro ε c
  simp [meanFieldLedgerCost]

/-- The mean-field weight has full support: every pair, including every distinct pair,
    is coupled with nonzero weight. This is the formal shape of "not finite-range" — a
    genuinely local weight graph must vanish outside a bounded neighborhood as `n`
    grows, and this one never does. -/
theorem meanFieldWeight_full_support (n : ℕ) (i j : Fin n) :
    (meanFieldWeight n).weight i j ≠ 0 := by
  simp [meanFieldWeight]