posTwo
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 in Recognition Science
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.
scope and limits
- Does not define multiplication or inversion on positive reals.
- Does not prove any property of the cost function J itself.
- Does not extend the algebra to non-positive numbers.
- Does not address the functional equation or physical constants.
Lean usage
theorem fix_two_implies_id (f : JAut) (h : f posTwo = posTwo) : f = id := eq_id_of_map_two_eq_two f hformal statement (Lean)
744def posTwo : PosReal := ⟨2, by norm_num⟩