module module high

`IndisputableMonolith.Gravity.DiscriminatorMatrix`

Tabulates Recognition Science predictions against four canonical quantum-gravity rivals across leading-log entropy, echo-damping, and rung-phase sectors. Track 6 and the gravity master theorem import it as the explicit comparison table required by master-plan §4 Track 6.D. Cells are short separation certificates built from upstream ledger-entropy and echo-rung bounds, with RS interval envelopes versus rival point or interval forecasts.

claimA finite discriminator matrix with rows the four canonical rival quantum-gravity programs and columns the observable sectors (leading $\log A$ entropy correction, black-hole echo damping, $\varphi$-rung phase). Each cell records whether the rival forecast lies outside the RS prediction interval $[L,U]$ for that sector, using ledger-derived entropy coefficients and structural echo-rung algebra in RS-native units.

background

Recognition Science recovers Bekenstein-Hawking entropy $S_{BH}=A/(4\ell_P^2)$ as a count of admissible horizon states on the discrete ledger, with a $\varphi$-rational coefficient on the leading $\log A$ term. Upstream entropy modules already separate that coefficient from the LQG value $-1/2$ and the string-theory value $-3/2$, and sharpen SI-unit margins.

Echo material imported here is structural $\varphi$-rung algebra only. The physical bounce-to-exterior re-emergence story is quarantined: a true event horizon does not permit that escape, so discriminators use the rung algebra and damping bounds without claiming a closed exterior-echo mechanism.

Track 6 of the quantum-gravity master plan demands theorem-grade discriminators against the four canonical alternatives. The companion certificate module supplies three such discriminators; this module organizes rivals, sectors, RS lower/upper envelopes, and named cells into an explicit comparison matrix.

proof idea

Definition-and-tabulation module, not a deep new proof engine. It introduces rival and sector enumerations, maps for rival forecasts and RS lower/upper prediction envelopes, then named cells (LQG/string/CDT on leading-log, echo-damping, and rung-phase) that assert separation or distinctness.

Each cell is a short certificate: apply imported entropy-SI margins or echo-rung lemmas, compare the rival value to the RS interval, and record outside/distinct. Load-bearing facts come from the entropy-from-ledger, entropy-SI, echo-from-bounce, and discriminator-certificate imports; this file wires them into the matrix layout Track 6 expects.

why it matters in Recognition Science

Feeds Gravity.MasterTheorem (Track 7.A master statement, conditional form) and Verification.Track6FalsifierSensitivity (Fork F integration endpoint for Track 6). Those parents need an explicit rival-versus-sector table so the master plan §4 Track 6.D requirement is machine-checkable rather than narrative.

Downstream sensitivity certificates read the cells to bound how far an observation must move before a discriminator collapses. The module sits on the closed structural path of the entropy-SI and discriminator-certificate work (zero sorry, zero RS-internal axiom on that path) and adds no new RS axioms. It is the bookkeeping layer that turns three theorem-grade discriminators into the matrix the master theorem and falsifier track cite.

scope and limits

Does not claim a closed physical bounce-to-exterior echo mechanism; that path is quarantined upstream.
Does not derive new values of $\alpha$, $G$, or other constants; it consumes RS constants and imported bounds.
Does not assert experimental detection of echoes or log corrections; only prediction separation on paper.
Does not cover every quantum-gravity program; only the four canonical rivals named for Track 6.D.
Does not replace the discriminator-certificate theorems; it organizes and cites them in matrix form.

used by (2)

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

IndisputableMonolith.Gravity.MasterTheorem module_import
IndisputableMonolith.Verification.Track6FalsifierSensitivity module_import

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce module_import
IndisputableMonolith.Gravity.BlackHoleEntropyFromLedger module_import
IndisputableMonolith.Gravity.BlackHoleEntropySI module_import
IndisputableMonolith.Gravity.DiscriminatorCert module_import

declarations in this module (23)

inductive Rival L82
inductive Sector L92
def rivalPrediction L103
def rsPredictionLower L120
def rsPredictionUpper L126
theorem cell_LQG_LeadingLog L142
theorem cell_LQG_EchoDamping L147
theorem cell_LQG_RungPhase L152
theorem cell_String_LeadingLog L157
theorem cell_String_EchoDamping L163
theorem cell_String_RungPhase_positive L169
theorem cell_CDT_LeadingLog_distinct L175
theorem cell_CDT_EchoDamping_positive L180
theorem cell_CDT_RungPhase_positive L184
theorem cell_Bohmian_LeadingLog_distinct L190
theorem cell_Bohmian_EchoDamping_positive L195
theorem cell_Bohmian_RungPhase_positive L200
structure DiscriminatorMatrixCert L212
def discriminatorMatrixFull L236
theorem discriminatorMatrixFull_inhabited L253
structure PerRivalDistinguishability L262
def perRivalDistinguishability_holds L272
theorem discriminator_matrix_one_statement L294