r_LR_SI
plain-language theorem explainer
Fixes the left–right diagonal branch-pair separation at 450 μm in the representative parallel two-interferometer BMV geometry. Downstream phase and entangling-invariant definitions cite this constant as a MODEL length input. The body is a single exact rational literal in SI metres.
Claim. In the named parallel two-interferometer geometry, the diagonal cross-pair (left–right) branch separation is the SI length $r_{LR} = 450 \times 10^{-6}\,\mathrm{m}$.
background
The module builds a certified BMV entanglement falsifier floor under a Newtonian weak-field phase model plus a fixed laboratory geometry. BMV entanglement is predicted by any quantum mediator, so the package is excluded from the pillar-3 discriminator; a clean null only refutes the named package (weak-field phases at this geometry), not the full RS framework without an unformalized magnitude premise.
Section 1 supplies four SI branch-pair distances. The collinear-adjacent Bose et al. identity is deliberately violated: $r_{LL}=r_{RR}=250,\mu\mathrm{m}$ with $r_{LR}=r_{RL}=450,\mu\mathrm{m}$ realises a parallel two-interferometer layout, not a linear adjacent chain. The sibling $r_{LL}$ note records that configuration choice.
These lengths enter the weak-field branch phase $\phi\propto G m_1 m_2 T/(\hbar r)$ and the entangling combination $1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL}$.
proof idea
Definition by exact rational literal: $450/10^6$ as a real. No lemmas, tactics, or proof obligations; pure MODEL geometry input parallel to $r_{LL}$, $r_{RR}$, and $r_{RL}$.
why it matters
Supplies the $r_{LR}$ slot in the four-distance geometry that feeds deltaPhi (the weak-field branch invariant $(G m_1 m_2 T/\hbar)(1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL})$) and the single-branch phase phase_LR. The exact rational theorem deltaPhi_eq_rat unfolds this constant with the other SI inputs and obtains $\Delta\phi=26696/47475$ by norm_num, placing the invariant in the certified band $[1/2,7/10]$ used by the non-product witness.
Within the module framing, that band is the falsifier floor: a measured product state at this geometry contradicts the package {weak-field phases + named geometry}. Framework-level falsification remains MODEL/OPEN because magnitude of the RS channel phases is not forced upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.