modally_equivalent_refl
Modal equivalence is reflexive, so any configuration satisfies the relation with itself under the one-tick distance. Researchers building equivalence classes or connectedness arguments in modal geometry cite this basic fact. The proof is a direct simplification that unfolds the definition and checks the reflexive clauses on value equality and time difference.
claimFor any configuration $c$, $c$ is modally equivalent to itself, where two configurations are modally equivalent precisely when they share the same value and their integer times differ by less than one tick in either direction.
background
Modal equivalence is defined by the predicate that two configurations $c_1$ and $c_2$ satisfy $c_1$.value = $c_2$.value together with the two strict inequalities on their integer times being less than 1 in absolute difference. The underlying Config structure carries the five real parameters upsilonStar, eps_r, eps_v, eps_t, eps_a drawn from the ILG gravity module. The lemma lives inside the ModalGeometry module, which imports the Possibility and Actualization files to supply the modal-distance and actualization primitives used throughout the modal layer.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of modally_equivalent, reducing the goal to the three reflexive clauses (value equality and the two time bounds) that hold identically.
why it matters in Recognition Science
The declaration supplies the reflexive leg of the modal equivalence relation, a prerequisite for any subsequent treatment of equivalence classes or connectedness inside possibility space. It directly supports sibling results such as possibility_space_connected and curvature statements that rely on local one-tick neighborhoods. Within the Recognition framework it anchors the eight-tick octave construction by guaranteeing that each configuration is equivalent to itself inside a single tick.
scope and limits
- Does not establish symmetry or transitivity of modal equivalence.
- Does not apply to types other than Config.
- Does not incorporate collision-free or empirical constraints from upstream modules.
- Does not address global properties such as periodicity or Nyquist limits.
formal statement (Lean)
146lemma modally_equivalent_refl (c : Config) : modally_equivalent c c := by
proof body
Term-mode proof.
147 simp [modally_equivalent]
148
149/-- Modal equivalence is symmetric. -/