c_RS_string_margin
plain-language theorem explainer
Strict lower bound: the RS leading-log black-hole entropy coefficient sits more than 5/4 above the string-theory canonical value −3/2. Anyone building observational discriminators or QNM/ringdown certificates against string theory cites this margin. The proof unfolds c_RS = −(log φ)/2 and feeds log φ < 1/2 into linear arithmetic.
Claim. With the RS leading-log coefficient $c_{\mathrm{RS}} = -(\log\varphi)/2$, one has $c_{\mathrm{RS}}-(-3/2)>5/4$. Equivalently $(\,3-\log\varphi\,)/2>5/4$, so any measurement of the leading-log coefficient finer than margin $5/4$ separates RS from the string-theory canonical value $-3/2$.
background
Track 3.B of the quantum-gravity plan lifts Bekenstein–Hawking leading entropy into SI units and sharpens leading-log discriminators against LQG and string theory. The RS coefficient is defined in the ledger module by $c_{\mathrm{RS}}=-(\log\varphi)/2\approx-0.241$. String theory’s canonical leading-log value is $-3/2$; mere inequality $c_{\mathrm{RS}}\neq-3/2$ is already known, but an observational channel needs an explicit numerical margin.
The key analytic input is $\log\varphi<1/2$, proved from $\varphi^2=\varphi+1<2.62<e$ and monotonicity of $\log$. That bound is sharper than the older private $\log\varphi<1$. In RS-native units $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain; here it only enters through the leading-log slope of the entropy expansion.
Sibling margins in the same module treat the LQG canonical $-1/2$ with gap $>1/4$. Both feed the SI entropy certificate and the discriminator matrix.
proof idea
Term-mode proof, three steps. First invoke the sibling lemma $\log\varphi<1/2$. Unfold the ledger definition $c_{\mathrm{RS}}=-({\rm Real.log},\varphi)/2$, so the target difference rewrites as $(3-\log\varphi)/2$. Linear arithmetic then closes: $\log\varphi<1/2$ forces $3-\log\varphi>5/2$, hence the quotient exceeds $5/4$. No further lemmas or case splits.
why it matters
Closes the string half of the sharper discriminator package in Track 3.B. The absolute-value form $|c_{\mathrm{RS}}-(-3/2)|>5/4$ is an immediate corollary, and both land in the master structure BlackHoleEntropySICert and the one-statement theorem that packages SI entropy lift plus LQG/string margins.
Downstream, leadingLogDiscriminator_holds and rs_qnm_distinct_LQG_string quote this bound as the theorem-grade separation of RS ringdown/QNM spectroscopy from string’s canonical $-3/2$. The discriminator matrix cell for string leading-log likewise depends on it. Framework-wise this is pure observational hygiene: φ-forced $c_{\mathrm{RS}}$ is pinned far enough from string that any experiment with sensitivity better than $5/4$ on the coefficient falsifies one side. No open sorry remains on this margin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.