Pith. sign in
module module high

IndisputableMonolith.Gravity.DiscriminatorCert

show as:
view Lean formalization →

Certificate layer that separates RS black-hole predictions from LQG and string theory on three observables: the leading-log entropy coefficient c_RS = -log(φ)/2, echo damping, and rung-phase delay. Gravity auditors cite it when wiring the discriminator matrix and the master theorem. Arguments are direct algebraic comparisons of closed-form RS constants to rival canonical values, packaged as inhabited certificate records.

claimThree discriminator certificates: (i) the RS leading-log entropy coefficient $c_{\mathrm{RS}}=-\log\phi/2$ differs from the LQG value $-1/2$ and the string value $-3/2$; (ii) the RS echo-damping ratio is strictly above $1/2$; (iii) the RS rung-phase delay is strictly below $1/2$. These assemble into an inhabited discriminator-matrix certificate, with a corollary that RS quasinormal-mode signatures are distinct from the LQG and string canons.

background

Recognition Science recovers the Bekenstein-Hawking area law from a discrete ledger count of admissible horizon states modulo σ-equivalence. Beyond the area term, RS predicts a φ-rational leading logarithmic correction $c\cdot\log A$ with coefficient $c_{\mathrm{RS}}=-\log\phi/2$. The literature already records LQG's canonical $-1/2$ and string theory's $-3/2$, so a clean numerical gap is available as a discriminator.

This module sits on BlackHoleEntropyFromLedger and BlackHoleEntropySI (Track F6 / Track 3.B), which supply the entropy coefficient and SI-unit margins, and on BlackHoleEchoesFromBounce, which supplies the φ-rung algebra for echo timing. Upstream status is explicit: the physical bounce-to-exterior echo mechanism is quarantined as not closed; only the rung algebra is treated as structural. Constants supplies φ and the RS time quantum.

proof idea

Three Prop-carrying discriminator structures are defined (leading-log, echo-damping, rung-phase). Each holds-lemma discharges by direct comparison of an RS closed form to fixed rival thresholds: $c_{\mathrm{RS}}=-\log\phi/2$ versus $-1/2$ and $-3/2$; echo-damping ratio above $1/2$; rung-phase delay below $1/2$. A matrix certificate packages the three, with an inhabitedness witness. A final corollary records QNM distinctness versus the LQG and string canons. No deep tactic search: the load-bearing steps are algebraic inequalities on explicit constants imported from the entropy and echo modules.

why it matters in Recognition Science

Feeds Gravity.DiscriminatorMatrix (Track 6.D: 4 rivals × 3 sectors discriminator matrix) and Gravity.MasterTheorem (Track 7.A master statement, conditional form). Downstream docs mark both as structural closures of the quantum-gravity master plan. The leading-log gap is the paper-level claim that RS is already distinguishable from LQG and string theory on the log-area coefficient; echo and rung-phase certificates extend the same separation into the bounce/echo sector, under the upstream quarantine that exterior-echo physics is not closed. This module is the certificate glue those parents import rather than a new physical derivation.

scope and limits

used by (2)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (15)