pith. machine review for the scientific record. sign in
theorem proved term proof high

multiplicative

show as:
view Lean formalization →

Any J-automorphism f satisfies f(xy) = f(x)f(y) for positive reals x and y. Researchers proving uniqueness of the cost algebra or constructing morphisms between cost structures cite this when composing maps or verifying group structure on automorphisms. The proof is a direct one-line projection of the multiplicativity field from the JAut subtype definition.

claimLet $f$ be a J-automorphism of the positive reals. Then $f(xy) = f(x) f(y)$ for all positive reals $x, y$.

background

JAut is the subtype of maps from PosReal to PosReal that are multiplicative under posMul and preserve the J-cost, where J(x) = (x + x^{-1})/2 - 1. PosReal is the type of positive reals equipped with the multiplication posMul(x, y) = x y. This declaration lives in the CostAlgebra module, which equips the positive reals with the canonical cost algebra satisfying the Recognition Composition Law.

proof idea

One-line term proof that projects the first component of the JAut structure pair, which is the multiplicativity axiom by definition of the subtype.

why it matters in Recognition Science

The property is used in the definition of composition of JAut maps and in cost_algebra_unique_aczel, which establishes uniqueness of the cost function via Aczel's theorem. It supports the T5 uniqueness step in the forcing chain by confirming that automorphisms respect the multiplicative structure of the cost algebra.

scope and limits

Lean usage

rw [f.multiplicative x y]

formal statement (Lean)

 774theorem multiplicative (f : JAut) (x y : PosReal) :
 775    f (posMul x y) = posMul (f x) (f y) :=

proof body

Term-mode proof.

 776  f.2.1 x y
 777
 778/-- Cost preservation of a `J`-automorphism. -/

used by (40)

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

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.