Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.LedgerBridgeNoGo

show as:
view Lean formalization →

No-go module for ledger-to-geometry bridges in recognition gravity. Any bridge that matches ledger deficits to geometric hinge deficits is forced to keep those geometric deficits nonnegative on the comparison map image, because ledger deficits are sums of nonnegative J-costs. Parity and evenness lemmas then rule out odd linear response in ratio-based deficit families. Cited by the seven-gaps campaign ledger and the recognition-ratio bridge phase.

claimIf a ledger-to-geometry bridge equates geometric hinge deficit $\Delta_{\mathrm{geom}}$ to ledger deficit $\Delta_{\mathrm{led}}$ along the comparison map $x_\sigma$, then $\Delta_{\mathrm{geom}}(x_\sigma(h))\ge 0$ at every hinge $h$. Ratio-cell costs built from $J$ are even under $r\mapsto 1/r$, so no such family can reproduce an odd (linear-response) deficit specification.

background

Recognition gravity books curvature-like cost on a discrete recognition ledger whose continuum limit supplies the gravitational action. The ledger deficit at a cell is assembled from the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), which is nonnegative for $x>0$ and vanishes only at $x=1$.

The companion module on the ledger-to-geometry bridge records the honest status of matching that discrete bookkeeping to an effective geometric (hinge) description. A bridge is a comparison map $x_\sigma$ together with a deficit-matching condition that identifies geometric hinge deficit with ledger deficit on the image of $x_\sigma$.

This module sits inside the Seven Gaps campaign: it isolates sign and parity obstructions that any admissible bridge must obey before one can claim a linear-response or odd-form recognition-ratio bridge.

proof idea

The positive-form sign obstruction is a direct transfer of ledger nonnegativity: once deficit-matching is assumed, geometric deficit on the image of $x_\sigma$ inherits nonnegativity from the fact that ledger deficits are sums of J-costs. A matching negative geometric deficit specification is therefore impossible.

Separately, ratio-cell costs and the associated ratio deficits are shown even under inversion of the ratio (J-cost ratio parity). Evenness plus an odd target forces the response to vanish, killing linear-response models built from pure ratio deficits. The same parity lifts to ledger families, yielding a family-level no-go for odd linear response.

why it matters in Recognition Science

Closes a concrete obstruction slice of the QG seven-gaps campaign: bridges cannot smuggle negative geometric deficits past the ledger, and ratio-only deficit families cannot supply the paper's odd (linear-response) form. Downstream, CampaignLedger imports this module as a scoped, kernel-checked increment without flipping full-strength QGScopeAudit flags. RecognitionRatioBridge (Phase 0a) uses the same no-go layer while treating the recognition-ratio bridge structure itself as a model-tier admissibility hypothesis (paper Def 6.2 clause), with the named theorems kept theorem-tier.

In framework terms this protects the J-cost forcing (T5) as it enters gravity: the composition law and nonnegativity of $J$ are not optional decoration; they constrain every ledger-to-geometry dictionary.

scope and limits

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (16)