hawking_target_pos
plain-language theorem explainer
The Hawking-temperature falsifier row carries a strictly positive Recognition Science target scale (unity in fractional T_H units). Anyone assembling the quantum-gravity falsifier register certificate cites this positivity check. The proof unfolds the attachment record and discharges 0 < 1 by numeric normalization.
Claim. The Hawking temperature dataset attachment has positive RS target scale: writing $D$ for that attachment, $0 < D_{\mathrm{rsTargetScale}}$. Concretely $D_{\mathrm{rsTargetScale}} = 1.0$ (fractional $T_H$), so the inequality holds.
background
This module attaches named observational channels, numerical sensitivities, and RS target scales to every row of the quantum-gravity master-plan §7 falsifier register. Attachments are conservative accounting records: they name a channel, a sensitivity, an RS target or band, and whether present data already reach that target. They do not claim empirical confirmation of RS.
A dataset attachment is a record with sector, dataset name, units, sensitivity, and rsTargetScale. The predicate "has positive target scale" is simply $0 < D_{\mathrm{rsTargetScale}}$. The Hawking temperature attachment is the row for future analog-gravity or primordial black-hole temperature measurements; its falsifier threshold is 10% on the leading Hawking formula, with sensitivity $0.10$ and RS target scale $1.0$ in fractional $T_H$ units.
proof idea
One-line tactic proof. Unfold the positivity predicate and the Hawking attachment definition, exposing the concrete inequality $0 < 1.0$. Discharge it with norm_num. No lemmas beyond definitional unfolding are required.
why it matters
The parent certificate falsifierDatasetRegisterCert bundles positivity of sensitivity and target scale for every attached row (BMV, Hawking, leading-log entropy, page curve, echoes, $\Omega_\Lambda$, dark-energy $w$, QNMs, PTA, etc.). This theorem fills the Hawking target slot of that certificate.
In the falsifiability accounting of the module, a row is only fully attached when both sensitivity and RS target scale are strictly positive. The Hawking row is deliberately future-facing (analog gravity / primordial BH), so the target-scale check is structural bookkeeping rather than a claim that current data already test $T_H$ at the 10% level. It keeps the register closed with zero sorry and no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.