hawkingTemperatureAttachment
plain-language theorem explainer
Registers the Hawking-temperature row of the quantum-gravity falsifier register: 10% fractional sensitivity on the leading T_H formula, linked to future analog-gravity or primordial black-hole temperature measurements, with RS target scale 1.0 and current sensitivity flagged false. Falsifiability accounting and the master dataset certificate cite this attachment. It is a pure structure instance filling fixed numerical fields.
Claim. The Hawking-temperature dataset attachment is the record with sector "Hawking temperature", dataset channel "Future analog-gravity or primordial-BH temperature measurement", units fractional $T_H$, numerical sensitivity $0.10$, RS target scale $1.0$, and $\mathrm{currentlySensitive}=\mathrm{false}$.
background
The 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: each row needs a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag whether present data already reach that target. Purpose is falsifiability accounting, not empirical confirmation.
A dataset attachment is a six-field record: sector string, dataset name, units string, dimensionless (unless units say otherwise) sensitivity and RS target scale, and a Boolean currently-sensitive flag. For several future rows the flag is honestly false: the channel is named but not yet precise enough to test the φ-suppressed target.
This row sits beside sibling attachments (BMV, leading-log entropy, Page curve, echoes, Ω_Λ, dark-energy w, QNMs, PTA). The Hawking row specifically records a 10% threshold on the leading Hawking temperature formula for future analog-gravity or primordial-BH searches.
proof idea
Pure definitional structure instance. The six fields of DatasetAttachment are assigned by literals: sector and dataset strings, units "fractional T_H", sensitivity 0.10, rsTargetScale 1.0, currentlySensitive false. No lemmas, tactics, or computation beyond the record constructor.
why it matters
Fills the Hawking-temperature slot required by the master certificate FalsifierDatasetRegisterCert, which demands every §7 falsifier-register row have a named dataset, positive sensitivity, and positive RS target scale. Downstream positivity lemmas unfold this attachment and discharge HasPositiveSensitivity and HasPositiveTargetScale by norm_num; the one-statement theorem conjoins those facts with the other sector rows.
In the Recognition framework this is bookkeeping for quantum-gravity falsifiability, not a derivation of T_H itself. It makes explicit that a 10% fractional test of the leading Hawking formula is the planned discriminator, while current data are not yet sensitive. Sibling leading-log entropy uses a related c_RS coefficient; this temperature row stays at target scale 1.0 with the future-channel flag false. Zero sorry, zero new RS axioms in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.