leadingLog_sensitivity_pos
plain-language theorem explainer
The leading-log black-hole entropy coefficient row carries a strictly positive numerical sensitivity (0.10). Falsifier-register auditors cite this to certify that the LIGO/Virgo and future LISA/ET QNM spectroscopy channel is observationally nontrivial against the RS target. The proof is a direct numerical check after unfolding the attachment record.
Claim. The leading-log entropy coefficient dataset attachment satisfies the positive-sensitivity requirement: its reported sensitivity scale $0.10$ obeys $0 < 0.10$.
background
This module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master-plan §7 falsifier register. An attachment is a record with sector, dataset name, units, a sensitivity scale, an RS target scale, and an honesty flag on whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.
Positive sensitivity is the predicate $0 < D.sensitivity$ on such a record. The leading-log entropy attachment records the coefficient row with target $c_{RS} = -\log\varphi/2 \approx -0.2406$, dataset channel "LIGO/Virgo ringdown and future LISA/Einstein Telescope QNM spectroscopy", sensitivity $0.10$, and RS target scale $0.05$. That sensitivity is chosen to distinguish RS from the LQG margin near $-1/2$ (gap $>0.25$).
proof idea
Term-mode proof: unfold the positive-sensitivity predicate and the leading-log attachment definition, exposing the concrete inequality $0 < 0.10$, then discharge it by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This lemma is one of the sensitivity witnesses packed into the falsifier dataset register certificate, which bundles positive-sensitivity and positive-target proofs for every attached row (BMV, Hawking temperature, leading-log entropy, page curve, echoes, and the rest). It also appears in the one-statement conjunction asserting that all falsifier-register rows have positive dataset sensitivities and positive RS target scales.
Within Recognition Science verification, the leading-log coefficient is a concrete QNM/spectroscopy falsifier: RS predicts $c_{RS}\approx -0.2406$, safely separated from LQG's $-1/2$. Certifying that the attached sensitivity is positive keeps the register honest: the row is observationally live, not a vacuous placeholder. The module is structural (zero sorry, zero new RS axioms); this fact is a small but required brick in that closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.