module module

`IndisputableMonolith.Gravity.NoGraviton.UnitBridge`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.ZeroFreeParameters module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Gravity.NoGraviton module_import
IndisputableMonolith.Gravity.QuantumChannel.BMVPositive module_import

declarations in this module (14)

def bmvGeometryFactor L59
def BMVPhaseRateNative L65
theorem G_over_hbar_RS_native L75
theorem bmv_phase_rate_native_eq L88
def alphaRS L103
theorem alphaRS_pos L105
theorem kappa_rs_alphaRS_eq_G_over_hbar L115
structure UnitBridgeInput L145
def bmvPhaseRateSI L176
theorem bmvPhaseRateSI_eq_kappa_alpha_factored L181
theorem bmvPhaseRateSI_band_endpoints L195
structure UnitBridgeTheorem L216
def unitBridgeTheorem L231
theorem unitBridgeTheorem_inhabited L236