pith. machine review for the scientific record. sign in
structure definition def or abbrev high

MediumStateH

show as:
view Lean formalization →

MediumStateH pairs a discrete medium state with a helicity proxy as a display wrapper in the Flight module. Researchers modeling discrete vorticity in light fields or aether scaffolds would cite this when extending medium states. It is defined directly as a structure with two fields and no further content.

claimA helicity-augmented medium state consists of a medium state $S$ (central vorticity voxel together with a list of neighbors) and a helicity proxy $H$ (a real number placeholder).

background

The Flight.Medium module supplies a minimal discrete interface for medium states in Recognition Science, intentionally decoupled from LNAL for now. MediumState is a center vorticity voxel plus a neighborhood list, with logVorticity serving as a φ-quantized proxy for log |ω|. HelicityProxy provides a lightweight real-valued stub for helicity tracking in auxiliary slots, as noted in LNAL fluids comments. Upstream structures include the MaxwellDEC Medium with eps and mu parameters, and the ILG action S.

proof idea

The declaration is a direct structure definition that simply declares the two fields S and H.

why it matters in Recognition Science

This structure provides the basic pairing needed for Flight proofs involving medium states. It supports the discrete scaffold without claiming continuum models, relating to the Maxwell medium and ILG action in the framework. No downstream uses are recorded yet, leaving room for refinement in helicity integration.

scope and limits

formal statement (Lean)

  70structure MediumStateH where
  71  S : MediumState
  72  H : HelicityProxy
  73
  74end Medium
  75end Flight
  76end IndisputableMonolith
  77

depends on (6)

Lean names referenced from this declaration's body.