bmvAttachment
plain-language theorem explainer
BMV phase-rate attachment records the MAQRO-class tabletop Bose–Marletto–Vedral entanglement channel against the RS target band $[4.77,5.04]\times10^{-7}$ rad/s. Sensitivity is the band half-span; the RS target scale is the midpoint. The row is attached but flagged not currently sensitive. Downstream positivity certificates and the master falsifier-register cert cite this record. Pure structure instance with literal field fills.
Claim. The BMV phase-rate dataset attachment is the falsifier-register record with sector "BMV phase-rate sign and magnitude", dataset the MAQRO-class tabletop BMV entanglement-generation experiment, units $\mathrm{rad}/\mathrm{s}$, sensitivity $5.04\times10^{-7}-4.77\times10^{-7}$, RS target scale the midpoint $(4.77\times10^{-7}+5.04\times10^{-7})/2$, and currently-sensitive flag $\mathrm{false}$.
background
This module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master plan §7 falsifier register. Status is structural (zero sorry, zero new RS axioms): the point is falsifiability accounting, not empirical confirmation.
A dataset attachment packages six fields: sector label, named dataset or channel, units, a numerical sensitivity scale, an RS target scale (or band midpoint), and a Boolean saying whether present data already reach that target. Sensitivity and target are dimensionless unless units says otherwise; several future rows honestly set currently-sensitive to false.
For BMV, the target band is taken from the master plan and the reproducibility script bmv_phase_rate.py: $[4.77,5.04]\times10^{-7}$ rad/s. Foundation material on eight-tick phases ($k\pi/4$) and related phase structure sits behind the phase-rate prediction itself; this definition only stores the numerical accounting row for that channel.
proof idea
Definitional structure instance, not a proved theorem. Sector, dataset, and units are string literals. Sensitivity is the arithmetic width of the published band endpoints ($5.04\times10^{-7}-4.77\times10^{-7}$). The RS target scale is their midpoint average. The currently-sensitive flag is hard-coded false because MAQRO-class is treated as a future channel. No tactics, no lemmas, no obligations beyond typechecking the DatasetAttachment fields.
why it matters
Supplies the BMV row consumed by the positivity theorems on sensitivity and target scale (both discharged by norm_num after unfolding). Those facts are fields of the master certificate that every §7 falsifier-register row has a named dataset, positive sensitivity, and positive RS target, and they appear in the one-statement conjunction over all register rows.
In the Recognition verification layer this closes the BMV accounting slot without claiming present-day reach: the tabletop BMV / MAQRO phase-rate prediction is named, banded, and unit-tagged, ready for later sensitivity upgrades when the channel matures. It does not itself invoke T5–T8 or the RCL; it only pins the experimental side of a phase-rate falsifier that those foundations motivate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.