samePattern
plain-language theorem explainer
samePattern declares that two octaves manifest the same pattern exactly when an equivalence exists between them. Researchers on scale transfer in RRF cite the relation to establish reflexivity and symmetry before proving equilibrium preservation. The definition is introduced as a direct abbreviation of nonempty OctaveEquiv.
Claim. Two octaves $O_1$ and $O_2$ manifest the same pattern when the set of equivalences between them is nonempty, i.e., Nonempty(OctaveEquiv $O_1$ $O_2$).
background
An Octave is a structure consisting of a state space, a strain functional (J-cost), and display channels; no physical constants appear at this level. OctaveEquiv consists of a pair of mutually inverse morphisms that preserve strain exactly in both directions. The module states that if two octaves are equivalent then their equilibrium structures coincide, which is the mechanism for the same pattern appearing at different scales.
proof idea
One-line definition that sets samePattern O1 O2 to Nonempty (OctaveEquiv O1 O2).
why it matters
The definition supplies the relation used by samePattern_refl and samePattern_symm. It encodes the module's central claim that isometric strain functions imply identical equilibria, supporting property transfer across octaves in the RRF layer of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.