Axis
plain-language theorem explainer
The abbreviation supplies the index set for the three spatial directions on the discrete lattice used by the Navier-Stokes operators. Discrete fluid models and topological charge calculations cite it when summing over directions in divergence or advection. It is realized as a direct alias to the standard finite type of cardinality three with no additional structure.
Claim. Let $A :=$ Fin $3$, the finite set of three indices labeling the coordinate directions in the lattice.
background
The module builds a concrete discrete incompressible Navier-Stokes operator on a finite lattice equipped with three directions. Vector fields and scalar fields are indexed by site and by direction, with forward and backward difference operators taking an explicit direction argument from this set. LatticeTopology supplies the neighbor maps plus and minus that are likewise indexed by direction, realizing the three-dimensional spatial structure required by the Recognition Science forcing chain at step T8.
proof idea
The declaration is a direct abbreviation to the standard three-element finite type Fin 3.
why it matters
This index set supplies the concrete realization of D = 3 for all lattice operators in the module, including advection, divergence, and the Laplacian. It feeds the downstream theorem winding_gives_three_charges, which shows that three winding numbers produce three independent topological charges matching independent_charge_count 3. The definition thereby closes the bijection between lattice directions and the three charges in the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.