posMul
plain-language theorem explainer
Multiplication on positive reals is defined by lifting the real product to the positive subtype. Researchers classifying J-automorphisms in the cost algebra cite this when verifying multiplicativity of maps that preserve the cost function J. The definition is a direct subtype constructor using real multiplication and the mul_pos lemma.
Claim. For positive reals $x, y > 0$, the product is the positive real whose underlying value is $x · y$.
background
PosReal is the subtype of real numbers strictly greater than zero. This definition appears in the CostAlgebra module that constructs the algebraic operations compatible with the cost function J from Recognition Science. It depends only on the PosReal type itself.
proof idea
The definition is a one-line subtype constructor that multiplies the underlying real values and attaches the positivity proof via mul_pos.
why it matters
This operation is required to define the JAut type of maps that are multiplicative and preserve J. It supports the classification that the only continuous bijective J-preserving maps are the identity and reciprocal. The result feeds the algebraic structure used in the forcing chain and derivation of physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.