JAut
plain-language theorem explainer
JAut is the subtype of maps from positive reals to positive reals that are multiplicative under the algebra's product and preserve the J-cost function. Algebraists and Recognition Science researchers cite it when classifying automorphisms of the cost structure or deriving uniqueness results for continuous bijections. The declaration is a direct subtype construction that encodes the two required properties without additional proof steps.
Claim. Let PosReal denote the positive reals. JAut is the type of all functions $f:$ PosReal $→$ PosReal such that $f(xy)=f(x)f(y)$ for every $x,y$ and $J(f(x))=J(x)$ for every $x$, where $J$ is the cost function on the positive reals.
background
PosReal is the subtype of reals consisting of strictly positive elements. posMul supplies the multiplication operation on this domain, defined by componentwise multiplication of the underlying reals while preserving positivity. J is the cost function whose functional equation is the Recognition Composition Law. The JAut definition lives inside the CostAlgebra module, which assembles the algebraic backbone for the forcing chain that begins with J-uniqueness at T5.
proof idea
The declaration is a direct subtype construction. It packages the multiplicativity condition with respect to posMul together with the J-preservation condition into a single bundled type; no lemmas or tactics are applied.
why it matters
JAut supplies the precise object needed for the automorphism classification theorems that follow. It is the domain of the composition operation and the source of the results eq_id_or_reciprocal and continuous_bijective_preserves_J_eq_id_or_inv. These theorems close the uniqueness step that follows from T5 J-uniqueness and the Recognition Composition Law, confirming that the only honest automorphisms are the identity and the reciprocal map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.