pageCurveAttachment
plain-language theorem explainer
Registers the Page-curve falsifier row: a future analog-gravity experiment that must separate a triangular Page curve from monotone Hawking entropy growth. Sensitivity and RS target scale are both set to 1.0 in shape-discriminator units, with current data marked not yet sensitive. Cited by the master falsifier-register certificate and the one-statement positivity theorem. Pure structure literal; no proof obligations.
Claim. The Page-curve row of the quantum-gravity falsifier register is the dataset attachment with sector "Page curve", dataset "Future analog-gravity Page-curve experiment", units "shape discriminator", dimensionless sensitivity $1.0$, 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 names a channel, a sensitivity scale, an RS target scale or band, and an honest flag for whether present data already reach that target. The purpose is falsifiability accounting, not empirical confirmation.
A DatasetAttachment is a six-field record: sector string, dataset name, units, real sensitivity, real RS target scale, and a Boolean currentlySensitive. Sensitivity and target are dimensionless unless units say otherwise. For several future rows the flag is honestly false: the channel is named but not yet precise enough to test a φ-suppressed prediction.
The Page-curve row is structural. The required experiment must distinguish the triangular Page curve (entropy that rises then falls) from monotone Hawking entropy increase in an analog-gravity setting.
proof idea
Definition by structure literal. The six fields of the dataset-attachment record are filled with fixed strings and numerals: sector and dataset name the future analog-gravity Page-curve channel; units are "shape discriminator"; both sensitivity and RS target scale equal 1.0; currentlySensitive is false. No lemmas, tactics, or computation.
why it matters
Closes the Page-curve slot in the §7 falsifier register so the master certificate can assert that every row has a named dataset, positive sensitivity, and positive RS target. Downstream, pageCurve_sensitivity_pos and pageCurve_target_pos discharge the positivity obligations by unfolding this literal and norm_num. Those facts feed FalsifierDatasetRegisterCert and the one-statement conjunction falsifier_dataset_register_one_statement.
In the broader RS picture this is an accounting hinge, not a derivation of the Page curve itself. It records that a shape-discriminator experiment (triangular vs monotone entropy) is the intended falsifier, with unit target scale and no claim of present sensitivity. Sibling rows cover BMV, Hawking temperature, leading-log entropy, echoes, Ω_Λ, dark-energy w, QNMs, and PTA channels under the same structural discipline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.