module module moderate

`IndisputableMonolith.Gravity.QuantumChannel.BMVFalsifierBand`

Module assembling SI-unit BMV protocol parameters and branch phases into a concrete falsifier band for the Recognition gravity channel. Experimentalists and quantum-gravity auditors cite it to convert the abstract nonzero-Δφ claim into a numerical window. Structure is definitional: CODATA/SI constants, geometry radii, and phase evaluations, importing the BMV-positive and mediator/locality theorems.

claimFix SI inputs $G$, $\hbar$, masses $m_1,m_2$, duration $T$, and branch separations $r_{LL},r_{RR},r_{LR},r_{RL}$. Define the BMV gravitational phases $\phi_{LL},\phi_{LR},\phi_{RL}$ (and the implied $\Delta\phi$ combination) so that a measured phase outside the predicted band would falsify the linear cost-gradient quantum channel.

background

Recognition Science Gravity IV treats gravity as a quantum channel on the ledger: the linear cost-gradient of LedgerSuperposition imprints a branch-dependent phase on a two-mass, two-path (BMV-style) interferometer. Upstream, BMV-Positive (Theorem 3) states that the entangling combination $\Delta\phi$ is generically nonzero, so the joint state is non-product. No-Classical-Mediator and Substrate-Local-Access close Tracks 2.D and 2.C: under T0–T8 there is no classical mediator, and measurement access remains substrate-local.

This module does not reprove those structural facts. It supplies the SI yardsticks and geometry needed to turn $\Delta\phi\neq 0$ into a lab-facing band. $G$ is the CODATA Newtonian constant entered as the exact rational $6674/10^{14}$ (measured input, not an RS derivation). Companion constants $\hbar$, masses, evolution time $T$, and the four branch radii $r_{ij}$ fix the Newtonian phase integrals along each pair of paths.

proof idea

Definition module, not a theorem package. It declares SI literals (G_SI, hbar_SI, masses, T_SI, four $r_{ij}$) and evaluates named phases phase_LL, phase_LR, phase_RL from those inputs. Logical force comes from the imported modules: BMV-Positive supplies the sign/nonzero claim for $\Delta\phi$; No-Classical-Mediator and Substrate-Local-Access bar classical-channel loopholes. No tactic proof body lives here beyond whatever trivial equalities pin the rationals and phase formulas.

why it matters in Recognition Science

Closes the last mile from Gravity IV Theorem 3 (BMV-positive entangling phase) to a falsifiable numerical window. Without SI phases and geometry, $\Delta\phi\neq 0$ stays formal; with them, a BMV-type run can confirm or kill the linear cost-gradient channel. Sits downstream of Tracks 2.C–2.D (substrate locality and no classical mediator under T0–T8), so a band violation cannot be blamed on a classical mediator or nonlocal readout. Used_by is empty in the graph: this is a leaf calibration surface for experiment design and for any later quantitative corollary that quotes the predicted phase window. Landmark link: the channel itself is forced by the Recognition composition law and the T0–T8 chain; the band only translates that channel into SI units.

scope and limits

Does not derive $G$ or $\hbar$ from RS; $G$ is CODATA measured input.
Does not reprove BMV-Positive, no-classical-mediator, or substrate locality.
Does not claim a full experimental protocol, noise model, or decoherence budget.
Does not fix unique masses, $T$, or radii; those are parameter inputs.
Does not assert the band is already observationally tested.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.QuantumChannel.BMVPositive module_import
IndisputableMonolith.Gravity.QuantumChannel.NoClassicalMediator module_import
IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess module_import

declarations in this module (35)

def G_SI L101
def hbar_SI L107
def m1_SI L111
def m2_SI L115
def T_SI L119
def r_LL_SI L132
def r_RR_SI L137
def r_LR_SI L142
def r_RL_SI L147
def phase_LL L152
def phase_LR L156
def phase_RL L160
def phase_RR L164
def deltaPhi L171
theorem branchPhaseInvariant_eq_deltaPhi L177
theorem deltaPhi_eq_rat L189
theorem deltaPhi_ge_half L196
theorem deltaPhi_le_seven_tenths L200
theorem deltaPhi_pos L204
theorem seven_tenths_lt_two_pi L209
theorem deltaPhi_lt_two_pi L214
theorem deltaPhi_not_congruent_zero L222
theorem rs_bmv_witness_band L252
theorem rs_bmv_geometry_entangled L268
theorem rs_amplitude_channel_unique L310
theorem bmv_band_entanglement L341
theorem clean_null_refutes_rs L376
theorem same_branch_phases_same_BMV_witness L398
structure BMVFalsifierStatus L425
def bmvFalsifierStatus L439
theorem bmvFalsifierStatus_witness_band_certified L445
theorem bmvFalsifierStatus_amplitude_channel_theorem_cited L448
theorem bmvFalsifierStatus_falsifier_named L451
theorem bmvFalsifierStatus_excluded_from_pillar3 L454
theorem bmvFalsifierStatus_all L459