c_RS_neg
plain-language theorem explainer
The RS leading-log coefficient satisfies c_RS < 0. Researchers comparing black-hole entropy corrections across quantum gravity approaches cite this to fix the sign of the phi-derived term before numerical checks. The proof unfolds the definition c_RS = -(log phi)/2, invokes one_lt_phi to obtain phi > 1, deduces log phi > 0 via Real.log_pos, and closes with linarith.
Claim. Let $c_{RS} := - (log phi)/2$. Then $c_{RS} < 0$.
background
The module recovers the Bekenstein-Hawking entropy from the discrete RS ledger as the count of admissible horizon states. It defines the combined formula S_RS(A) = A/4 + c_RS log A, where the leading term equals A/4 in RS-native units with Planck length set to 1. The coefficient is introduced by the definition c_RS := -(Real.log Constants.phi)/2, which appears in the master certificate structure BlackHoleEntropyFromLedgerCert.
proof idea
Term-mode proof. Unfold c_RS to expose the expression -(log phi)/2. Apply Constants.one_lt_phi to obtain 1 < phi. Apply Real.log_pos to obtain 0 < log phi. Linear arithmetic (linarith) then yields the strict inequality.
why it matters
The result supplies the c_RS_neg field of BlackHoleEntropyFromLedgerCert, the master certificate for Track F6. It confirms the leading-log term is negative and thereby distinct from the LQG value -1/2 and the string-theory value -3/2. The same fact is reused by c_RS_band to place c_RS inside (-0.25, 0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.