comp_id
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the corresponding left identity law.
- Does not apply to functions outside the JAut subtype.
- Does not derive inverses or group structure.
- Does not impose or use continuity assumptions on the maps.
Lean usage
simp only [comp_id]formal statement (Lean)
819@[simp] theorem comp_id (f : JAut) : comp id f = f := by
proof body
Term-mode proof.
820 apply JAut.ext
821 intro x
822 rfl
823