r_RL_SI
plain-language theorem explainer
Fixes the SI branch-pair distance for the RL (diagonal cross) pair in the named BMV two-interferometer geometry at exactly 450 micrometers. Anyone evaluating the weak-field phases or the entangling invariant at this model point cites it as a pure geometry input. The body is a single exact rational literal, not a derived quantity.
Claim. In the representative parallel two-interferometer geometry, the RL diagonal cross-pair separation is the exact SI length $r_{RL} = 450/10^{6}\,\mathrm{m} = 450\,\mu\mathrm{m}$.
background
The module builds a certified BMV falsifier floor: under a Newtonian weak-field phase model plus a fixed laboratory geometry, the pure two-qubit branch state is non-product, with the entangling invariant pinned in a numeric band away from $0 \bmod 2\pi$. A clean null at that geometry therefore refutes the package, not every quantum-mediator theory.
Section 1 of the file names the SI constants and the four branch-pair distances of a representative parallel two-interferometer layout. The RL entry is the diagonal cross pair (as opposed to the co-located LL/RR arms and the other cross pair LR). All four lengths feed the weak-field phase formula from BMVPositive and the combination that defines the branch invariant.
The module is explicit that BMV entanglement is predicted by any quantum mediator, so this package is excluded from the pillar-3 discriminator slot; it is only a falsifier floor for the named model package.
proof idea
Pure definition: the real constant is the exact rational $450/10^6$. No lemma applications, no tactics, no axioms. Downstream unfolds treat it as a numeric literal under norm_num.
why it matters
Supplies one of the four geometry inputs to the weak-field branch phase $\phi_{RL}$ and to the entangling invariant $\Delta\Phi = (G m_1 m_2 T/\hbar)(1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL})$.
Those feed deltaPhi_eq_rat, which evaluates $\Delta\Phi$ exactly to $26696/47475$ (about $0.562$ rad) by rational arithmetic on the named SI package, and thence the certified band and non-product theorems. Without a fixed $r_{RL}$, the geometric bracket and the falsifier floor are undefined.
Framework note: the algebra here is THEOREM; the claim that RS actually produces Newtonian weak-field phases of this magnitude at this geometry remains MODEL/OPEN, so a clean null refutes the package, not automatically the whole framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.