equivZModTwo
The closed automorphism theorem states that the group of multiplicative J-preserving maps on positive reals is isomorphic to Z/2Z. Researchers deriving the Recognition Composition Law or the forcing chain would cite this to confirm that only the identity and reciprocal maps qualify as automorphisms. The definition is a one-line wrapper that composes the existing Fin-2 coding with the standard equivalence from Fin 2 to ZMod 2.
claimThe set of maps $f : (0,∞) → (0,∞)$ that satisfy $f(xy) = f(x)f(y)$ and $J(f(x)) = J(x)$ for all $x,y > 0$ is equivalent to the cyclic group of order two: $Aut(J) ≃ ℤ/2ℤ$, with the two elements corresponding to the identity and the map $x ↦ x^{-1}$.
background
The J-cost is the function $J(x) = ½(x + x^{-1}) - 1$ on positive reals, the unique solution to the Recognition Composition Law. JAut is the subtype of all maps on positive reals that are multiplicative and preserve this J-cost exactly. An upstream result already codes these maps as a two-point set: the identity at one element and the reciprocal map at the other.
proof idea
This is a one-line wrapper that transports the equivalence equivFinTwo : JAut ≃ Fin 2 along the canonical equivalence Fin 2 ≃ ZMod 2 supplied by ZMod.finEquiv.
why it matters in Recognition Science
This definition supplies the paper-facing statement that Aut(J) is exactly ℤ/2ℤ, closing the classification of automorphisms required for J-uniqueness in the forcing chain (T5). It confirms that the only symmetries of the cost algebra are the identity and reciprocal, consistent with the self-similar fixed point and the eight-tick octave structure.
scope and limits
- Does not prove that continuity or bijectivity are required for the classification.
- Does not address maps that fail to preserve J.
- Does not compute the induced group law on ZMod 2 explicitly.
- Does not extend the result beyond positive reals.
formal statement (Lean)
928noncomputable def equivZModTwo : JAut ≃ ZMod 2 :=
proof body
Definition body.
929 equivFinTwo.trans (ZMod.finEquiv 2).toEquiv
930
931end JAut
932
933/-- Paper-facing closed automorphism theorem:
934 the only continuous multiplicative bijections on `ℝ_{>0}` preserving `J`
935 are the identity and reciprocal maps. The continuity and bijectivity
936 assumptions are stronger than needed; the proof uses the sharper `JAut`
937 classification above. -/