rsPredictionLower
plain-language theorem explainer
RS lower bounds on three gravity discriminator sectors: leading-log coefficient above −1/4, echo damping above 1/2, and rung phase above 0. Gravity auditors cite these floors when filling the 4×3 rival matrix against LQG, string, CDT, and Bohmian. The definition is a three-way case split on Sector with explicit rational constants justified by elementary φ inequalities.
Claim. The Recognition Science lower bound on each discriminator sector is the map sending leading-log to $-1/4$ (so the RS coefficient $c_{\mathrm{RS}}$ is claimed above $-1/4$), echo-damping to $1/2$ (so the amplitude ratio $1/\varphi$ is claimed above $1/2$), and rung-phase to $0$ (so $\log\varphi$ is claimed positive).
background
Track 6.D of the quantum-gravity plan builds a 4×3 discriminator matrix: rivals (LQG, string, CDT, Bohmian) against three algebraic sectors. The sectors are LeadingLog (black-hole entropy leading-log coefficient, tied to QNM spectroscopy and holography), EchoDamping (φ-rung amplitude ratio, still quarantined until the echo mechanism is derived), and RungPhase (φ-rung phase coefficient, likewise quarantined).
Each matrix cell is meant to be a theorem-grade numerical band that separates RS from a rival and is observationally accessible. Session 93's DiscriminatorCert already supplies three theorem-grade discriminators from φ; this module supplies the explicit RS floors and ceilings that the cell inequalities compare against.
The comments on the cases record the elementary φ facts used as justification: $\log\varphi < 1/2$ forces the leading-log floor $-1/4$, $\varphi < 2$ forces $1/\varphi > 1/2$, and $\log\varphi > 0$ forces the rung-phase floor at zero.
proof idea
Pure definition by pattern match on the inductive type Sector. No tactics and no lemmas: LeadingLog maps to $-1/4$, EchoDamping to $1/2$, RungPhase to $0$. The inline comments record the intended φ inequalities that later cell theorems discharge when they prove RS lies strictly above these floors.
why it matters
Without explicit RS lower bounds the discriminator matrix cannot state numerical margins such as "margin > 1/4" against LQG's leading-log value $-1/2$ or "RS > 1/2" on echo damping. The module doc ties this directly to the Track 6 binding success criterion: at least one unambiguous cell per rival, with three or more theorem-grade discriminators from φ and named observational channels.
Sibling cell theorems (cell_LQG_LeadingLog, cell_String_LeadingLog, cell_LQG_EchoDamping, and the CDT/Bohmian positivity cells) are the intended consumers: they compare rivalPrediction against these floors and the matching upper bounds. The construction sits in the gravity domain of the forcing chain aftermath (T5 J-uniqueness, T6 φ fixed point), using φ-native constants rather than free fit parameters.
EchoDamping and RungPhase remain quarantined rung algebra until the missing echo mechanism is derived; the floors still give structural targets for that future derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.