Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker

show as:
view Lean formalization →

Defines the signed deficit-source constitutive coupling: the MODEL premise that a bare recognition ledger lacks. Source strength equals hinge coupling times signed geometric deficit, with mesh scale and small-source bound for the cubic estimate; no field names the recognition ratio. Gravity and QG auditors cite it as the substrate that turns stationarity into a ratio bridge. Structure is definitions plus derived equalities and a negative result that no bare-ledger selector recovers the signed source.

claimA signed deficit-source constitutive coupling supplies channel count, hinge coupling $\kappa$, signed geometric deficit, and source strength with $\mathrm{sourceStrength}(\sigma)=\kappa(\sigma)\cdot\mathrm{geometricDeficit}(\sigma)$, plus positive mesh scale and a structural small-source bound. No field of the coupling mentions the recognition ratio or $\log$ of that ratio. From this coupling one obtains a ratio bridge and the equality of log-ratio to minimizer strain; a bare sign-blind ledger cannot recover the signed source.

background

This module sits in the Seven Gaps gravity stack, immediately above the stationarity-to-bridge closure. That upstream file is theorem-status for every named statement and inherits a MODEL flag for the deficit-source coupling inside the sourced action (the same constitutive premise flagged in the hinge-stationarity core). Here that premise is isolated and named explicitly.

The central object is a signed deficit-source constitutive coupling: channel count, hinge coupling, signed geometric deficit, and source strength tied by the product law above, together with positive mesh scale and the small-source bound the cubic estimate needs. Companion structure includes a deficit-source action (equal to a sum of $J$-costs), a sign-blind bare ledger, and a recovery predicate asking whether a selector on that bare ledger can reconstruct the signed source.

Notation stays RS-native: $J$ is the unique cost from the forcing chain, and the recognition ratio is deliberately not a field of the coupling. The module's job is to state the substrate that is missing when one only has a bare ledger.

proof idea

Definition-heavy module with a short derived layer and one negative theorem. The coupling and action are introduced as data; an equality identifies the deficit-source action with a sum of $J$-costs. From the coupling one builds a ratio bridge and proves that the log-ratio equals minimizer strain, then packages a conditional derivation of the recognition ratio under the coupling hypothesis. Separately, the bare ledger is shown sign-blind (negation invariance of cost), and a no-go lemma states that no bare-ledger selector recovers the signed source; a nontrivial source-backed family is exhibited to make the obstruction live. No new axioms; the MODEL tag marks the constitutive premise, not a sorry.

why it matters in Recognition Science

Closes the honesty gap between a bare ledger and a derived recognition ratio: the ratio is not free data, it is forced only after the signed deficit-source coupling is supplied. Downstream, RecognitionRatioDerived packages this blocker's conditional derivation with the mesh dual-entry coupling and the stationarity minimizer receipt under the ledger name gap1_bridge_derived. FullTheoryLedger records that benchmark as a boolean pillar flag in the full QG campaign. RecognitionDualEntryEnrichment4D imports the same substrate for Wave B residual work on signed-source enrichment without an a-priori ratio field. In framework terms this is the constitutive hinge that lets stationarity (upstream bridge closure) become a ratio statement without smuggling $\log$-ratio into the MODEL.

scope and limits

used by (3)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)