modally_equivalent_refl
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.