equivZModTwo
The declaration supplies an explicit isomorphism identifying the automorphism group of the J-cost function with the cyclic group of order two. Algebraists working inside the Recognition Science cost framework cite it to close the classification of J-preserving multiplicative maps on positive reals. The proof is a one-line composition that transports the two-point coding equivFinTwo through the standard equivalence between Fin 2 and ZMod 2.
claimLet $J(x) = (x + x^{-1})/2 - 1$. The set of multiplicative maps $f : (0,1]_{+} ightarrow (0,1]_{+}$ satisfying $J(f(x)) = J(x)$ for all $x > 0$ is in bijection with $mathbb{Z}/2mathbb{Z}$, sending the identity map to $0$ and the reciprocal map $x mapsto x^{-1}$ to $1$.
background
J is the canonical cost function on positive reals, defined by $J(x) = frac12(x + x^{-1}) - 1$, which satisfies the Recognition Composition Law. JAut is the subtype of maps $f : PosReal to PosReal$ that are multiplicative and preserve the value of J. The upstream result equivFinTwo already exhibits a bijection between JAut and Fin 2 by sending the identity to 0 and the reciprocal automorphism to 1. The present definition simply relabels the codomain via the canonical equivalence Fin 2 ≃ ZMod 2.
proof idea
One-line wrapper that applies the equivalence equivFinTwo : JAut ≃ Fin 2 and composes it with the standard equivalence (ZMod.finEquiv 2).toEquiv : Fin 2 ≃ ZMod 2.
why it matters in Recognition Science
The definition realizes the closed automorphism theorem that Aut(J) is exactly ℤ/2ℤ. It supplies the algebraic symmetry group underlying the J-uniqueness step (T5) of the forcing chain and the two-element structure that appears in cost composition and ledger forcing. The result confirms that the only continuous multiplicative J-automorphisms are the identity and the reciprocal map, consistent with the eight-tick octave and the emergence of three spatial dimensions.
scope and limits
- Does not derive the two-element classification from the functional equation without the JAut subtype.
- Does not address continuity or measurability assumptions beyond the algebraic setting.
- Applies only to the specific cost J and not to other solutions of the Recognition Composition Law.
- Does not supply an independent inverse construction outside the composition with equivFinTwo.
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. -/