modally_equivalent
plain-language theorem explainer
Modal equivalence holds for two configurations precisely when their values coincide and their integer time coordinates differ by less than one tick in either direction. Researchers developing modal geometry or the modal Nyquist limit in Recognition Science cite the definition to encode one-tick indistinguishability. The definition is supplied directly as a three-part conjunction on the Config fields.
Claim. Two configurations $c_1$ and $c_2$ satisfy modal equivalence when $c_1.value = c_2.value$ and $|(c_1.time : ℤ) - (c_2.time : ℤ)| < 1$.
background
In Modal.Possibility a Config is a simplified point in recognition state space carrying a positive real value (generalizing bond multiplier) and an integer time coordinate measured in ticks. The present definition operates directly on pairs of such Configs. Upstream structures supply the value and time projections used in the conjunction; the surrounding module imports Possibility and Actualization to place the predicate inside modal geometry.
proof idea
This is a direct definition whose body is the conjunction of value equality with the pair of strict inequalities on the integer time difference.
why it matters
The definition supplies the predicate used to prove reflexivity and symmetry of modal equivalence and to state the modal Nyquist theorem (the universe cannot distinguish possibilities finer than one tick). That theorem is presented as the modal counterpart of Nyquist sampling, Heisenberg uncertainty, and the gap-45 consciousness threshold. It therefore anchors the modal layer of the Recognition framework before further geometry lemmas are derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.