Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.LedgerBridgeNoGo

show as:
view Lean formalization →

Records a sign obstruction for ledger-to-geometry bridges in recognition gravity: any bridge that matches ledger deficits to geometric hinge deficits forces those geometric deficits to be nonnegative on the comparison map image. Downstream seven-gaps work cites it to rule out odd linear-response and negative-deficit matching. Proofs reduce to nonnegativity of J-costs and evenness under ratio inversion.

claimAny ledger-to-geometry bridge that matches recognition-ledger deficits to geometric hinge deficits forces the geometric deficit $\Delta_{\mathrm{geom}}$ to satisfy $\Delta_{\mathrm{geom}}(x_\sigma(h))\ge 0$ at every hinge $h$ in the image of the comparison map $x_\sigma$. Ratio-parity of the $J$-cost further implies that $J$-ratio cell costs and deficits are even under $r\mapsto 1/r$, so no such bridge (nor any ledger family with that parity) can realize a nonzero odd linear response in the deficit.

background

Recognition gravity bookkeeps curvature-like cost on a discrete recognition ledger whose continuum limit supplies the gravitational action. The ledger deficit at a cell is a sum of $J$-costs; $J(x)=(x+x^{-1})/2-1$ is the unique nonnegative cost fixed by the Recognition Composition Law, so every ledger deficit is nonnegative.

The ledger-to-geometry bridge module states the honest status of maps from that discrete substrate to an effective geometric (hinge) description. A comparison map $x_\sigma$ sends hinges into the ledger coordinate, and a bridge is asked to match ledger deficits to geometric deficits along that image.

This module sits in the Seven Gaps campaign: it isolates the pure sign and parity obstructions that any such matching bridge must obey before one attempts a full continuum identification.

proof idea

The positive sign theorem is a direct transfer of deficit_nonneg from the recognition ledger: once the bridge equates geometric deficit on the image of $x_\sigma$ with a ledger deficit, nonnegativity of summed $J$-costs yields $\Delta_{\mathrm{geom}}\ge 0$ there. The matching-no-go for a negative-deficit specification is the contrapositive.

Separately, $J$-cost ratio parity $J(r)=J(1/r)$ makes the ratio cell cost and the ratio deficit even functions of the strain ratio. Evenness plus an odd linear-response ansatz forces the response coefficient to vanish, giving the no-linear-response theorems for both single $J$-ratio deficits and full ledger families that inherit ratio parity. Auxiliary two-cell strain notation packages the local even/odd decomposition used in those arguments.

why it matters in Recognition Science

The module supplies the machine-checked no-go half of the recognition-ratio bridge story used by Seven Gaps Phase 0a. RecognitionRatioBridge imports it so that the paper's odd-form bridge (Def 6.2 clause) is constrained: any admissible matching bridge cannot reproduce negative geometric deficits or a nonzero odd linear response in the deficit.

CampaignLedger records the campaign status against these increments without flipping full-strength QGScopeAudit flags. In the broader RS gravity chain, the obstruction is the ledger-side reason one cannot naively identify an arbitrary geometric hinge deficit with a recognition cost: the cost is a sum of nonnegative $J$-values with $r\leftrightarrow 1/r$ symmetry, so the geometric side is forced into the same cone and parity class.

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)