pith. sign in
module module high

IndisputableMonolith.Flight.Thrust

show as:
view Lean formalization →

The Thrust module supplies a minimal 3-vector type and associated thrust operations inside the Flight scaffold of Recognition Science. Researchers formalizing discrete propulsion models cite it for basic acceleration infrastructure. It depends on the Medium and Pressure modules and consists solely of type and function definitions.

claimThe module introduces a 3-dimensional vector space together with maps for thrust vector construction and net thrust computation in the discrete flight medium.

background

This module sits inside the Flight domain, which builds a discrete scaffold for spiral-field propulsion. It imports the Medium module (discrete vorticity proxy, intentionally decoupled from LNAL) and the Pressure module (mathematical pressure proxy separated from physical hypotheses). The supplied doc-comment states the module's sole purpose is a minimal 3-vector type for thrust and acceleration.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the vector primitives imported by the main Flight facade (convenience re-export for the Spiral-Field Propulsion formalization) and by the Falsifiers module (executable predicates over traces). It therefore anchors the lowest layer of the φ-Vortex Drive scaffold before physical hypotheses are added.

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)