eq_id_of_map_two_eq_two
Any J-automorphism of the positive reals that fixes 2 must be the identity map everywhere. Researchers classifying the automorphism group of the cost algebra cite this result to separate the identity case from the reciprocal case. The proof applies the pointwise dichotomy lemma, then uses multiplicativity on 2x to derive a contradiction if the reciprocal branch is chosen at any point.
claimLet $f$ be a multiplicative map from the positive reals to themselves satisfying $J(f(x)) = J(x)$ for all $x > 0$. If $f(2) = 2$, then $f(x) = x$ for every $x > 0$.
background
The canonical cost algebra equips the positive reals with multiplication and the J-cost function, where J satisfies the Recognition Composition Law. A J-automorphism is a multiplicative map that also preserves J-cost. The module develops algebraic closure properties of this structure. The key upstream result states: 'Pointwise, a J-automorphism can only choose the identity branch or the reciprocal branch.' This supplies the case split used throughout the proof.
proof idea
Apply JAut.ext to reduce to pointwise equality. For arbitrary x invoke eq_self_or_inv to obtain either f(x) = x (immediate) or f(x) = posInv x. In the latter case multiplicativity yields f(2x) = 2 * posInv x. A second application of eq_self_or_inv to 2x produces either x = 1 (contradicting the reciprocal assumption) or an immediate falsehood via two_mul_inv_ne_inv_two_mul.
why it matters in Recognition Science
This lemma is invoked inside eq_id_or_reciprocal to obtain the exact classification that every J-automorphism is either the identity or the reciprocal map. It closes the case analysis needed for the automorphism group of the cost algebra, reinforcing T5 J-uniqueness in the Recognition Science forcing chain. The parent result eq_id_or_reciprocal quotes the dichotomy directly from this theorem.
scope and limits
- Does not apply to maps lacking J-cost preservation.
- Does not classify automorphisms on structures other than positive reals.
- Does not address maps that fail multiplicativity.
- Does not claim every automorphism fixes 2.
formal statement (Lean)
871theorem eq_id_of_map_two_eq_two (f : JAut) (h2 : f posTwo = posTwo) : f = id := by
proof body
Tactic-mode proof.
872 apply JAut.ext
873 intro x
874 rcases eq_self_or_inv f x with hfx | hfx
875 · exact hfx
876 · have hmul : f (posMul posTwo x) = posMul posTwo (posInv x) := by
877 calc
878 f (posMul posTwo x) = posMul (f posTwo) (f x) := f.multiplicative posTwo x
879 _ = posMul posTwo (posInv x) := by rw [h2, hfx]
880 rcases eq_self_or_inv f (posMul posTwo x) with htx | htx
881 · have hx1 : x = posOne := (two_mul_inv_eq_two_mul_iff x).mp (hmul.symm.trans htx)
882 subst x
883 simpa [id] using hfx
884 · exact False.elim ((two_mul_inv_ne_inv_two_mul x) (hmul.symm.trans htx))
885
886/-- The reciprocal automorphism is genuinely nontrivial. -/