Pith. sign in
module module high

IndisputableMonolith.Gravity.DiscriminatorMatrix

show as:
view Lean formalization →

Organizes Track 6 quantum-gravity discriminators as a matrix of rival programs versus observable sectors. Cells compare RS interval predictions on leading-log entropy corrections, echo damping, and rung phase against LQG, string, CDT, and the remaining canonical rival. Gravity and verification authors cite it when wiring falsifier margins into the master statement. Content is definitional layout plus imported prediction bounds, not new analytic proofs.

claimA discriminator matrix whose rows are the four canonical rival quantum-gravity programs and whose columns are observable sectors (leading-log coefficient of black-hole entropy, echo damping, rung phase). Each cell records the rival point prediction $P_R$ against the RS lower/upper bounds $(L_{\mathrm{RS}},U_{\mathrm{RS}})$ on that sector, marking separation when the intervals are disjoint.

background

Track 6 of the quantum-gravity master plan demands theorem-grade separators between Recognition Science and the four canonical alternative programs. Upstream, black-hole entropy from the ledger recovers the Bekenstein-Hawking area law $S_{BH}=A/(4\ell_P^2)$ as a count of admissible horizon states and predicts a $\varphi$-rational coefficient on the leading $\log A$ correction, already distinct from the LQG value $-1/2$ and the string value $-3/2$. The SI entropy module sharpens those numerical margins.

Echo structure is supplied only as $\varphi$-rung algebra: the bounce-to-exterior escape story is explicitly quarantined, since a true event horizon forbids re-emergence. DiscriminatorCert packages three theorem-grade separators built on those bounds. This module is the tabular layout that names rivals, sectors, and the per-cell RS versus rival predictions those certificates fill.

proof idea

Definition and assembly module, not a deep proof development. It introduces rival and sector enumerations, rival point predictions, and RS lower/upper prediction maps, then fills named cells (LQG/string/CDT on leading-log, echo damping, and rung-phase signs or separations). Load-bearing inequalities and SI conversions live in the imported entropy and DiscriminatorCert modules; here the work is wiring those facts into a uniform matrix so downstream certificates can index cells rather than restate comparisons.

why it matters in Recognition Science

Feeds Gravity.MasterTheorem (Track 7.A master statement, conditional form authored once the seven tracks close) and Verification.Track6FalsifierSensitivity (Fork F integration endpoint for Track 6 of the master plan). Without a single matrix of rivals versus sectors, falsifier sensitivity cannot cite a stable index of which observable separates RS from which program. The layout realizes master-plan §4 Track 6.D: discriminators against the four canonical alternatives, grounded in the $\varphi$-ladder entropy log term and the quarantined echo rung algebra rather than new dynamics.

scope and limits

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (23)