comp_apply
The theorem states that the composition of two J-automorphisms g and f applied to a positive real x equals g applied to f x. Researchers deriving the ODE from the d'Alembert equation or establishing strict convexity of Jcost cite this when unfolding compositions in algebraic reductions. The proof is immediate from the pointwise definition of the composition operation on JAut.
claimFor J-automorphisms $g, f$ and positive real $x$, the composite satisfies $(g ∘ f)(x) = g(f(x))$.
background
JAut is the subtype of maps from PosReal to PosReal that are multiplicative under posMul and preserve the J-cost function. PosReal is the subtype of positive reals. The module develops the algebra of cost functions obeying the Recognition Composition Law. The upstream comp definition constructs the composite JAut by pointwise application while preserving the automorphism axioms.
proof idea
One-line wrapper that applies reflexivity to the definition of comp, which is constructed explicitly as the pointwise map fun x => g (f x).
why it matters in Recognition Science
This identity is invoked repeatedly in downstream derivations such as dAlembert_to_ODE_general_theorem and dAlembert_to_ODE_theorem in FunctionalEquation and AczelTheorem, as well as in Jcost_strictConvexOn_pos. It supplies the algebraic simplification step needed to pass from the functional equation to the second-order ODE that recovers the hyperbolic cosine form of J. The result sits inside the J-uniqueness and RCL infrastructure of the forcing chain.
scope and limits
- Does not establish existence or classification of non-identity elements of JAut.
- Does not address continuity, differentiability, or measurability of the automorphisms.
- Does not extend the identity to other algebraic structures or non-positive domains.
- Does not derive the Recognition Composition Law itself.
Lean usage
example (g f : JAut) (x : PosReal) : comp g f x = g (f x) := by simp [comp_apply]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)
-
dAlembert_to_ODE_general -
dAlembert_to_ODE_general -
cosh_strictly_convex -
Jcost_strictConvexOn_pos -
dAlembert_to_ODE_general_theorem -
dAlembert_to_ODE_theorem -
even_deriv_at_zero -
dAlembert_to_ODE_theorem -
comp -
dalembert_deriv_ode -
conservation_from_balance -
regge_sum_cubicHinges -
realizationOrbit_isNNO -
CE_factor -
involutionOp_shiftInvOp -
involutionOp_shiftOp -
shiftInvOp_shiftOp -
shiftOp_shiftInvOp -
physical_equiv_symm -
conserved_iff_conserved' -
symmetry_comp -
compAutomorphism -
compAutomorphism_inv_left_toFun -
compAutomorphism_inv_right_toFun -
compSymmetry -
gaugeEquivalent_trans -
channel_mono_transfer -
rank_invariant -
low_temp_limit