modal_nyquist_limit
plain-language theorem explainer
The modal Nyquist limit is defined as half the eight-tick modal period, yielding the integer value 4. Researchers modeling resolution in possibility spaces or modal evolution cite it when bounding equivalence classes under the tick quantum. The definition is a direct arithmetic reduction of the upstream modal period constant.
Claim. The modal Nyquist limit equals half the fundamental modal period: $P/2$ where $P=8$ ticks, so the limit is 4. This sets the maximum modal frequency at $1/(2τ_0)$ with $τ_0$ the fundamental time quantum, making configurations differing by less than one tick modally equivalent.
background
Modal geometry analyzes possibility spaces using the fundamental time quantum tick, defined as $τ_0=1$ in RS-native units. The upstream modal period is fixed at 8, establishing the eight-tick octave as the basic evolution cycle. This definition sits inside the ModalGeometry module, which imports Possibility and Actualization to treat modal equivalence under small differences.
proof idea
The definition is a one-line wrapper that divides the modal period constant by 2, directly producing the integer 4 as the Nyquist resolution bound.
why it matters
This definition supplies the modal resolution limit that parallels the Nyquist sampling theorem, with bandwidth 4 ticks per octave. It directly implements the eight-tick period from the forcing chain (T7) and supports equivalence statements in modal geometry. No downstream theorems yet reference it, leaving open its integration into broader possibility-space curvature results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.