strongField_sensitivity_pos
plain-language theorem explainer
The strong-field falsifier row (Cassini Shapiro delay, GRAVITY S2, EHT M87*) carries a strictly positive observational sensitivity, namely Cassini's fractional metric-deviation scale 2.3×10⁻⁵. Anyone citing the quantum-gravity falsifier register or the Cassini/EHT/S2 attachment-status lemmas needs this positivity fact. The proof is a one-line unfold-and-norm_num check on the recorded sensitivity field.
Claim. The strong-field dataset attachment (Cassini Shapiro delay; GRAVITY S2 precession; EHT M87* shadow), with sensitivity $2.3\times 10^{-5}$ in fractional metric-deviation units, satisfies $0 < \text{sensitivity}$.
background
The module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master-plan §7 falsifier register. Attachment means a named dataset, a sensitivity scale, an RS target scale, and an honest flag for whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.
A dataset attachment is a record with sector, dataset string, units, sensitivity, and RS target scale. Positive sensitivity is the predicate $0 < D.\mathrm{sensitivity}$. The strong-field row stores Cassini's PPN-$\gamma$ precision $2.3\times 10^{-5}$ as the most precise current solar-system strong/weak-field number, while the dataset string lists the full channel set (Cassini, GRAVITY S2, EHT M87*). The RS target scale on that row is $6.376\times 10^{-10}$.
proof idea
Term-mode proof by unfolding. Expand the positive-sensitivity predicate to $0 < D.\mathrm{sensitivity}$, substitute the strong-field attachment record (whose sensitivity field is the literal $2.3\times 10^{-5}$), and discharge the resulting numerical inequality by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This positivity fact is a required conjunct in the Cassini, EHT M87*, and GRAVITY S2 dataset-attachment status theorems, each of which packages positive sensitivity, positive RS target scale, and the explicit flag currentlySensitive = false. It also feeds the aggregate falsifier-register certificate and the one-statement theorem that every register row has positive sensitivity and positive RS target.
In the Recognition framework this is structural verification infrastructure: it makes the strong-field / precision-GR sector of the falsifier register machine-checkably non-vacuous. It does not claim that Cassini, EHT, or GRAVITY have confirmed RS; the downstream status lemmas deliberately mark the row as not currently sensitive to the RS target ($6.376\times 10^{-10}$ vs sensitivity $2.3\times 10^{-5}$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.