id
plain-language theorem explainer
The identity automorphism on positive reals is the map sending each element to itself while preserving multiplication and the J-cost function. Algebraists classifying automorphisms of the cost algebra cite this as the trivial case in the id-or-reciprocal theorem. It is constructed directly by packaging the identity function with reflexivity proofs for the two required properties.
Claim. The identity element of the automorphism group $JAut$ is the function $f : {>0} {>0}$ given by $f(x) = x$, which satisfies $f(xy) = f(x) f(y)$ and $J(f(x)) = J(x)$ for all positive reals $x, y$.
background
JAut is the subtype of maps from positive reals to positive reals that are multiplicative under posMul and preserve the J-cost function, where J satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The CostAlgebra module assembles this structure from the canonical cost algebra on {>0} and imports arithmetic identities from Foundation modules. The identity definition depends on the JAut type and on sibling constructions such as reciprocal.
proof idea
The definition is a one-line wrapper that supplies the identity function on PosReal and verifies the two JAut properties by reflexivity inside a constructor block.
why it matters
This definition supplies the base case for eq_id_or_reciprocal, which classifies every J-automorphism as either id or reciprocal, and for the closed theorem continuous_bijective_preserves_J_eq_id_or_inv. It anchors the T5 J-uniqueness step in the forcing chain by exhibiting the trivial solution and is referenced in comp_id, eq_id_of_map_two_eq_two, and intensityRatio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.