pith. sign in
module module high

IndisputableMonolith.Flight.GravityBridge

show as:
view Lean formalization →

GravityBridge bridges Flight geometry and scheduling with Gravity formalisms to define rotation periods and dynamical times for rotating devices. Researchers formalizing Podkletnov shielding or spiral propulsion cite its auxiliary definitions. The module contains no proofs and functions as a pure re-export and specialization layer over the four imported modules.

claimA rotating device satisfies $T = 2\pi/\omega$ with dynamical time scales derived from the RS time quantum $\tau_0$ and 8-tick schedules; the bridge supplies lab-scale ratios and phase durations linking $\phi$-tetrahedral geometry to ILG kernels.

background

The module sits in the Flight domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants. Flight.Geometry supplies the purely geometric layer of $\phi$-tetrahedral angles and log-spiral rotor paths derived from Recognition Science axioms. Flight.Schedule reuses 8-window neutrality predicates, while Gravity re-exports Newtonian rotation identities ($v^2 = GM/r$) and Information-Limited Gravity time-kernels. The DOC_COMMENT states the elementary period relation for any rotating device.

proof idea

This is a definition module with no proofs. It structures the argument by importing the four upstream modules and exposing specialized quantities (rotationPeriod, deviceDynamicalTime, phaseDuration, labScaleRatio) that connect geometric and scheduling primitives to gravity parameterizations.

why it matters in Recognition Science

The module feeds the Flight facade, the Podkletnov gravity-shielding hypothesis (weight reduction on rotating YBCO disks), and QFT decoherence timescales. It supplies the rotation bridge required to link the 8-tick octave and $\phi$-ladder geometry to ILG weight functions, closing the interface between geometric flight models and gravity candidates.

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)