c_RS_observable_distinct_carried_prop
plain-language theorem explainer
Packages four strict separation inequalities for the RS leading-log black-hole entropy coefficient against the LQG value −1/2 and the semiclassical value −3/2. Cited by anyone assembling the Track 3.B / M4 discriminator clause of the quantum-gravity master theorem. Pure Prop definition: no proof obligation, only the carried margin content.
Claim. The proposition that the RS leading-log entropy coefficient $c_{\mathrm{RS}}$ satisfies $c_{\mathrm{RS}}+\tfrac12>\tfrac14$, $c_{\mathrm{RS}}+\tfrac32>\tfrac54$, $\lvert c_{\mathrm{RS}}+\tfrac12\rvert>\tfrac14$, and $\lvert c_{\mathrm{RS}}+\tfrac32\rvert>\tfrac54$ (signed and absolute separation from the loop value $-1/2$ and the semiclassical value $-3/2$).
background
Gravity Track 7.A authors the quantum-gravity master statement as a twelve-clause conjunction. One closed clause is the leading-log entropy discriminator (Track 3.B / Session 90, margin content M4): the RS coefficient of the black-hole entropy expansion must sit observably away from both loop quantum gravity and semiclassical/string benchmarks.
Here $c_{\mathrm{RS}}$ is the leading-log coefficient drawn from the ledger-derived black-hole entropy module. The classical comparison points are the LQG value $-1/2$ and the semiclassical value $-3/2$. The carried content records four inequalities: signed excess over each benchmark by more than $1/4$ and $5/4$ respectively, together with the matching absolute-value bounds.
This definition isolates only that margin content. The full observable-distinctness clause later conjoins it with the SI black-hole entropy certificate.
proof idea
No proof. The declaration is a def of type Prop whose body is the four-fold conjunction of the signed and absolute separation inequalities on Gravity.BlackHoleEntropyFromLedger.c_RS. Downstream consumers treat the name as a single atomic hypothesis or certificate atom.
why it matters
Supplies the pure mathematical content of master-theorem clause M4 (leading-log discriminator). The parent definition c_RS_observable_distinct is exactly this Prop conjoined with Nonempty BlackHoleEntropySICert; the non-circularity audit records that equality by rfl.
In the Recognition framework this is the concrete numerical wedge between RS gravity and both LQG and string/semiclassical entropy coefficients. It is one of the eight CLOSED clauses discharged inside rs_quantum_gravity_master_conditional from existing Session 89–96 anchors, while five other tracks remain open as hypothesis inputs. Without these strict margins the master statement could not claim observable distinctness of the entropy expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.