modally_equivalent
plain-language theorem explainer
Two configurations are defined as modally equivalent precisely when their values coincide and their integer tick times differ by less than one unit in either direction. Modal geometry work in Recognition Science cites this when formalizing indistinguishability at the tick scale. The definition is a direct conjunction of the three conditions with no lemmas or reductions required.
Claim. Configurations $c_1$ and $c_2$ (each with a positive real value field and an integer time coordinate in ticks) satisfy modal equivalence when $c_1.value = c_2.value$ and both directed differences of their times are strictly less than 1.
background
In the ModalGeometry module a Config is taken from Possibility and consists of a positive real value together with a time coordinate measured in ticks; the module treats this as a simplified point in recognition state space rather than a full LedgerState. The definition of modal equivalence therefore operates directly on these two fields. Upstream structures such as ILG.Config and the various is predicates supply supporting notions of configuration but do not alter the local modal equivalence condition.
proof idea
The declaration is a definition whose body is the conjunction of value equality with the pair of strict inequalities on the cast time coordinates. No tactics or upstream lemmas are invoked; the three conjuncts are written explicitly.
why it matters
The definition supplies the relation used by modally_equivalent_refl, modally_equivalent_symm and the modal_nyquist theorem. The latter states that the universe cannot distinguish possibilities finer than one tick and draws the explicit analogy to Nyquist sampling, Heisenberg uncertainty and the Gap-45 consciousness threshold. It therefore anchors the one-tick resolution limit inside the modal fragment of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.