c_RS_neq_string
plain-language theorem explainer
RS leading-log coefficient for black-hole entropy corrections differs algebraically from the string-theory value -3/2. Quantum gravity researchers comparing model predictions would cite this separation. Proof assumes equality, substitutes the definition c_RS = -log phi /2, rearranges to log phi =3, and contradicts the bound log phi <1 by linear arithmetic.
Claim. Let $c_{RS} = - (log phi)/2$. Then $c_{RS} ≠ -3/2$.
background
The module recovers Bekenstein-Hawking entropy from the discrete RS ledger by counting admissible horizon states modulo sigma-equivalence. The leading-log correction takes the form c_RS log A with the coefficient defined as c_RS := -(Real.log Constants.phi)/2. The module also records S_lead(A) = A/4 together with positivity for A > 0.
proof idea
Assume for contradiction that c_RS equals -3/2. Unfold the local definition of c_RS. The equality rearranges to log phi = 3. Apply the lemma log_phi_lt_one to obtain log phi < 1. Linear arithmetic produces the contradiction.
why it matters
This theorem supplies the c_RS_neq_string field of the BlackHoleEntropyFromLedgerCert structure. The structure in turn feeds the one-statement theorem that packages the A/4 match, negativity, and distinctions from both LQG and string theory. It sharpens the phi-rational prediction against the string-theory canonical value, consistent with the module falsifier of an observed coefficient lying outside a 0.05 neighborhood of c_RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.