c_RS_observable_distinct_proven
plain-language theorem explainer
The RS black-hole entropy prefactor is observably distinct from both LQG and string-theory values, with certified positive absolute margins. Gravity and quantum-gravity workers comparing microstate-counting schemes cite this closed master-theorem clause. The proof is a pure term that packages the four margin fields and the BlackHoleEntropySI certificate.
Claim. The Recognition Science black-hole entropy coefficient $c_{\mathrm{RS}}$ is observably distinct from the loop-quantum-gravity and string-theory coefficients: the signed and absolute margins against both alternatives are positive, as certified by the SI black-hole entropy certificate.
background
Gravity Track 7.A authors the quantum-gravity master statement as a twelve-clause conjunction. Eight clauses are CLOSED and discharged from existing Lean certificates; five remain open as hypothesis inputs. This declaration inhabits one closed clause: observable distinctness of the RS entropy prefactor.
The SI black-hole entropy certificate (BlackHoleEntropySI) already records numerical margins of $c_{\mathrm{RS}}$ against the LQG and string values, together with their absolute values. Those four margin fields, plus the certificate itself, are the only data needed here.
Local setting: the master theorem is still conditional on five open tracks (RegEH continuum/Bianchi, unconditional amplitude linearity, Page curve, PTA stochastic GW, strong-field tests). Closed clauses such as this one are discharged unconditionally inside that conditional proof.
proof idea
Term-mode pair construction, no tactics. The outer pair is (margins, certificate). The margins component is the 4-tuple of fields from blackHoleEntropySICert: signed LQG margin, signed string margin, absolute LQG margin, absolute string margin. The certificate component is the singleton packing of the same blackHoleEntropySICert record. Inhabitation of c_RS_observable_distinct is therefore pure packaging of an already-proved SI certificate.
why it matters
Feeds the conditional master theorem rs_quantum_gravity_master_conditional, which under five open-track hypotheses asserts the full twelve-clause RS quantum-gravity statement, discharging the eight closed clauses from Sessions 89–96 anchors. Also feeds closed_certs_hold in the non-circularity audit, which conjoins the six closed certificate clauses (Lorentzian 1+3, Hawking temperature SI, this distinctness claim, $\Omega_\Lambda$ from $\phi$, QNM distinctness, and related).
In the framework this is a discriminator clause: RS predicts a concrete entropy prefactor whose separation from LQG and string is numerically certified, not merely qualitative. It sits beside the Hawking-temperature SI and QNM-distinctness closed clauses as part of the gravity-track evidence bundle. It does not touch T0–T8 forcing, RCL, or the $\phi$-ladder mass formula directly; those enter other master clauses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.