pith. machine review for the scientific record. sign in
def definition def or abbrev high

comp

show as:
view Lean formalization →

Composition of J-automorphisms is defined by sequential application of the maps, with the resulting function verified to remain multiplicative and cost-preserving. Researchers constructing chains of automorphisms in the cost algebra cite this definition to close the monoid structure. The proof shape is a direct construction that invokes the multiplicativity and preservation properties of the factors in sequence.

claimLet $JAut$ be the type of maps $f:ℝ_{>0}→ℝ_{>0}$ satisfying $f(xy)=f(x)f(y)$ (with respect to positive multiplication) and $J(f(x))=J(x)$, where $J(x)=½(x+x^{-1})-1$. The composition of two such maps $g$ and $f$ is the map $x↦g(f(x))$, which again lies in $JAut$.

background

The J-cost function is the unique solution to the Recognition Composition Law on positive reals, given by $J(x)=½(x+x^{-1})-1$. JAut consists of those maps that are multiplicative with respect to posMul and preserve the value of J. The module develops the algebraic structure of these maps to support later constructions in action functionals and Hamiltonian mechanics. Upstream results include the definition of JAut itself together with the extraction theorems for its multiplicativity and cost-preservation properties.

proof idea

The definition builds the composite function explicitly and then constructs the proof object for the two JAut conditions. Multiplicativity of the composite is shown by rewriting first with the property of the inner map and then with the property of the outer map. Cost preservation follows by applying the preservation theorem of the outer map to the image under the inner map and then the preservation theorem of the inner map to the original argument.

why it matters in Recognition Science

This definition is a prerequisite for the monoid structure on JAut and is invoked in the classification result that every J-automorphism is either the identity or the reciprocal map. It supports downstream theorems on convexity of the J-action and energy conservation along trajectories. Within the Recognition Science framework it ensures closure of the automorphism group under composition, consistent with the derivation of the J-function from the functional equation.

scope and limits

formal statement (Lean)

 808def comp (g f : JAut) : JAut :=

proof body

Definition body.

 809  ⟨fun x => g (f x), by
 810    constructor
 811    · intro x y
 812      change g (f (posMul x y)) = posMul (g (f x)) (g (f y))
 813      rw [f.multiplicative x y, g.multiplicative (f x) (f y)]
 814    · intro x
 815      rw [g.preserves_cost (f x), f.preserves_cost x]⟩
 816

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.