samePattern
plain-language theorem explainer
Two octaves manifest the same pattern precisely when an equivalence exists between them, i.e., a pair of mutually inverse morphisms that preserve the strain functional isometrically in both directions. Researchers studying scale transfer in Recognition Science cite this when moving equilibrium or ordering properties from one octave to another. The definition is a direct abbreviation of the nonempty equivalence relation.
Claim. Two octaves $O_1$ and $O_2$ manifest the same pattern if there exists an equivalence between them, that is, a pair of mutually inverse morphisms that preserve the strain functional exactly in both directions.
background
An octave is a structure consisting of a state space, a strain functional (the J-cost), and display channels. Equivalence between two octaves requires mutually inverse morphisms that preserve the strain functional exactly, as defined in the core octave structure. The module on octave transfer theorems establishes that equivalent octaves share the same equilibrium structures, enabling pattern transfer across scales.
proof idea
This is a one-line definition that sets samePattern O1 O2 to the proposition Nonempty (OctaveEquiv O1 O2), directly encoding the existence of an equivalence.
why it matters
This definition underpins the reflexivity and symmetry theorems for the same-pattern relation, which support the main transfer results such as equilibria_transfer. It aligns with the Recognition Science emphasis on the eight-tick octave and self-similar structures, allowing properties to propagate across equivalent scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.