m2_SI
plain-language theorem explainer
Second equal test mass in the representative BMV two-interferometer geometry, fixed at $10^{-14}$ kg in SI units. Anyone computing the four weak-field branch phases or the entangling invariant at the named model point cites this constant. It is a pure numeric definition: the real literal $1/10^{14}$, with no proof content.
Claim. In the representative parallel two-interferometer geometry, the second test mass is the SI value $m_2=10^{-14}\,\mathrm{kg}$, taken equal to the first test mass.
background
The BMVFalsifierBand module packages a certified entanglement witness for a Bose–Marletto–Vedral style parallel two-interferometer geometry. Panel framing is explicit: BMV entanglement is predicted by any quantum mediator, so the package is a falsifier floor, not a pillar-3 discriminator between Recognition Science and GR+QFT.
Section 1 of the module fixes MODEL inputs: SI constants $G$, $\hbar$, equal test masses $m_1=m_2$, coherence time $T$, and the four branch separations $r_{LL},r_{LR},r_{RL},r_{RR}$. Each branch phase is the Newtonian weak-field formula from BMVPositive, $\phi=G m_1 m_2 T/(\hbar r)$, and the entangling invariant is the signed combination of the four reciprocal separations.
This declaration is the second mass slot in that named geometry. The doc-comment states the model choice $m_2=10^{-14},\mathrm{kg}$ with equal test masses.
proof idea
Definitional assignment only. The body is the real literal $1/10^{14}$; there is no tactic proof, no lemma application, and no unfolding obligation beyond ordinary real arithmetic when downstream norm_num goals expand the geometry.
why it matters
Feeds every named branch phase at the model point (phase_LL, phase_LR, phase_RL, phase_RR) and the entangling invariant deltaPhi, which is definitionally the weak-field branch invariant of BMVPositive at those SI inputs. Downstream, deltaPhi_eq_rat unfolds this mass (with $G$, $\hbar$, $m_1$, $T$, and the four radii) and obtains the exact rational $26696/47475$ by kernel-checked norm_num.
That rational sits inside the certified band $[1/2,7/10]$, bounded away from $0\bmod 2\pi$, which underwrites the non-product (nonzero amplitude-matrix determinant) theorems of the module. The mass choice is MODEL input, not a forced RS constant; the module doc keeps the magnitude premise MODEL/OPEN relative to the Track 2 channel-uniqueness results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.