equivZModTwo
plain-language theorem explainer
The closed automorphism theorem asserts that J-automorphisms on positive reals form a group isomorphic to ℤ/2ℤ. Researchers classifying symmetries under the Recognition Composition Law would cite this equivalence when reducing Aut(J) to a two-element group. The definition is a one-line wrapper composing the Fin 2 coding with the standard Fin-to-ZMod equivalence.
Claim. The type of multiplicative maps $f$ on positive reals that preserve the cost function $J(x) = ½(x + x^{-1}) - 1$ is canonically equivalent to $ℤ/2ℤ$.
background
JAut is the subtype of maps PosReal → PosReal that are multiplicative and satisfy J(f(x)) = J(x) for all x, where J is the unique cost obeying the Recognition Composition Law. equivFinTwo supplies the prior equivalence JAut ≃ Fin 2 that sends the identity map to 0 and the reciprocal map to 1. The module works inside the canonical cost algebra on ℝ>0 and imports the functional equation results that force J to be the hyperbolic cosine form.
proof idea
One-line wrapper that applies equivFinTwo and then composes with (ZMod.finEquiv 2).toEquiv.
why it matters
This definition supplies the ℤ/2ℤ coding required by the paper-facing closed automorphism theorem, which states that the only continuous multiplicative bijections preserving J are the identity and reciprocal maps. It completes the classification step that aligns with T5 J-uniqueness in the forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.