pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Flight.Thrust

show as:
view Lean formalization →

The Thrust module supplies a minimal three-dimensional vector type for representing thrust and acceleration in the Recognition Science flight model. Researchers formalizing spiral-field propulsion cite it for basic vector operations on the discrete scaffold. It is a definition module containing only type and function declarations with no theorems or proofs.

claimThe module declares a type $V_3$ representing three-dimensional vectors together with functions thrustVector and netThrust for computing thrust and net acceleration vectors.

background

This module belongs to the Flight subdomain of Recognition Science, which builds a discrete scaffold for spiral-field propulsion. It imports the medium state interface from Flight.Medium, which supplies a discrete vorticity proxy intentionally decoupled from LNAL, and the pressure proxy from Flight.Pressure, which separates mathematical definitions from physical hypotheses. The module itself introduces the minimal 3-vector type to support thrust and acceleration calculations on top of these imported interfaces.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the basic vector infrastructure re-exported by the main IndisputableMonolith.Flight facade for the Spiral-Field Propulsion formalization scaffold. It also supports Flight.Falsifiers by providing the vector primitives needed for executable predicates over recorded traces. It fills the lowest-level definition step in the φ-Vortex Drive chain before physical hypotheses are layered on.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)