bmv_sensitivity_pos
plain-language theorem explainer
The BMV tabletop phase-rate dataset row has strictly positive numerical sensitivity. Verification and falsifiability accounting cite this when assembling the quantum-gravity register certificate. The proof unfolds the attachment record and closes the inequality by numerical normalization on the half-width of the target band.
Claim. The BMV / MAQRO-class phase-rate dataset attachment has positive sensitivity: if $s = 5.04\times 10^{-7} - 4.77\times 10^{-7}$ (rad/s half-width of the target band), then $0 < s$.
background
This module attaches named observational channels and numerical scales to every row of the quantum-gravity master-plan falsifier register. Each row is a DatasetAttachment: sector, dataset string, units, a real sensitivity, an RS target scale, and a boolean saying whether current data already reach that target. The purpose is falsifiability accounting, not empirical confirmation of RS.
Positive sensitivity is the predicate $0 < D.\mathrm{sensitivity}$. The BMV row records a MAQRO-class tabletop entanglement-generation channel in rad/s. Its sensitivity is the half-width of the master-plan target band $[4.77, 5.04]\times 10^{-7}$ rad/s; the RS target scale is the band midpoint. The row is attached but flagged not yet currently sensitive, since MAQRO-class reach is still future.
proof idea
Term-mode proof in two steps. Unfold the positivity predicate and the BMV attachment definition so the goal is the concrete inequality $0 < 5.04\times 10^{-7} - 4.77\times 10^{-7}$. Discharge that arithmetic fact with norm_num. No lemmas beyond the local definitions are required.
why it matters
This is one of the per-row positivity lemmas that pack into the register certificate structure and into the one-statement conjunction asserting every falsifier-register row has positive sensitivity and positive RS target scale. Without it, the structural theorem that the dataset attachments are well-formed (zero sorry, zero new RS axioms) cannot close for the BMV phase-rate channel.
In the broader Recognition framework this is verification infrastructure, not a forcing-chain step: it makes the BMV phase-rate sign-and-magnitude prediction auditably comparable to a named experiment at a stated precision. Downstream consumers only need the certificate fields; they do not re-derive the half-width positivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.