posTwo
plain-language theorem explainer
posTwo supplies the concrete element 2 inside the positive reals subtype that carries the canonical cost algebra. Algebraists classifying J-automorphisms cite it to anchor the case split between the identity and the reciprocal map. The definition is a direct subtype constructor that packages the numeral 2 with a norm_num proof of positivity.
Claim. $2$ as an element of the subtype of positive reals, i.e., the pair consisting of the real number 2 and the proof that $2 > 0$.
background
PosReal is the subtype of positive real numbers, written {x : ℝ // 0 < x}. This carrier supports the multiplication, inversion, and J-cost operations that appear throughout the cost algebra module. The local setting is the algebra of positive reals equipped with the Recognition Composition Law satisfied by J. The sole upstream dependency is the PosReal abbreviation itself, which supplies the domain on which all automorphisms and fixed-point arguments are stated.
proof idea
The definition is a direct subtype constructor. It applies the subtype pair constructor to the numeral 2 and discharges the positivity obligation with a single norm_num tactic.
why it matters
This constant anchors the classification of J-automorphisms. It is invoked in eq_id_of_map_two_eq_two to prove that any automorphism fixing 2 is the identity, and in eq_id_or_reciprocal to separate the identity case from the reciprocal case. In the Recognition Science framework it supplies the fixed point required for the uniqueness properties of J and for the self-similar structure on the positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.