rs_qnm_distinct_LQG_string
plain-language theorem explainer
Packages the black-hole QNM/echo discriminator clause used by the quantum-gravity master statement: RS leading-log entropy coefficient and echo damping are distinct from LQG and string benchmarks, and the full discriminator-matrix certificate is inhabited. Gravity and QG auditors cite it as master-plan clause M4. It is a pure Prop conjunction of carried margins with Nonempty of the matrix cert; no new proof work lives here.
Claim. The QNM discriminator clause holds when both of the following are true: (i) the RS leading-log coefficient satisfies $c_{\mathrm{RS}}-(-1/2)>1/4$ and $c_{\mathrm{RS}}-(-3/2)>5/4$, and the echo damping ratio lies in $(1/2,1)$ and is positive; (ii) the discriminator-matrix certificate (leading-log, echo-damping, and rung-phase cells against LQG, string, and related rivals) is inhabited.
background
Gravity Track 7.A authors the master quantum-gravity statement as a twelve-clause conjunction. Closed clauses are named Props discharged from existing theorems; open tracks remain hypothesis inputs. This declaration is the named Prop for the QNM/echo discriminator clause (M4).
The carried content asserts explicit margins on the RS leading-log entropy coefficient $c_{\mathrm{RS}}=-\log\varphi/2$ against the LQG value $-1/2$ and the string value $-3/2$, together with the per-echo damping ratio strictly inside $(1/2,1)$ and positive (distinct from uniform damping, no echo, and undamped). Upstream, the DiscriminatorCert theorem already proves the two leading-log inequalities, and the matrix cert structure packages three independent discriminators (leading-log, echo damping, rung phase) covering RS vs LQG, string, uniform discreteness, and no-echo.
The second conjunct only requires that the matrix certificate type be inhabited, i.e. that every required cell is filled by a theorem-grade algebraic inequality.
proof idea
Definitional packaging only: the Prop is the conjunction of the carried QNM/echo content and Nonempty of the discriminator-matrix certificate. No tactics or lemmas are applied at this site. Downstream, the proven inhabitant builds the first conjunct from the DiscriminatorCert leading-log and echo theorems and the second from the inhabited matrix cert constructor.
why it matters
Fills master-plan Track 7 clause M4 (Session 93 QNM discriminator): RS ringdown/QNM spectroscopy is theorem-grade distinct from LQG and string at the leading-log coefficient, with echo-band content included. It is one conjunct of RSQuantumGravityMaster and is discharged inside the conditional master theorem once the five open-track hypotheses are supplied.
Parents include the proven inhabitant of this Prop, the strong-field-tests bundle, the one-statement discriminator matrix theorem, and the non-circularity audit of closed certs. Framework-wise it is an observational discriminator, not a forcing-chain step: it separates RS predictions ($c_{\mathrm{RS}}\approx -0.241$, damping $1/\varphi$) from canonical QG alternatives without claiming the full unconditional discovery until Tracks 1.B/1.C, 2, 3.C, and 6.B/6.C close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.