log_phi_lt_half
plain-language theorem explainer
Natural log of the golden ratio is strictly less than one half. Gravity and quantum-gravity workers cite it to place the RS leading-log black-hole coefficient above −1/4 and to open explicit margins against LQG (−1/2) and string (−3/2). The proof compares φ² = φ+1 against a decimal upper bound and exp(1), then uses log monotonicity and the power rule.
Claim. If $\varphi=(1+\sqrt{5})/2$ is the golden ratio, then $\log\varphi < 1/2$. Equivalently $2\log\varphi < 1$, so the RS leading-log coefficient $c_{\mathrm{RS}}=-(\log\varphi)/2$ satisfies $c_{\mathrm{RS}} > -1/4$.
background
Module Gravity.BlackHoleEntropySI closes Track 3.B of the quantum-gravity plan: SI lift of Bekenstein–Hawking leading entropy plus sharper discriminator margins against LQG and string-theory canonical leading-log values. The RS coefficient in this track is $c_{\mathrm{RS}}=-(\log\varphi)/2$ (from the ledger entropy expansion), not the cosmological $\eta_B$ prefactor of the same name.
The golden ratio $\varphi$ is forced in the Recognition chain as the self-similar fixed point (T6). Two elementary identities are used here: $\varphi^2=\varphi+1$ (the defining quadratic) and the tighter numerical bound $\varphi<1.62$ (from $\sqrt{5}<2.24$). Prior work already had the coarser private bound $\log\varphi<1$; this lemma sharpens it to $1/2$, which is exactly the threshold needed to exclude the LQG half-integer and to produce positive observational margins.
proof idea
Tactic proof by chained inequalities. Start from positivity of $\varphi$, the identity $\varphi^2=\varphi+1$, and $\varphi<1.62$. Rewrite to get $\varphi^2<2.62$. Compare against a fixed decimal lower bound on $e=\exp 1$ to conclude $\varphi^2<\exp 1$. Apply strict monotonicity of $\log$ on the positive reals, then rewrite $\log(\varphi^2)=2\log\varphi$ and $\log(\exp 1)=1$. A final linear arithmetic step yields $\log\varphi<1/2$.
why it matters
This is the numerical hinge for the Track 3.B discriminator package. Immediate corollaries are $c_{\mathrm{RS}}>-1/4$, the LQG margin $c_{\mathrm{RS}}-(-1/2)>1/4$, and the string margin $c_{\mathrm{RS}}-(-3/2)>5/4$. Those feed the master certificate BlackHoleEntropySICert and the numerical band $c_{\mathrm{RS}}\in(-1/4,0)$ in BlackHoleHorizonStates. Existing ledger work only proved $c_{\mathrm{RS}}\neq -1/2$ and $\neq -3/2$; without an explicit margin, experimental sensitivity cannot close the falsification gap. The bound also supports rung-phase-delay comparisons in DiscriminatorCert. Framework landmark: $\varphi$ from T6, used here purely as a real-analytic constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.