strongField_target_pos
plain-language theorem explainer
The strong-field falsifier-register attachment carries a strictly positive RS target scale. Cassini Shapiro-delay, EHT M87*, and GRAVITY S2 status theorems cite it, as does the master dataset-register certificate. The proof is a pure numerical check: unfold the positivity predicate and the attachment record, then discharge 0 < target by norm_num.
Claim. The strong-field dataset attachment $D$ in the quantum-gravity falsifier register satisfies $0 < D.(\mathrm{rs\,target\,scale})$.
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 only: a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag for whether current data already reach that target. No row claims empirical confirmation of RS.
HasPositiveTargetScale is the predicate $0 < D.\mathrm{rsTargetScale}$ on a DatasetAttachment record. The strong-field row bundles the classical strong-field tests listed in the module header (Cassini Shapiro delay $\gamma-1$, EHT M87* ring/shadow, GRAVITY S2 Schwarzschild precession). Sibling positivity lemmas play the same role for BMV phase rate, Hawking temperature, leading-log entropy, Page curve, echoes, $\Omega_\Lambda$, $w$, QNMs, and PTA channels.
Upstream scale machinery (phi-ladder powers, PRC positivity) is imported elsewhere in the stack; this lemma only needs the concrete numeric field stored on the strong-field attachment.
proof idea
Term-mode proof by unfolding. Expand HasPositiveTargetScale to the inequality $0 < D.\mathrm{rsTargetScale}$, expand strongFieldAttachment to expose the stored real constant, then close with norm_num. No lemmas beyond definitional reduction and numeric evaluation.
why it matters
Closes the target-scale half of the strong-field row in the falsifier-register certificate. Downstream, cassini_dataset_attachment_status, ehtM87_dataset_attachment_status, and gravityS2_dataset_attachment_status each package this fact with sensitivity positivity and the explicit currentlySensitive = false flag. The master falsifierDatasetRegisterCert aggregates the same positivity obligation across every §7 row.
In the broader RS verification story this is bookkeeping, not dynamics: it makes the strong-field prediction numerically comparable to Cassini, EHT, and GRAVITY data without asserting that those experiments already constrain the RS target. That honesty flag is part of the structural theorem status of the module (0 sorry, 0 new RS axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.