pith. sign in
module module high

IndisputableMonolith.Flight.Medium

show as:
view Lean formalization →

The Medium module supplies a local vorticity voxel proxy and related state definitions for the Flight namespace. It replicates the LNAL VorticityVoxel structure to permit independent compilation of Flight submodules. The module introduces MediumState, logVorticity, absLogVorticity, HelicityProxy, and MediumStateH as mathematical proxies. These definitions form the base layer for modeling spiral-field propulsion without external dependencies. The module consists solely of definitions with no theorems or proofs.

claimIntroduces a record for local vorticity voxels with position and vector components, a medium state type $S$, scalar field functions for logarithmic vorticity and its absolute value, a helicity proxy $h$, and a state helper $S_H$, all as self-contained proxies.

background

This module operates in the Flight domain, providing proxies for fluid-like quantities in spiral-field models. It defines a vorticity voxel record that mirrors the LNAL version but resides locally to avoid dependencies on the larger VM stack. Key objects include MediumState for representing the local medium, logVorticity and absLogVorticity for derived scalar fields, HelicityProxy for topological measures, and MediumStateH as a helper. The setting isolates mathematical definitions from physical hypotheses, as seen in the downstream Pressure and Thrust modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds the main Flight module, which acts as a facade for Spiral-Field Propulsion formalization, and supports the Pressure and Thrust layers. It enables separation of mathematical proxies from physical assumptions in the φ-Vortex Drive scaffold. The definitions allow lemmas on vorticity to be proved independently while keeping the Flight namespace self-contained.

scope and limits

used by (3)

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

declarations in this module (6)