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

The cost re-expressed

The declaration exactJCostAsGeneralLedgerCost_eval is a consistency check, not a new discovery. It states that a particular cost function, called exactJCostAction, can be written in a general ledger form. A ledger, in this framework, is a discrete record of events where the cost of a configuration is a sum of two kinds of terms: a per-site term that depends on the value at a single site, and a per-link term that depends on the difference between values at two linked sites. The theorem proves that the exact cost function is identical to a ledger cost where the per-site term is always zero and the per-link term is the hyperbolic cosine of the difference minus one.

This re-expression matters because it clarifies what the cost function does and does not contain. The cost function, which the framework derives from five conditions on how recognition events are priced, turns out to have no absolute, per-site component. In physics language, this means there is no on-site mass term of the form a constant times the square of the field value at a point. The only costs arise from relations between sites, not from the value at any single site. This is a property of the specific cost function, not a general theorem about all possible costs.

The declaration itself is a simple equality. It does not prove that the cost function must have this form. It merely shows that the specific function, as defined, can be expressed in this way. The proof is a direct computation, unfolding definitions and simplifying. It is a sanity check that the ledger representation is faithful, not a derivation of the cost function's properties.

What the declaration does not claim is just as important. It does not claim that all admissible ledger costs must have a zero per-site term. A separate theorem, called l1_onsite_forced_constant, shows that a general ledger cost must have a constant per-site term if it satisfies a condition called global shift invariance. That condition says that adding the same constant to every site's value does not change the total cost. The declaration here does not invoke that condition. It simply observes that the specific cost function already sits in the slice where the per-site term is zero.

This distinction matters for the framework's broader project. The framework aims to derive physical structure from the forced cost of recognition. Showing that its core cost has no on-site term is a step. But it is a step about this particular function, not about all possible costs. The general theorem about what shift invariance forces is a separate result, and it is the one that carries the physical weight. This declaration is the quiet bookkeeping that confirms the ledger representation is consistent.

/-- The re-expression agrees with `exactJCostAction` exactly. -/
theorem exactJCostAsGeneralLedgerCost_eval {n : ℕ} (G : WeightedLedgerGraph n)
    (ε : LogPotential n) :
    (exactJCostAsGeneralLedgerCost G).eval ε = exactJCostAction G ε := by
  unfold GeneralLedgerCost.eval exactJCostAsGeneralLedgerCost exactJCostAction
  simp

/-- The re-expression agrees with `exactJCostAction` exactly. -/
theorem exactJCostAsGeneralLedgerCost_eval {n : ℕ} (G : WeightedLedgerGraph n)
    (ε : LogPotential n) :
    (exactJCostAsGeneralLedgerCost G).eval ε = exactJCostAction G ε := by
  unfold GeneralLedgerCost.eval exactJCostAsGeneralLedgerCost exactJCostAction
  simp

What this page does not claim

This declaration does not prove that the cost function is the only possible cost. This declaration does not derive the form of the cost function from first principles. This declaration does not address the exclusion of non-local screening effects.

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/PairKernelOnsiteExclusion.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: