modally_equivalent_symm
plain-language theorem explainer
Modal equivalence between two configurations is symmetric. Researchers modeling possibility spaces and modal distances in Recognition Science cite this when verifying that equivalence forms a relation compatible with the eight-tick structure. The proof is a term-mode reduction that unfolds the definition via simplification then swaps the asymmetric components of the unpacked triple.
Claim. For configurations $c_1$ and $c_2$, modal equivalence holds between $c_1$ and $c_2$ if and only if it holds between $c_2$ and $c_1$.
background
In the modal geometry setting, configurations inhabit a possibility space whose structure is built from possibility and actualization maps. Modal equivalence is the relation obtained when the modal distance vanishes. Upstream results supply the fundamental time quantum (one tick) and the eight-tick phase function taking values $kπ/4$ for $k=0$ to $7$, which together enforce the periodicity underlying modal resolution.
proof idea
The term proof first simplifies the definition of modal equivalence to expose its internal triple. Constructor splits the biconditional; each direction introduces the triple and rebuilds it by applying symmetry to the first component while exchanging the second and third.
why it matters
The lemma supplies the symmetry half of the equivalence-relation axioms needed for modal geometry. It directly supports the modal Nyquist statement that the universe cannot resolve possibilities finer than one tick, linking to the eight-tick octave and the forcing chain's T7 step. No downstream uses are recorded, so the result functions as a local closure for symmetry properties within the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.