equivFinTwo
plain-language theorem explainer
This definition supplies an explicit bijection from the set of J-automorphisms to the two-element set. Researchers establishing the automorphism group of the cost algebra would cite it to reach the isomorphism with Z/2Z. The construction defines the forward map by sending the identity to 0 and all other maps to 1, then verifies the two-sided inverse property by case analysis on the classification of automorphisms.
Claim. The set of maps $f : (0,∞) → (0,∞)$ that preserve multiplication and satisfy $J(f(x)) = J(x)$ for all $x$ is in bijection with the set with two elements, sending the identity map to 0 and the map $x ↦ x^{-1}$ to 1.
background
The J-cost is the function $J(x) = ½(x + x^{-1}) - 1$ on the positive reals, the unique solution to the Recognition Composition Law. JAut is the subtype of multiplicative maps $f$ that also preserve the value of J. The upstream classification theorem states that every such map is either the identity or the reciprocal map $x ↦ x^{-1}$, and the reciprocal differs from the identity.
proof idea
The definition builds the equivalence by explicit functions. The forward map returns 0 on the identity and 1 otherwise. The inverse returns the identity on 0 and the reciprocal on 1. The left-inverse property follows from case analysis on the classification theorem together with the fact that the reciprocal differs from the identity. The right-inverse property is checked by exhaustive case analysis on the two elements of Fin 2.
why it matters
The equivalence is the immediate predecessor of equivZModTwo, which states that the automorphism group of J is isomorphic to Z/2Z. This closed automorphism theorem confirms that the only symmetries preserving the cost function are the identity and inversion, a necessary algebraic fact for the forcing chain and the derivation of the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.