HasPositiveSensitivity
plain-language theorem explainer
A dataset attachment has positive sensitivity when its reported numerical sensitivity scale is strictly greater than zero. Verification certificates for Cassini, Planck dark-energy w, EHT M87*, and PTA rows cite this predicate to guarantee that the observational channel is not a vacuous zero-precision stub. The body is a one-line inequality on the sensitivity field of the attachment record.
Claim. A falsifier-register dataset attachment $D$ has positive sensitivity when $0 < D.\mathrm{sensitivity}$, where sensitivity is the reported numerical precision scale of the named observational channel (dimensionless unless units say otherwise).
background
The module attaches concrete named datasets and numerical sensitivity records to every row of the quantum-gravity master plan §7 falsifier register. An attachment is a record with sector, dataset name, units, a real sensitivity scale, an RS target scale or band, and a boolean flag saying whether current data already reach that target.
Sensitivity and RS target scale are dimensionless unless the units field says otherwise. The module is deliberately conservative: attachment means the channel is named and quantified, not that RS has been confirmed. Anchor examples include Planck 2018 $\Omega_\Lambda$, Cassini Shapiro delay $\gamma-1$, EHT M87* ring diameter, and NANOGrav/EPTA stochastic-background records.
This predicate is the first of two positivity gates (the sibling is positive RS target scale). Together they keep zero or nonsense scales out of downstream likelihood certificates.
proof idea
Pure definitional abbreviation: the proposition is exactly the inequality $0 < D.\mathrm{sensitivity}$ on the real field of the attachment structure. No lemmas, no tactics. Downstream status theorems discharge it by pairing a concrete positivity lemma (e.g. strongField_sensitivity_pos) with the corresponding target-scale positivity and a reflexivity proof of the currentlySensitive flag.
why it matters
Falsifiability accounting in Recognition Science requires every §7 register row to carry a non-vacuous observational precision. This predicate is the shared gate used by Cassini strong-field, dark-energy $w(z)$ Planck, EHT M87* strong-field, and EPTA PTA attachment-status theorems, each of which asserts positive sensitivity, positive RS target scale, and an honest currently-sensitive flag (often false for $\varphi$-suppressed targets).
Those status theorems feed the corresponding likelihood certificate structures (Cassini, DarkEnergyW, EHTM87, EPTA), which package residual-vs-sigma comparisons. The definition therefore sits at the base of the verification stack that turns the master-plan falsifier list into machine-checkable dataset attachments without claiming empirical confirmation of RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.