modal_nyquist_limit
plain-language theorem explainer
The modal Nyquist limit is defined as half the eight-tick modal period, yielding the integer 4. Modal geometers cite it when bounding resolution of possibility configurations under the Recognition framework. The definition is a direct arithmetic reduction from the period constant.
Claim. The modal Nyquist limit equals 4, so configurations differing by less than one tick are modally equivalent, with maximum modal frequency $1/(2τ_0)$ and bandwidth 4 ticks per octave.
background
Tick denotes the fundamental RS time quantum τ₀ = 1. Modal period is the eight-tick fundamental evolution period of modal states. The definition appears in the ModalGeometry module after imports of Possibility and Actualization; it rests on the period constant and the one constants from IntegersFromLogic and RationalsFromLogic.
proof idea
One-line definition that divides the modal period by two.
why it matters
It encodes the Nyquist sampling analogy for modal equivalence inside the Recognition framework. The declaration fills the T7 eight-tick octave step and supplies the bandwidth figure quoted in the module doc-comment. No parent theorems or downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.