modally_equivalent_refl
plain-language theorem explainer
Modal equivalence on configurations is reflexive under the tick-difference definition. Researchers building equivalence relations on possibility spaces in Recognition Science would cite this when verifying that modal equivalence is an equivalence relation. The proof is a one-line simplification that unfolds the definition and checks the zero time difference satisfies both strict inequalities.
Claim. For every configuration $c$, the relation holds: $c.value = c.value$ and $(c.time : ℤ) - (c.time : ℤ) < 1$ and $(c.time : ℤ) - (c.time : ℤ) < 1$.
background
Modal equivalence is defined by identical value components together with time components differing by less than one tick in each direction. The Config structure carries a value field and an integer time field, drawn from the Possibility module. The lemma sits inside ModalGeometry, whose imports from Possibility and Actualization locate it in the discrete-tick treatment of modal geometry.
proof idea
One-line wrapper that applies simp on the definition of modally_equivalent; the resulting equalities and inequalities hold identically when both arguments are the same configuration.
why it matters
The lemma supplies the reflexive leg of modal equivalence, a prerequisite for any equivalence-relation arguments in the modal layer. It directly supports constructions that treat configurations as interchangeable within a single tick, consistent with the eight-tick octave and the discrete time structure used throughout the framework. No downstream uses are recorded in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.