modal_nyquist
plain-language theorem explainer
Modal Nyquist theorem states that two configurations agreeing on value and time are modally equivalent. Researchers in discrete spacetime models or modal quantum interpretations cite it to enforce the sampling limit from the eight-tick structure. The proof reduces directly by simplification on the equivalence predicate using the two equality hypotheses.
Claim. If two configurations $c_1$ and $c_2$ satisfy $c_1.value = c_2.value$ and $c_1.time = c_2.time$, then $c_1$ and $c_2$ are modally equivalent.
background
In ModalGeometry the type Config is imported from the ILG gravity module. The eight-tick phase supplies discrete angles $k pi / 4$ for $k = 0..7$, periodic with period $2 pi$. Cost is defined in two places: as the derived cost of a multiplicative recognizer comparator and as the J-cost of a recognition event. Modal equivalence is the predicate that two configurations are indistinguishable under the possibility structure.
proof idea
The proof is a one-line wrapper that applies simp to unfold modally_equivalent and substitute the hypotheses on value and time.
why it matters
It supplies the modal analog of Nyquist sampling inside the Recognition Science framework, directly implementing the eight-tick octave limit. The result bounds distinguishability of possibilities and connects to the phase-space uncertainty and qualia thresholds listed in the declaration comment. No downstream uses are recorded, so its role in closing the modal geometry section remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.