pageCurve_sensitivity_pos
plain-language theorem explainer
The Page-curve row of the quantum-gravity falsifier register carries a strictly positive numerical sensitivity. Anyone auditing completeness of the §7 dataset attachments cites this. The proof unfolds the attachment record and discharges 0 < 1 by norm_num.
Claim. The Page-curve dataset attachment (future analog-gravity experiment, shape discriminator) has strictly positive sensitivity: $0 < 1.0$.
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, and an honest flag on whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.
A DatasetAttachment packages sector, dataset name, units, sensitivity, and RS target scale. Positive sensitivity is the predicate $0 < D.\mathrm{sensitivity}$. The Page-curve attachment is a structural row: a future analog-gravity experiment must distinguish the triangular Page curve from monotone Hawking entropy increase, with sensitivity and RS target both set to $1.0$ in shape-discriminator units.
proof idea
One-line term-style proof. Unfold the positive-sensitivity predicate and the Page-curve attachment record, exposing the concrete inequality $0 < 1.0$. Discharge it by norm_num. No lemmas beyond definitional unfolding.
why it matters
Closes the sensitivity half of the Page-curve row in the falsifier-register certificate. Downstream, falsifierDatasetRegisterCert bundles this fact with the other sector positivity proofs, and falsifier_dataset_register_one_statement packages the full conjunction: every register row has positive dataset sensitivity and positive RS target scale.
In the Recognition Science verification layer this is bookkeeping for quantum-gravity falsifiability, not a derivation of the Page curve itself. It records that the structural Page-curve prediction is assigned a positive discriminator scale so the register cannot silently drop the row. Zero sorry, zero new RS axioms; pure numerical hygiene on the attachment table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.