absLogVorticity
plain-language theorem explainer
absLogVorticity supplies the absolute value of the signed log-vorticity at the center voxel of a MediumState, serving as a magnitude proxy for discrete vorticity in the flight medium model. Researchers deriving pressure proxies or helicity placeholders in Recognition Science cite it when converting signed log-vorticity to positive magnitudes. It is realized as a direct one-line definition applying absolute value to the center's logVorticity field.
Claim. For a medium state $S$, let $absLogVorticity(S) := |logVorticity(S)|$, where $logVorticity(S)$ denotes the signed log-vorticity proxy at the center voxel of $S$.
background
MediumState is a structure with a center VorticityVoxel and a list of neighboring voxels; it mirrors the way an LNAL VM evolves a local patch. The sibling logVorticity extracts the signed log-vorticity at the center and treats it as a φ-quantized proxy for log |ω|. The module supplies a minimal discrete medium interface for Flight proofs and deliberately decouples from the LNAL invariants subtheory while it is being modernized.
proof idea
One-line wrapper that applies the absolute value function to the logVorticity of the center voxel of the input MediumState.
why it matters
This definition is used by omegaMag in the Pressure module to produce a positive magnitude proxy for Bernoulli-like pressure drop calculations. It completes the lightweight discrete scaffold for the aether/light field medium, providing the magnitude proxy needed before helicity can be refined. The module comment notes that helicity remains a stubbed auxiliary slot for downstream work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.