HasPositiveTargetScale
plain-language theorem explainer
A dataset attachment satisfies the positive RS target-scale predicate exactly when its recorded Recognition Science target scale is strictly positive. Falsifier-register status theorems (Cassini, dark-energy w, EHT M87*, EPTA, and siblings) cite it to certify that each named row carries a usable numerical RS target. The body is a one-line definitional unfolding of that inequality.
Claim. A dataset attachment $D$ has positive RS target scale when $0 < s_{\mathrm{RS}}(D)$, where $s_{\mathrm{RS}}(D)$ is the dimensionless (unless units say otherwise) Recognition Science target scale stored on $D$.
background
The module attaches named observational channels to every row of the quantum-gravity master-plan §7 falsifier register. Each attachment is a record with sector, dataset name, units, numerical sensitivity, an RS target scale or band, and a Boolean flag saying whether current data already reach that target. The purpose is falsifiability accounting, not empirical confirmation: rows name which experiment tests which prediction and at what reported precision.
DatasetAttachment stores sensitivity and rsTargetScale as real numbers (dimensionless unless units says otherwise) and currentlySensitive as an honest flag. For several future channels the flag is false: the dataset is named but not yet sensitive enough to test a φ-suppressed target. The companion predicate requires positive sensitivity; this one requires a positive RS target scale so that comparisons against the target are well-posed.
proof idea
Definitional, not a proved theorem. The predicate is the proposition $0 < D.\mathrm{rsTargetScale}$. Downstream status lemmas discharge it by pairing a concrete positivity lemma for the named row's target constant with the corresponding sensitivity positivity fact and a rfl on the currentlySensitive flag.
why it matters
Every named falsifier-register status theorem in the verification layer conjoins this predicate with positive sensitivity and an explicit currently-sensitive flag. Downstream consumers include cassini_dataset_attachment_status, darkEnergyW_dataset_attachment_status, ehtM87_dataset_attachment_status, epta_dataset_attachment_status, and the corresponding likelihood certificate structures (Cassini strong-field, dark-energy $w$ Planck, EHT M87*, EPTA PTA, and further siblings).
Without a strictly positive RS target, residual-versus-sigma comparisons in those certificates would be meaningless. The definition therefore closes the structural side of falsifiability accounting for the register: each row must carry a usable numerical RS scale before any claim about reach or non-reach is stated. It does not itself encode φ-ladder mass formulas or T0–T8 forcing; it only polices the numerical hygiene of the attachment records those predictions feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.