PosReal
plain-language theorem explainer
PosReal supplies the subtype of strictly positive reals that carries the canonical cost algebra. Researchers deriving J-automorphisms or applying the Recognition Composition Law cite it as the base space on which J(x) = (x + x^{-1})/2 - 1 is defined and preserved. The declaration is a direct subtype abbreviation requiring no lemmas.
Claim. Let $PosReal := {x ∈ ℝ | x > 0}$.
background
The CostAlgebra module builds the algebra of costs on positive reals, importing the J-functional and its functional equation from Cost.FunctionalEquation. J satisfies J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) together with non-negativity and the fixed-point relation at the golden ratio. PosReal is introduced precisely to restrict the domain so that every element admits a well-defined reciprocal and every operation stays inside the positive cone.
proof idea
The declaration is a one-line abbreviation of the subtype {x : ℝ // 0 < x}.
why it matters
PosReal anchors every subsequent construction of JAut and the classification theorems that follow from it, including eq_self_or_inv and continuous_bijective_preserves_J_eq_id_or_inv. Those results realize the uniqueness of J-automorphisms required by the T5 step of the forcing chain and feed the Recognition Composition Law into the derivation of three spatial dimensions. The definition therefore closes the interface between the abstract functional equation and the concrete positive reals used throughout the algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.