MediumState
plain-language theorem explainer
The structure packages a central vorticity voxel with its neighbors to represent a local patch in the discrete flight medium. Fluid modelers working inside the Recognition framework cite it when assembling pressure drop proxies and thrust vectors. The declaration is a direct structure definition that encodes the center-neighborhood pattern without axioms or proof obligations.
Claim. A local state of the medium consists of a central vorticity voxel together with a list of neighboring vorticity voxels.
background
The Flight.Medium module supplies a discrete scaffold for the aether or light field. It employs a vorticity proxy rather than a full continuum Navier-Stokes model and remains decoupled from the LNAL VM stack. VorticityVoxel is the local record that stores signed log-vorticity (treated as a phi-quantized proxy for log of vorticity magnitude), stream function, sign parity, and time slice. Upstream results include the unit voxel length from RSNativeUnits and the neighbor extraction pattern from StakeGraph.
proof idea
The declaration is a direct structure definition that introduces the two fields center and neighbors. No lemmas are applied and no tactics are used.
why it matters
MediumState supplies the basic interface required by downstream Flight constructions, including logVorticity, absLogVorticity, the helicity wrapper MediumStateH, omegaMag, PressureDropFromVorticity, and thrustVector. It realizes the discrete vorticity proxy approach stated in the module documentation and supports the pressure-equals-proxy hypothesis interface. The structure therefore occupies the local-patch slot in the Flight layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.