samePattern_symm
plain-language theorem explainer
The samePattern relation on octaves is symmetric. Researchers modeling scale-invariant recognition structures cite this when establishing that equivalence is bidirectional before transferring equilibria or ordering. The proof is a one-line term construction that extracts the OctaveEquiv witness and applies its built-in symmetry.
Claim. Let $O_1$ and $O_2$ be octaves. If there exists a pair of mutually inverse strain-preserving morphisms between them, then there exists such a pair in the opposite direction.
background
An octave consists of a state space, a strain functional (J-cost), and observation channels. Two octaves stand in the OctaveEquiv relation when there exist mutually inverse morphisms that preserve strain exactly in both directions. The predicate samePattern holds precisely when this equivalence type is nonempty.
proof idea
The proof is a term-mode one-liner. It destructures the hypothesis to obtain the OctaveEquiv witness e and immediately constructs the converse witness by applying OctaveEquiv.symm to e.
why it matters
This lemma supplies the symmetry half of the equivalence-relation properties for samePattern, which the OctaveTransfer module uses to move equilibria and ordering statements between scales. It directly supports the module's stated goal that equivalent octaves share the same equilibrium structures, a prerequisite for the claim that identical patterns appear across different octaves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.