pith. machine review for the scientific record. sign in
theorem other other high

comp_apply

show as:
view Lean formalization →

Composition of J-automorphisms acts by successive application on positive reals. Researchers deriving the ODE from the d'Alembert equation in the cost algebra cite this when unfolding maps during algebraic reductions. The proof is immediate reflexivity from the explicit definition of comp.

claimFor $J$-automorphisms $g,f$ and positive real $x$, the composition satisfies $(g∘f)(x)=g(f(x))$, where a $J$-automorphism is a multiplicative map $f:ℝ_{>0}→ℝ_{>0}$ obeying $J(f(x))=J(x)$.

background

JAut is the subtype of maps on PosReal that are multiplicative and preserve the value of J. PosReal is the subtype of positive reals. The operation comp constructs a new JAut by pointwise application of the outer map to the image of the inner map, inheriting multiplicativity from the factors. This construction lives in the CostAlgebra module that equips the positive reals with the canonical cost structure satisfying the Recognition Composition Law.

proof idea

One-line wrapper that applies reflexivity to the definition of comp, which is constructed explicitly as the map sending x to g (f x).

why it matters in Recognition Science

This result is invoked in the derivations of dAlembert_to_ODE_general and dAlembert_to_ODE_theorem in the FunctionalEquation and AczelProof modules, as well as in the convexity statements for Jcost. It supplies the algebraic identity needed to manipulate composed maps while preserving the J-cost and multiplicativity properties that underpin the forcing chain from T5 J-uniqueness through the Recognition Composition Law.

scope and limits

formal statement (Lean)

 817@[simp] theorem comp_apply (g f : JAut) (x : PosReal) : comp g f x = g (f x) := rfl

proof body

 818

used by (29)

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

depends on (6)

Lean names referenced from this declaration's body.