c_RS_string_margin_abs
plain-language theorem explainer
The absolute gap between the RS leading-log entropy coefficient and the string-theory canonical value −3/2 exceeds 5/4. Quantum-gravity auditors cite this when packaging observational discriminator certificates against string entropy expansions. The proof is a short absolute-value rewrite of the already-proved signed margin, using positivity from linear arithmetic.
Claim. Let $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$ be the RS leading-log coefficient. Then $\lvert c_{\mathrm{RS}} - (-3/2)\rvert > 5/4$.
background
In Recognition Science the leading-log coefficient of black-hole entropy is fixed by the two-sided eight-tick sphaleron washout: each of the matter and antimatter sectors contributes a factor $(1 - \varphi^{-8})$, so $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$. Canonical string-theory treatments of the same expansion take the value $-3/2$.
This module closes Track 3.B of the quantum-gravity master plan: an SI lift of Bekenstein–Hawking leading entropy, plus sharper discriminator margins against LQG ($c = -1/2$) and string ($c = -3/2$). Strict inequality $c_{\mathrm{RS}} \neq -3/2$ is already known from the ledger module; an observational channel needs an explicit lower bound on the gap so that experimental sensitivity below the margin closes the falsification window.
The signed margin $c_{\mathrm{RS}} - (-3/2) > 5/4$ is proved earlier in the file. The absolute-value form packages that gap for certificates that compare distances rather than oriented differences.
proof idea
One short tactic block on top of the signed string margin. Record $c_{\mathrm{RS}} - (-3/2) > 5/4$ from that lemma; linear arithmetic gives positivity of the same difference; rewrite $\lvert\cdot\rvert$ via the positive-case absolute-value identity; discharge by the signed bound. No fresh arithmetic on $\varphi$ is performed here.
why it matters
Supplies the absolute string margin field of the leading-log discriminator certificate, and through the Track 3.B master cert feeds the gravity MasterTheorem statement that $c_{\mathrm{RS}}$ is observably distinct from both LQG and string canonical values. Together with the companion LQG absolute margin, it upgrades mere $\neq$ facts into theorem-grade observational margins (gap $> 1.25$ against string). The eight-tick octave (forcing step T7) enters only through the definition of $c_{\mathrm{RS}}$ as the squared washout prefactor $(1-\varphi^{-8})^2$; the SI entropy bridge itself is independent scaffolding closed earlier in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.