pageCurve_target_pos
plain-language theorem explainer
The Page-curve dataset attachment carries a strictly positive RS target scale. Auditors of the quantum-gravity falsifier register cite this to confirm that row is numerically well-formed before certification. The proof unfolds the attachment record and discharges 1.0 > 0 by numeric normalization.
Claim. The Page-curve falsifier attachment has positive RS target scale: if $D$ is that attachment, then $0 < D.\mathrm{rsTargetScale}$. Concretely the recorded target is $1.0$ (shape-discriminator units), so $0 < 1.0$.
background
This module attaches named observational channels and numerical scales to every row of the quantum-gravity master-plan §7 falsifier register. Attachment is structural accounting: a named dataset, a sensitivity scale, an RS target scale or band, and a flag for whether current data already reach that target. The records do not claim empirical confirmation of RS.
HasPositiveTargetScale is the predicate $0 < D.\mathrm{rsTargetScale}$ on a DatasetAttachment. The Page-curve row is a structural future channel: a future analog-gravity experiment must distinguish the triangular Page curve from monotone Hawking entropy growth. Its record sets sector "Page curve", units "shape discriminator", sensitivity $1.0$, and rsTargetScale := 1.0.
proof idea
Term-mode proof by unfolding. Expand HasPositiveTargetScale to the inequality $0 < D.\mathrm{rsTargetScale}$, substitute the Page-curve attachment (so the goal is $0 < 1.0$), and close with norm_num. No lemmas beyond definitional unfolding.
why it matters
Feeds the aggregate certificate falsifierDatasetRegisterCert, which bundles positivity of sensitivity and target scale for every named row (BMV, Hawking temperature, leading-log entropy, Page curve, echoes, $\Omega_\Lambda$, dark-energy $w$, QNMs, PTA, etc.). Without this fact the Page-curve slot cannot enter the register cert.
In the broader RS verification story this is falsifiability bookkeeping, not a derivation of the Page curve from the forcing chain (T0–T8) or the Recognition Composition Law. It only guarantees the structural row has a positive target so the register stays numerically honest. Closure status of the module is zero sorry and zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.