m1_SI
plain-language theorem explainer
Fixes the first test mass in the BMV parallel two-interferometer model geometry at $10^{-14}$ kg (Bose-et-al-2017 microdiamond scale). Downstream phase and entangling-invariant definitions cite it as a pure MODEL input. The body is a one-line real literal, not a derived claim.
Claim. Model parameter: the first equal test mass is $m_1 = 10^{-14}\,\mathrm{kg}$ in SI units, the Bose-et-al-2017-style microdiamond mass scale for the representative parallel two-interferometer geometry.
background
The module builds a certified BMV falsifier floor: under a Newtonian weak-field phase model plus a named geometry, the joint two-qubit branch state is non-product, with entangling invariant in a numeric band bounded away from $0 \bmod 2\pi$. A clean null at that geometry refutes the package, not every quantum-mediator theory.
Section 1 of the file is pure MODEL input: SI constants and geometry lengths. This declaration is mass 1 of the equal-mass pair. Its sibling is mass 2 at the same scale. Both feed the weak-field branch phases $\phi_{LL},\phi_{LR},\phi_{RL},\phi_{RR}$ and the invariant $\Delta\Phi = (G m_1 m_2 T/\hbar)(1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL})$.
Upstream depends_on edges that mention ledger mass are name collisions from the SevenGaps posting layer; they are not used in the body. The only content here is the real literal $1/10^{14}$.
proof idea
Definitional abbreviation: m1_SI is the real $1/10^{14}$. No lemmas, no tactics, no reduction. Downstream unfolds (e.g. deltaPhi_eq_rat) expand this literal together with $G$, $\hbar$, $m_2$, $T$, and the four separations, then close by norm_num on exact rationals.
why it matters
Anchors the numeric BMV geometry so the certified band is reproducible. Parents in this file: the four branch phases and deltaPhi, and through them deltaPhi_eq_rat (exact value $26696/47475$) and the entanglement/falsifier theorems that consume the invariant.
Per the module framing, BMV entanglement is predicted by any quantum mediator, so this package is excluded from the pillar-3 discriminator. It is the falsifier floor only. The mass scale is MODEL input, not forced by the T0–T8 chain or by amplitude-channel uniqueness; those force channel structure, not the magnitude of branch phases. Framework-level reading “clean null refutes RS” remains MODEL/OPEN until the Newtonian-magnitude premise is formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.