equivFinTwo
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not classify the automorphisms; it relies on the prior result that every J-automorphism is the identity or the reciprocal.
- Does not extend the bijection to maps that fail to preserve multiplication or J.
- Does not impose or verify continuity or measurability on the automorphisms.
formal statement (Lean)
913noncomputable def equivFinTwo : JAut ≃ Fin 2 := by
proof body
Definition body.
914 classical
915 refine
916 { toFun := fun f => if f = id then 0 else 1
917 invFun := fun i => if i = 0 then id else reciprocal
918 left_inv := ?_
919 right_inv := ?_ }
920 · intro f
921 rcases eq_id_or_reciprocal f with h | h
922 · simp [h]
923 · simp [h, reciprocal_ne_id]
924 · intro i
925 fin_cases i <;> simp [reciprocal_ne_id]
926
927/-- **Closed automorphism theorem**: `Aut(J)` is exactly `ℤ/2ℤ`. -/