S_RS
plain-language theorem explainer
The RS black-hole entropy combines the leading area term with a logarithmic correction from the ledger. Quantum gravity researchers comparing coefficient predictions would cite it to distinguish the RS value from LQG and string-theory results. The declaration is a direct definition that assembles the pre-derived S_lead and c_RS without additional steps.
Claim. The RS black-hole entropy is defined by $S_{RS}(A) = A/4 + c_{RS} log A$, where $c_{RS} = -log φ / 2$ and $A$ is the horizon area in RS-native units with Planck length set to 1.
background
The module recovers Bekenstein-Hawking entropy from the discrete RS ledger as the count of admissible horizon states modulo σ-equivalence. S_lead(A) is the leading-order term defined by A/4. The coefficient c_RS is the RS-specific value -log φ / 2, obtained from the two-sided 8-tick washout prefactor in the cosmology derivation and specialized here to the gravity setting.
proof idea
One-line definition that applies the sibling S_lead(A) = A/4 together with the local c_RS = -(Real.log Constants.phi)/2.
why it matters
This supplies the full entropy expression that the module certifies against the classical formula. It completes the combined leading-plus-log step in Track F6, with the φ-rational coefficient structurally distinct from the LQG value -1/2 and the string-theory value -3/2. The module flags the empirical coefficient match as awaiting semiclassical gravity adjudication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.