Pith. sign in
module module high

IndisputableMonolith.Foundation.PairKernelOnsiteExclusion

show as:
view Lean formalization →

Defines general ledger costs on log-potential carriers as free onsite terms plus link terms on posting differences, then forces the onsite sum to a constant under shift invariance. Cited by anyone deriving pair-kernel locality or excluding absolute mass terms from the RS ledger. Argument classifies shift-invariant costs, embeds exact J-cost, and kills non-constant onsite decoys (e.g. Yukawa-type).

claimA general ledger cost on $n$ log-potential carriers is $C(\psi)=\sum_i\mathrm{onsite}(\psi_i)+\sum_{i\sim j}w_{ij}\,\mathrm{link}(\psi_i-\psi_j)$ over an admissible weighted graph. Shift invariance (invariance under $\psi\mapsto\psi+c$) holds if and only if the onsite sum is constant; non-constant onsite decoys fail it. Exact $J$-cost embeds as one such ledger cost.

background

Recognition Science assigns costs to configurations of log-potential carriers $\psi$. The classical cost $J(x)=(x+x^{-1})/2-1$ is forced by the Recognition Composition Law (T5) and, via the continuum and nonlinear bridges, stationarizes to Regge equations and Einstein gravity (up to $\kappa=8\varphi^5$).

This module works one level more abstractly. A general ledger cost allows a free absolute per-site term onsite plus a per-link term on posting differences over a weighted graph. Nothing in the bare structure forces onsite to vanish or even to be constant; that forcing must come from an extra hypothesis.

The natural extra hypothesis is shift invariance: the cost depends only on differences, not on absolute levels of $\psi$. Upstream continuum and edge-length modules identify pure $J$-cost with geometric edge data; here the question is which deformations of that cost remain admissible.

proof idea

Definition-heavy module with a short forcing chain. Introduce GeneralLedgerCost (onsite + weighted link) and the predicate ShiftInvariant. The link part is automatically shift-invariant. Characterize the full cost as shift-invariant iff the onsite sum is constant (shiftInvariant_iff_onsite_sum), and specialize to force an $\ell^1$ onsite term constant. Exhibit a Yukawa-type onsite decoy that fails shift invariance, and a mean-field weight with full support whose ledger cost is shift-invariant. Close by embedding exact $J$-cost as one instance of GeneralLedgerCost.

why it matters in Recognition Science

Supplies the onsite-exclusion step required by the pair-kernel provenance lane. Downstream PairKernelLocality (Door 2 / L0) states that this module "proved on-site-mass exclusion conditional on ShiftInvariant (difference-only cost)", clearing the last absolute-term obstruction before finite-range locality on the ledger weight graph can be imposed. That locality hypothesis, together with the ratio bridge, feeds the continuum identification of $J$-cost with the Regge action and thence EFE. Without onsite exclusion, absolute mass-like terms would survive into the continuum limit and spoil the pure curvature reading of the ledger.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (14)