module module

`IndisputableMonolith.Flight.GravityBridge`

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 (3)

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

IndisputableMonolith.Flight module_import
IndisputableMonolith.Gravity.Candidates.Podkletnov module_import
IndisputableMonolith.QFT.Decoherence module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Flight.Geometry module_import
IndisputableMonolith.Flight.Schedule module_import
IndisputableMonolith.Gravity module_import

declarations in this module (22)

def rotationPeriod L50
def deviceDynamicalTime L53
def tau0_seconds L59
def typicalLabPeriod_seconds L62
def labScaleRatio L65
def ilg_alpha L69
structure LabScalePrediction L80
def mkLabPrediction L89
def phaseDuration L101
def ticksPerPhase L106
def scheduleWellSeparated L110
theorem lab_schedule_well_separated L113
def nullHypothesis L123
theorem null_holds_if_C_lag_small L127
structure GravityFalsifier L151
def falsifierTriggered L156
def C_lag_RS L163
def rsLabPrediction L172
def rs_lab_prediction_value L181
def optionA_testable L187
def optionB_bound_only L192
structure RunningCoupling L198