leadingLog_target_pos
plain-language theorem explainer
The leading-log entropy coefficient attachment has a strictly positive RS target scale. Auditors of the quantum-gravity falsifier register cite this to confirm that row is well-formed before the full certificate is assembled. The proof unfolds the positivity predicate and the attachment record, then closes 0 < 0.05 by numerical normalization.
Claim. The dataset attachment for the leading-log entropy coefficient satisfies the positive RS target-scale requirement: its recorded RS target scale is strictly greater than zero.
background
This module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master plan §7 falsifier register. A row is attached when it carries a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag for whether current data already probe the RS target. The purpose is falsifiability accounting, not empirical confirmation.
HasPositiveTargetScale is the predicate that a dataset attachment $D$ obeys $0 < D.\mathrm{rsTargetScale}$. The leading-log entropy attachment records the sector as the leading-log entropy coefficient, channels LIGO/Virgo ringdown and future LISA/Einstein Telescope QNM spectroscopy, sensitivity $0.10$, and RS target scale $0.05$. Its doc notes the target coefficient $c_{\mathrm{RS}} = -\log\varphi/2 \approx -0.2406$, with sensitivity $0.10$ chosen to separate RS from LQG's $-1/2$ margin.
proof idea
Short tactic proof. Unfold the positivity predicate and the leading-log attachment definition to expose the concrete inequality $0 < 0.05$, then close it with norm_num. No lemmas beyond those unfolds are required.
why it matters
Feeds falsifierDatasetRegisterCert, which packages positivity certificates for every attached row (both sensitivity and target). Without this fact the leading-log row cannot enter the structural certificate that the register is fully populated with positive scales. It lives in the verification layer that makes the QG falsifier register machine-checkable: zero sorry, zero new RS-specific axioms. The leading-log coefficient is an RS prediction tied to $\varphi$ (forcing-chain T6 fixed point), so positivity of the stored target scale is a minimal well-formedness gate before any comparison to LIGO/Virgo or future LISA/ET spectroscopy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.