VorticityVoxel
plain-language theorem explainer
VorticityVoxel supplies a six-field record that holds signed log-vorticity together with defaulted proxies for stream function, sign parity, time slice, velocity mode, and vorticity phase. Researchers building discrete medium states in the Flight domain cite it when constructing local patches that evolve independently of the LNAL VM. The definition is a direct record construction that supplies explicit types and defaults for every secondary field.
Claim. A vorticity voxel is a record consisting of a real number for signed log-vorticity, a real number for stream function (default 0), an integer for sign parity (default 1), a natural number for time slice (default 0), an integer for velocity mode (default 0), and an integer for vorticity phase (default 0).
background
The Flight module supplies a minimal discrete scaffold for medium states that deliberately avoids continuum Navier-Stokes modeling. Upstream results supply the fundamental tick as the RS time quantum equal to 1 and the voxel as the corresponding length quantum. The logVorticity field functions as a signed proxy for log of vorticity magnitude, while the vorticityPhase field draws on the eight-tick phase definition that returns multiples of π/4.
proof idea
The declaration is a direct structure definition that enumerates the six fields with explicit types and default values on five of them. No lemmas or tactics are invoked; the construction simply replicates the LNAL record shape inside the Flight namespace.
why it matters
VorticityVoxel populates the center field of MediumState and thereby supplies the discrete vorticity proxy required for local-patch evolution in Flight proofs. It implements the module's stated intention to mirror LNAL shape while remaining decoupled during LNAL modernization. The structure therefore supports the eight-tick octave and RS-native units without committing to full continuum dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.