ext
Two J-automorphisms of the positive reals that agree pointwise are identical. Researchers working with the canonical cost algebra would invoke this to equate maps that coincide on the domain. The proof is a one-line wrapper that reduces equality of the subtype to function extensionality.
claimLet $f$ and $g$ be honest automorphisms of the positive reals (multiplicative maps that preserve the $J$-cost). If $f(x) = g(x)$ for every positive real $x$, then $f = g$.
background
The module Algebra.CostAlgebra develops the canonical cost algebra on positive reals. PosReal is the subtype of strictly positive reals. JAut is the subtype of maps from PosReal to PosReal that preserve posMul multiplication and satisfy J(f x) = J x for all x, encoding the preservation properties required by the Recognition Composition Law.
proof idea
The proof is a one-line wrapper. It applies Subtype.ext to reduce the claim to equality of the underlying functions, then funext to obtain pointwise equality from the hypothesis, and finally applies the given pointwise agreement.
why it matters in Recognition Science
This supplies the extensionality principle for JAut inside the cost algebra. It allows pointwise agreement to serve as equality when manipulating automorphisms that preserve the J-cost and the functional equation. The result sits at the base of algebraic work on the cost structure before any appeal to the forcing chain or physical constants.
scope and limits
- Does not prove existence of non-identity automorphisms.
- Does not extend beyond the positive reals.
- Does not impose or derive continuity or measurability.
- Does not connect to the eight-tick octave or spatial dimension D=3.
formal statement (Lean)
783@[ext] theorem ext {f g : JAut} (h : ∀ x : PosReal, f x = g x) : f = g := by
proof body
Term-mode proof.
784 apply Subtype.ext
785 funext x
786 exact h x
787
788/-- The identity automorphism. -/