comp_id
plain-language theorem explainer
The right unit law for composition of J-automorphisms states that composing the identity map with any such automorphism recovers the original map. Algebraists formalizing the multiplicative structure of the cost algebra would invoke this when establishing that the automorphisms form a monoid. The proof proceeds by applying the extensionality principle for these automorphisms and reducing pointwise to the identity function.
Claim. For every J-automorphism $f$, the composition of the identity automorphism with $f$ equals $f$.
background
JAut is the type of functions from positive reals to positive reals that are multiplicative under positive multiplication and preserve the J-cost function. Composition of two J-automorphisms is defined by ordinary function composition, which preserves both multiplicativity and J-preservation by direct verification. The identity automorphism is the map sending every positive real to itself, satisfying the two defining properties of JAut by reflexivity.
proof idea
The proof applies the extensionality lemma for JAut to reduce the equality of automorphisms to a pointwise statement, then introduces an arbitrary positive real and concludes by reflexivity.
why it matters
This supplies the right-neutral element for the monoid of J-automorphisms, which is used by downstream theorems establishing right-neutrality for recognition automorphisms and symmetry maps. It forms part of the algebraic layer supporting the Recognition Composition Law and the uniqueness properties of J in the forcing chain from T5 onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.