ext
plain-language theorem explainer
The extensionality theorem for J-automorphisms states that two maps in this subtype of multiplicative J-preserving functions on positive reals are identical whenever they agree at every point. Researchers formalizing the canonical cost algebra would cite it to equate morphisms without additional structure. The proof is a direct term-mode reduction that invokes subtype extensionality followed by function extensionality.
Claim. Let $f$ and $g$ be J-automorphisms of the positive reals, i.e., maps satisfying multiplicativity under posMul and preservation of the J-cost function. If $f(x) = g(x)$ for all $x > 0$, then $f = g$.
background
JAut is the subtype of maps from PosReal to PosReal that are multiplicative (f(posMul x y) = posMul (f x) (f y)) and preserve the J-cost (J((f x).1) = J(x.1)). PosReal is the subtype {x : ℝ // 0 < x} serving as the domain of the canonical cost algebra. The module CostAlgebra develops algebraic operations on this structure, importing the cost functional equation and its Aczel variant to ground the J-cost.
proof idea
The term proof applies Subtype.ext to equate the underlying functions, then funext to convert the pointwise hypothesis into equality of the function bodies, and finally exact to discharge the goal with the given h.
why it matters
This declaration supplies the extensionality principle required to manipulate JAut as ordinary maps inside the cost algebra. It underpins uniqueness arguments that feed into the J-uniqueness step (T5) of the forcing chain, where J(x) = (x + x^{-1})/2 - 1 is isolated as the canonical cost function. No downstream uses are recorded yet, leaving its role as a foundational lemma for later algebraic identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.