equiv_wellPosed
plain-language theorem explainer
Octave equivalences preserve well-posedness: if two octaves are related by mutually inverse strain-preserving morphisms, then one satisfies the well-posed predicate precisely when the other does. Researchers modeling scale-invariant equilibrium structures in RRF would cite this to transfer balance properties across equivalent octaves. The proof is a term-mode biconditional constructor that maps equilibrium witnesses forward and backward using the equivalence and inverse strain equality.
Claim. Let $e$ be an equivalence between octaves $O_1$ and $O_2$, meaning mutually inverse morphisms that preserve strain isometrically in both directions. Then $O_1$ is well-posed if and only if $O_2$ is well-posed, where well-posed means existence of a state satisfying the zero-strain (isBalanced) condition.
background
In the RRF framework, an OctaveEquiv between octaves $O_1$ and $O_2$ consists of mutually inverse OctaveMorphism instances that preserve strain exactly in both directions, as defined in RRF.Core.Octave. The wellPosed predicate asserts existence of a state satisfying the isBalanced condition, the zero-strain predicate from StrainFunctional (abbreviated in RRF.Core.Glossary as the zero-strain predicate). The module develops transfer lemmas showing that equivalent octaves share equilibrium structures, building on the core definition that equivalence means isometric strain functions so the same pattern manifests at different scales.
proof idea
The proof is a term-mode biconditional constructor. The forward direction takes a witness $x$ with balance hypothesis $hx$ for $O_1$, maps it via $e.toFun.map x$, and rewrites using the sibling lemma equiv_equilibria_iff to obtain the balanced state for $O_2$. The reverse direction maps via $e.invFun.map y$ and applies the inverse strain preservation $e.strain_eq_inv y$ to transfer the balance condition.
why it matters
This theorem establishes that well-posedness transfers under octave equivalence, supporting the module insight that equivalent octaves have identical equilibrium structures. It contributes to showing how the same pattern manifests at different scales within the eight-tick octave structure. With no downstream uses recorded, it serves as a foundational transfer result for later applications such as channel quality transfer or pattern preservation lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.