Gravity No Graviton Unit Bridge Bmv Phase Rate Si Band Endpoints

The unit bridge

The declaration bmvPhaseRateSI_band_endpoints is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that a certain dimensionless number, the RS coupling κ_rs, which is fixed to 8φ⁵ and lies in a band from 85.6 to 90.4, can be converted into a physical rate measured in SI units. That rate is the entangling phase rate, the speed at which two masses cause quantum entanglement to accumulate between them due to gravity, an effect proposed by Bose, Marletto, and Vedral as a tabletop test of quantum gravity.

The theorem's content is a unit bridge. In RS-native units, the reduced Planck constant ħ equals φ⁻⁵ and Newton's constant G equals φ⁵/π, so the ratio G/ħ equals φ¹⁰/π, a closed-form number fixed by the golden ratio φ alone. The entangling phase rate in those native units is (G m₁ m₂ / ħ) · g, where g is a geometry factor depending on the distances between the two masses and their two possible paths. The theorem proves that this native rate, multiplied by a calibration constant Uconv, gives the SI value, and that the band on κ_rs propagates linearly to that SI rate.

The proof is conditional. The calibration constant Uconv is not derived; it is an input, an inhabitant of a structure called ExternalCalibration that lives at a named open frontier. Until that frontier is discharged, the theorem is a conditional theorem with the calibration as a given. The theorem does not claim that the calibration has been made, nor that the entangling phase rate has been measured. It establishes the algebraic bridge: given the calibration, the SI rate follows from the RS-native closed form.

What the theorem does not claim is equally precise. It does not prove that gravity is quantized, nor that the BMV experiment will succeed. It does not derive the calibration constant from first principles. It does not claim that the band (85.6, 90.4) is a prediction of a measurement; it is a band on the dimensionless coupling that propagates to the phase rate. The theorem is a formal statement about the relationship between two unit systems, not an empirical result.

/-- **T4 band propagation.** The κ_rs band `85.6 < κ_rs < 90.4`
propagates linearly to a band on the SI BMV phase rate, at fixed
`(Uconv, m₁, m₂, geometry)`. -/
theorem bmvPhaseRateSI_band_endpoints (U : UnitBridgeInput) :
    let lower :=
      U.Uconv * (85.6 * alphaRS *
        U.m1 * U.m2 *
        bmvGeometryFactor U.r_LL U.r_LR U.r_RL U.r_RR)
    let upper :=
      U.Uconv * (90.4 * alphaRS *
        U.m1 * U.m2 *
        bmvGeometryFactor U.r_LL U.r_LR U.r_RL U.r_RR)
    let mid := bmvPhaseRateSI U
    -- For positive geometry · m1 · m2, the band on κ_rs propagates.
    -- We state the structural identity and let users instantiate
    -- positivity per-experiment.
    mid =
      U.Uconv * (ZeroParameterGravity.kappa_rs * alphaRS *
        U.m1 * U.m2 *
        bmvGeometryFactor U.r_LL U.r_LR U.r_RL U.r_RR) := by
  exact bmvPhaseRateSI_eq_kappa_alpha_factored U

/-- **Helper: G/ℏ in RS-native units.**
We compute `G/ℏ = (φ⁵/π) · φ⁵ = φ¹⁰/π` directly by unfolding the
RS-native definitions:
* `G = λ_rec² c³ / (π ℏ)` with `λ_rec = c = 1` and `ℏ = φ⁻⁵`,
* so `G = 1/(π · φ⁻⁵) = φ⁵/π`,
* and `G/ℏ = (φ⁵/π)/φ⁻⁵ = φ¹⁰/π`. -/
theorem G_over_hbar_RS_native :
    G / hbar = phi ^ (5 : ℝ) / Real.pi * phi ^ (5 : ℝ) := by
  unfold G hbar cLagLock lambda_rec ell0 c tau0 tick
  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
  have hphi_ne : phi ^ (-(5 : ℝ)) ≠ 0 :=
    ne_of_gt (Real.rpow_pos_of_pos phi_pos _)
  -- After the unfold, we have (1^2 * 1^3) / (π * (φ⁻⁵ * 1)) / (φ⁻⁵ * 1)
  simp only [one_pow, mul_one, div_one]
  -- Goal: 1 / (π * φ⁻⁵) / φ⁻⁵ = φ⁵/π * φ⁵
  rw [Real.rpow_neg phi_pos.le]
  field_simp

/-- The SI BMV phase rate predicted under a unit-bridge input. -/
noncomputable def bmvPhaseRateSI (U : UnitBridgeInput) : ℝ :=
  U.Uconv * BMVPhaseRateNative U.m1 U.m2 U.r_LL U.r_LR U.r_RL U.r_RR

/-- A unit-bridge input parameterizes the conversion of the
RS-native BMV phase rate to SI. It records:
1. The RS-native algebraic identity `G/ℏ = (φ⁵/π) · φ⁵` (already a
   theorem, but bundled for clean propagation);
2. A scale factor `Uconv : ℝ` representing the dimensional
   `seconds_per_tick × meters_per_voxel⁻¹ × ...` combination supplied by
   `Constants.RSNativeUnits.ExternalCalibration`;
3. The test-mass parameters `(m₁, m₂, {r_ab})` in SI units.

This is a deliberately simple `Prop`-valued structure: the actual
`ExternalCalibration` instance lives in
`Foundation.DimensionalBridgeStructural`'s named open frontier. -/
structure UnitBridgeInput where
  /-- SI conversion scale (positive). -/
  Uconv : ℝ
  /-- Conversion is positive. -/
  Uconv_pos : 0 < Uconv
  /-- Mass 1 (SI). -/
  m1 : ℝ
  /-- Mass 1 positivity. -/
  m1_pos : 0 < m1
  /-- Mass 2 (SI). -/
  m2 : ℝ
  /-- Mass 2 positivity. -/
  m2_pos : 0 < m2
  /-- Branch separation r_LL. -/
  r_LL : ℝ
  /-- Nonzero. -/
  r_LL_ne : r_LL ≠ 0
  /-- Branch separation r_LR. -/
  r_LR : ℝ
  /-- Nonzero. -/
  r_LR_ne : r_LR ≠ 0
  /-- Branch separation r_RL. -/
  r_RL : ℝ
  /-- Nonzero. -/
  r_RL_ne : r_RL ≠ 0
  /-- Branch separation r_RR. -/
  r_RR : ℝ
  /-- Nonzero. -/
  r_RR_ne : r_RR ≠ 0

What this page does not claim

The theorem does not prove that gravity is quantized. The theorem does not claim the calibration constant has been measured or derived. The theorem does not claim the band on κ_rs is a prediction of a specific experimental outcome.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/NoGraviton/UnitBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: