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

reciprocal

show as:
view Lean formalization →

The reciprocal automorphism inverts positive reals while preserving both multiplication and the cost function J. Algebraists classifying symmetries of the cost algebra cite this as the explicit non-identity element of JAut. The definition packages posInv together with direct verification of multiplicativity via commutativity and J-preservation via the reciprocal symmetry theorem.

claimThe reciprocal automorphism is the map $f(x) = x^{-1}$ on positive reals satisfying $f(xy) = f(x) f(y)$ and $J(f(x)) = J(x)$ for all positive $x, y$.

background

JAut is the type of maps from positive reals to positive reals that are multiplicative under posMul and preserve the cost function J. posInv supplies inversion on positive reals and posMul supplies their multiplication. Upstream J_reciprocal states that J(x) equals J of its reciprocal, which is the invariance used to close the second axiom. This definition lives inside CostAlgebra, the module that equips the positive reals with the algebraic structure required by Recognition Science's cost accounting.

proof idea

The definition supplies posInv as the underlying function and proves the two JAut properties inside a constructor. Multiplicativity is obtained by Subtype.ext followed by simp using posMul, posInv and mul_comm. J-preservation follows immediately from the theorem J_reciprocal applied to the underlying real and its positivity witness.

why it matters in Recognition Science

This supplies the non-identity element required by eq_id_or_reciprocal, which classifies every J-automorphism as either the identity or the reciprocal map. It is also invoked inside continuous_bijective_preserves_J_eq_id_or_inv to close the automorphism group under stronger assumptions. In the Recognition framework the construction realizes the inversion symmetry that follows from J-uniqueness, where J(x) = J(1/x) encodes the double-entry balance of costs.

scope and limits

Lean usage

example : JAut := reciprocal

formal statement (Lean)

 798noncomputable def reciprocal : JAut :=

proof body

Definition body.

 799  ⟨posInv, by
 800    constructor
 801    · intro x y
 802      apply Subtype.ext
 803      simp [posMul, posInv, mul_comm]
 804    · intro x
 805      simpa [posInv] using (J_reciprocal x.1 x.2).symm⟩
 806
 807/-- Composition of `J`-automorphisms. -/

used by (40)

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

… and 10 more

depends on (12)

Lean names referenced from this declaration's body.