symm
plain-language theorem explainer
Symmetry on octave equivalences inverts the forward and backward morphisms while swapping the strain preservation conditions. Researchers modeling scale-invariant patterns across manifestation levels would cite this when verifying that equivalence relations are symmetric. The definition constructs the inverse by direct component swap of the two morphisms and their strain equalities.
Claim. Given octaves $O_1$ and $O_2$ and an equivalence $e$ between them (mutually inverse morphisms preserving the strain functional $J$ exactly in both directions), the symmetric equivalence from $O_2$ to $O_1$ is the structure with forward map equal to the inverse of $e$, inverse map equal to the forward map of $e$, and the two strain-preservation statements interchanged.
background
An octave is a state space equipped with a strain functional (the J-cost), a bundle of display channels, and a non-emptiness witness. Two octaves are equivalent when there exist mutually inverse morphisms that preserve the strain functional exactly in both directions, as recorded in the OctaveEquiv structure. This module supplies the abstract octave structure without embedding physical constants such as the golden ratio or the eight-tick period; those appear in layered hypotheses. Upstream results supply concrete octave ratios, including the factor of 2 from musical scales and the factor of 8 from the fundamental evolution period.
proof idea
The definition is a direct structural construction that sets the forward map to the inverse of the input equivalence, the inverse map to the forward map, and swaps the two strain preservation statements.
why it matters
This definition supplies the symmetry axiom for the equivalence relation on octaves, allowing construction of equivalence classes that identify patterns across different manifestation scales. It supports the Recognition framework's treatment of particles and structures as the same at different octaves related by phi-scaling. No downstream uses are recorded yet, but it underpins symmetry in the octave category.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.