Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioBridge

show as:
view Lean formalization →

Packages the paper's Def 6.2 recognition-ratio bridge: each hinge carries a positive ratio x, a coupling kappa, and a signed geometric deficit, linked by |log x - kappa·deficit| ≤ R·h³. Proves this form admits negative deficits and separates ledger from geometric observables, escaping the Lane 1a no-gos. Gravity workers closing the substrate-to-triangulation bridge cite it. Structure is definitional plus two-hinge witnesses and J-cost identities.

claimA recognition-ratio bridge on hinges $\sigma\in H$ assigns $x(\sigma)>0$, coupling $\kappa(\sigma)$, signed geometric deficit $\delta_g(\sigma)$, mesh scale $h$, and remainder $R$, subject to $|\log x(\sigma)-\kappa(\sigma)\,\delta_g(\sigma)|\le R\,h^3$. The module records this admissibility clause and proves compatibility with negative deficits and separation from recognition-ledger deficit observables.

background

Recognition gravity bookkeeps curvature in a recognition ledger; the continuum limit of total ledger cost is the gravitational action. Lane 1a (LedgerBridgeNoGo) proves two obstruction theorems against the assumed bridge that equates ledger deficit at each cell with a raw geometric hinge deficit: sign and parity kill that identification.

Lane 1b (LedgerEnergyBridge) supplies the corrected ledger-to-geometry path. This module sits between those results and stationarity closure. It packages Def 6.2 as an explicit structure: comparison is carried by $\log x$ rather than deficit equality, so the relation may take either sign. When the ratio enters ledger cost, the J-cost $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$ appears.

The remainder clause is recorded at fixed mesh; the $h\to 0$ family behind $O(h^3)$ is not yet formalized (open, lane 2).

proof idea

Primarily definitional: the bridge structure packages the odd admissibility inequality. Exact-case lemmas recover $\log x=\kappa,\delta_g$ and $x=\exp(\kappa,\delta_g)$ when the remainder vanishes.

Explicit two-hinge witnesses build concrete bridges with negative geometric deficit and negative log-ratio, showing escape from the Lane 1a no-gos. A companion ledger instance and cost identity route the ratio through J-cost via the cosh representation. Separation lemmas show ledger-deficit observables need not match geometric-deficit observables under this bridge, reconciling parity with the refuted raw identification.

why it matters in Recognition Science

Supplies the MODEL hypothesis that StationarityBridgeClosure imports when it closes stationarity to an inhabited bridge. Downstream treats the deficit-source coupling inside the sourced action as MODEL, inherited from this recognition-ratio form.

Within the Seven Gaps program this is the constructive counterpart to LedgerBridgeNoGo: after raw deficit-equality is refuted, the ratio form (paper Def 6.2) is the surviving admissibility clause. It does not derive the clause from first principles (wave 1b target) and does not formalize the continuum $h\to 0$ family. Framework contact runs through the recognition ledger and J-cost uniqueness (T5) when costs of ratios are evaluated.

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 (22)