hawking_sensitivity_pos
plain-language theorem explainer
The Hawking-temperature falsifier row records a strictly positive numerical sensitivity (10% fractional on T_H). Auditors of the quantum-gravity falsifier register cite it to show that attachment is non-vacuous. The proof unfolds the positivity predicate and the attachment record, then discharges 0 < 0.10 by numeric normalization.
Claim. The Hawking-temperature dataset attachment has strictly positive sensitivity: its recorded fractional $T_H$ sensitivity equals $0.10$, and $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. Attachments are deliberately conservative: a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag on whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.
HasPositiveSensitivity is the predicate $0 < D.sensitivity$ on a dataset attachment. The Hawking-temperature attachment sets sector "Hawking temperature", dataset "Future analog-gravity or primordial-BH temperature measurement", units fractional $T_H$, sensitivity $0.10$, and RS target scale $1.0$. Its doc states the falsifier threshold is 10% on the leading Hawking temperature formula, aimed at future analog-gravity or primordial-BH searches.
proof idea
One-line tactic proof. Unfold the positivity predicate (which is $0 < D.sensitivity$) and the Hawking-temperature attachment (which fixes sensitivity to $0.10$). The goal reduces to $0 < 0.10$, discharged by norm_num. No lemmas beyond definitional unfolding.
why it matters
Feeds the register certificate falsifierDatasetRegisterCert as the hawking_sensitivity field, and appears in the conjunctive one-statement theorem that every falsifier-register row has positive dataset sensitivity and positive RS target scale. That one-statement form is the structural closure of the module (0 sorry, 0 RS-internal axioms).
In the Recognition framework this is bookkeeping for quantum-gravity falsifiability, not a derivation of Hawking radiation from the forcing chain (T0–T8) or the Recognition Composition Law. It only certifies that the Hawking-temperature row is numerically well-formed so the register cannot hide a zero-sensitivity placeholder. Downstream consumers treat it as a certificate field, not as an empirical claim that $T_H$ has been measured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.