equiv_equilibria_iff
plain-language theorem explainer
Octave equivalences preserve equilibria exactly: a state x in the first octave satisfies the zero-strain condition if and only if its image under the equivalence map satisfies the zero-strain condition in the second octave. Researchers modeling scale-invariant patterns cite this when transferring equilibrium conditions across octaves. The proof is a direct term-mode reduction that simplifies the isBalanced predicate and rewrites via the strain equality from the equivalence.
Claim. Let $e$ be an equivalence between octaves $O_1$ and $O_2$, and let $x$ be a state in the state space of $O_1$. Then the strain functional of $O_1$ is balanced at $x$ if and only if the strain functional of $O_2$ is balanced at the image of $x$ under the map induced by $e$.
background
An octave is a structure consisting of a state space, a strain functional (the J-cost), and observation channels. The isBalanced predicate is the zero-strain condition, defined as the total cost being zero. Equivalences between octaves are maps that preserve the strain functional exactly via the strain_eq property. This theorem appears in the RRF.Theorems.OctaveTransfer module, whose module documentation states that equivalent octaves have the same equilibrium structures, allowing the same pattern to manifest at different scales.
proof idea
The proof is a term-mode reduction. It applies simp only on StrainFunctional.isBalanced to unfold the predicate, then rewrites the strain value at the mapped state using the equality e.strain_eq x supplied by the OctaveEquiv structure.
why it matters
This result is invoked directly by equiv_wellPosed to transfer well-posedness between equivalent octaves. It supplies the equilibrium-transfer step in the OctaveTransfer module, supporting the framework claim that equivalent octaves share identical equilibrium structures. In the Recognition Science setting it underpins transfer across the eight-tick octave without reference to specific constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.