Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker

show as:
view Lean formalization →

Models the signed deficit-source constitutive coupling that is missing from any bare ledger: channel count, hinge coupling, geometric deficit, and source strength linked by sourceStrength = kappa * geometricDeficit, plus mesh scale and small-source bound. No field names the recognition ratio. Shows the ratio and log-ratio bridge are derived from that coupling, and that no sign-blind bare-ledger selector recovers a signed source. Cited by the full-theory ledger as the substrate-blocker pillar.

claimA signed deficit-source constitutive coupling supplies channels, 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. From this coupling alone one derives the recognition-ratio bridge and $\log$-ratio equals minimizer strain. No sign-blind bare ledger recovers a signed source; a nontrivial source-backed family exists.

background

This module sits in the Seven Gaps gravity campaign, immediately after stationarity-to-bridge closure. Upstream, every named statement in StationarityBridgeClosure is a theorem (0 sorry, 0 new axiom); the deficit-source coupling inside the sourced action is explicitly flagged MODEL and inherited here under the same label.

The missing premise is a signed deficit-source constitutive coupling: it packages channel count, hinge coupling, signed geometric deficit, and a source strength forced by the product law $\mathrm{sourceStrength}=\kappa\cdot\mathrm{geometricDeficit}$, together with positive mesh scale and the small-source bound used by cubic estimates. Critically, none of its fields mention the recognition ratio or $\log$ of that ratio.

A companion bare object is the sign-blind bare ledger (cost data without signed source). The module contrasts what the constitutive coupling derives with what any selector on the bare ledger can recover.

proof idea

Definition layer: introduce the MODEL structure DeficitSourceConstitutiveCoupling and the associated deficit-source action; prove the action equals a sum of $J$-costs. Bridge layer: build the recognition-ratio bridge from the coupling and derive that the recognition ratio (and its log) equal minimizer strain, without ever putting the ratio into the MODEL fields.

Blocker layer: define the sign-blind bare ledger and cost extensionality; show negation invariance of the bare ledger; formalize the predicate "recovers signed source from bare ledger"; prove no bare-ledger selector recovers a signed source; exhibit a nontrivial source-backed family. Overall shape is MODEL definition plus derived bridge theorems plus a negative recovery theorem.

why it matters in Recognition Science

Closes the substrate gap between stationarity-bridge theorems and a full sourced recognition ledger: the recognition ratio is not primitive; it is forced by a signed deficit-source constitutive law that the bare ledger does not contain. Downstream, FullTheoryLedger imports this module as part of Phase 0c of the full quantum-gravity campaign ledger (one boolean flag per pillar; flags flip only on kernel-checked, axiom-audited targets).

In framework terms it separates constitutive MODEL data (channels, $\kappa$, geometric deficit, source strength) from derived recognition-ratio observables, and records an explicit impossibility: sign-blind cost ledgers cannot select signed sources. That blocker is what justifies carrying the coupling as MODEL rather than pretending the bare ledger already encodes gravity sourcing.

scope and limits

used by (1)

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)