bmv_target_pos
plain-language theorem explainer
The BMV/MAQRO phase-rate falsifier row has a strictly positive RS target scale (midpoint of the [4.77, 5.04]×10⁻⁷ rad/s band). Anyone assembling the quantum-gravity falsifier register certificate cites this to discharge the target-positivity field for that row. The proof is a two-step unfold-and-norm_num check on the literal midpoint.
Claim. For the BMV tabletop / MAQRO-class phase-rate dataset attachment, the recorded RS target scale satisfies $0 < \mathrm{rsTargetScale}$. Explicitly, with target band $[4.77, 5.04]\times 10^{-7}\,\mathrm{rad/s}$, the midpoint $(4.77+5.04)\times 10^{-7}/2$ is positive.
background
The module attaches named observational channels and numerical scales to every row of the quantum-gravity master-plan §7 falsifier register. Each DatasetAttachment records sector, dataset string, units, a numerical sensitivity, an RS target scale (or band representative), and a boolean for whether current data already reach that target. The purpose is falsifiability accounting, not empirical confirmation.
HasPositiveTargetScale is the predicate $0 < D.\mathrm{rsTargetScale}$. The BMV row is the tabletop / MAQRO-class phase-rate channel: units rad/s, sensitivity equal to the half-width of the published band, and rsTargetScale the band midpoint $(4.77+5.04)\times 10^{-7}/2$. The row is attached but flagged not currently sensitive, since MAQRO-class reach is still future.
proof idea
Term-mode proof by unfolding. Expand HasPositiveTargetScale to the inequality $0 < \mathrm{rsTargetScale}$, expand bmvAttachment to expose the literal midpoint definition, then discharge the numerical inequality with norm_num. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the bmv_target field of falsifierDatasetRegisterCert, the structural certificate that every falsifier-register row has positive sensitivity and positive RS target scale. Together with the sibling sensitivity positivity lemma for the same attachment, it closes the BMV slot in the zero-sorry register. In the broader RS verification story this is bookkeeping for a φ-ladder phase-rate prediction (master-plan / bmv_phase_rate.py band), not a derivation of the band itself; it makes the target scale machine-checkably positive so the register cannot silently carry a non-positive or missing target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.