rsPredictionUpper
plain-language theorem explainer
RS supplies a sector-wise numerical upper bound on its own predicted observables: 0 on the leading-log coefficient, 1 on echo damping, and 1/2 on the rung phase. Builders of the 4×3 gravity discriminator matrix cite these ceilings when proving strict separation from rival bands. The body is a three-way case split on Sector, pinned by the known inequalities c_RS < 0, 1/φ < 1, and log φ < 1/2.
Claim. For each algebraic sector $S$, the RS upper prediction $U(S)\in\mathbb{R}$ is $U(\mathrm{LeadingLog})=0$, $U(\mathrm{EchoDamping})=1$, and $U(\mathrm{RungPhase})=1/2$. These ceilings match the comments $c_{\mathrm{RS}}<0$, $1/\varphi<1$, and $\log\varphi<1/2$.
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, the physical channel), EchoDamping (quarantined φ-rung amplitude ratio), and RungPhase (quarantined φ-rung phase coefficient).
Cell margins compare an RS band to a rival prediction. When the rival quotes a number, the margin is a strict inequality RS − rival > margin; when the rival predicts no signal, positivity (or negativity) of the RS value alone discriminates. The matrix therefore needs explicit RS lower and upper numerical envelopes per sector.
The leading-log envelope is tied to the RS coefficient c_RS (negative in the native ledger/SI bridge conventions used here). Echo damping sits at the Berry-scale ratio 1/φ. Rung phase sits at log φ. The companion lower-bound map records the matching floors; together they box each RS cell for theorem-grade margin proofs.
proof idea
Pure definition by cases on the Sector inductive. LeadingLog maps to 0 (comment: c_RS < 0). EchoDamping maps to 1 (comment: 1/φ < 1). RungPhase maps to 1/2 (comment: log φ < 1/2). No tactics, no lemmas, no sorry: a total function Sector → ℝ whose numerical choices are the claimed RS upper envelopes.
why it matters
Fills the RS upper column of the Track 6.D discriminator matrix in Gravity.DiscriminatorMatrix. Module status is structural theorem (0 sorry, 0 RS-internal axiom): combined with DiscriminatorCert it closes the binding success criterion that the matrix exist with at least one unambiguous cell per rival and three or more theorem-grade φ-derived discriminators with named channels.
Downstream cell lemmas (LQG/String/CDT/Bohmian × LeadingLog/EchoDamping/RungPhase) use these ceilings to state margins such as RS leading-log at least 1/4 above LQG's −1/2, echo damping above 1/2, and rung phase below 1/2. The definition therefore anchors the anti-retreat numerical bands without itself proving the inequalities; those live in the cell theorems and in the c_RS / φ facts from Constants and the SI bridge.
Framework landmarks in play: φ from the T6 self-similar fixed point, the eight-tick octave behind ledger timing, and the native c_RS bookkeeping used in entropy and cosmology prefactors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.