module module high

`IndisputableMonolith.Flight.GravityBridge`

GravityBridge supplies rotation-period and dynamical-time definitions that link angular velocity to RS time quanta for rotating devices. Researchers modeling Podkletnov shielding or spiral-field propulsion cite these bridges. The module assembles imported geometry, schedule, and gravity primitives into a single interface. Its structure consists of declarative definitions with no internal proofs.

claimFor a device with angular velocity $ω$, the rotation period is $T=2π/ω$. The module also defines device dynamical time $T_ dyn$, lab-scale ratios, and mappings from these quantities to the RS time quantum $τ_0=1$ tick.

background

The module resides in the Flight domain, which scaffolds spiral-field propulsion on top of φ-tetrahedral geometry and 8-tick scheduling. It imports the fundamental RS time quantum $τ_0=1$ tick, the φ-tetrahedral angles and log-spiral rotor paths, the 8-window neutrality predicates, and Newtonian rotation identities together with ILG time kernels. The short module doc-comment states that a rotating device with angular velocity ω has period T=2π/ω.

proof idea

This is a definition module. It performs four module imports and declares a collection of bridge constants and functions (rotationPeriod, deviceDynamicalTime, labScaleRatio, etc.). No tactics or terms are applied; the file contains only declarations.

why it matters in Recognition Science

The module feeds the top-level Flight facade and supplies the rotating-disk model required by the Podkletnov gravity-shielding hypothesis. It also supports decoherence timescale calculations by providing dynamical-time ratios. It closes the interface between Gravity rotation curves and Flight scheduling within the eight-tick octave.

scope and limits

Does not contain any proved theorems.
Does not introduce new physical constants.
Does not model quantum effects or decoherence.
Does not include numerical predictions or error analysis.

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