pith. sign in
module module high

IndisputableMonolith.Flight.GravityBridge

show as:
view Lean formalization →

GravityBridge supplies definitions connecting rotating device periods and lab scales to RS time quanta and 8-tick scheduling. Researchers modeling Podkletnov effects or spiral-field propulsion cite these to parameterize angular velocities inside the Flight domain. The module consists entirely of definitions drawn from imported Geometry, Schedule, Gravity, and Constants primitives.

claimThe module defines rotation period $T=2\pi/\omega$ for angular velocity $\omega$, device dynamical time, $\tau_0$ in seconds, typical lab period, lab scale ratio, ILG $\alpha$, LabScalePrediction, phase duration, ticks per phase, and scheduleWellSeparated predicate.

background

This module sits in the Flight domain and bridges Gravity (Rotation identities $v^2=GM/r$, ILG time-kernels, ParameterizationBridge linking $\alpha$ to $T_\text{dyn}/T_0$) with Flight.Geometry ($\phi$-tetrahedral angles and log-spiral paths) and Flight.Schedule (8-tick control discipline). It introduces rotationPeriod, deviceDynamicalTime, tau0_seconds ($\tau_0=1$ tick), labScaleRatio, ilg_alpha, and scheduling functions phaseDuration and ticksPerPhase. The setting uses RS-native units with $c=1$, $\hbar=\phi^{-5}$, and the eight-tick octave from the forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Flight facade and is imported by Gravity.Candidates.Podkletnov (weight reduction claim) and QFT.Decoherence (Gap-45 timescales). It supplies the definitional layer linking Newtonian rotation curves to RS constants and the 8-tick discipline, closing the bridge step in the spiral-field propulsion scaffold without new hypotheses.

scope and limits

used by (3)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (22)