posOne
plain-language theorem explainer
The definition supplies the positive real 1 as an element of the PosReal subtype inside the cost algebra. Researchers proving that J-automorphisms fixing 2 are identities cite this constant, as do simplification lemmas for inversion. It is introduced by a direct subtype constructor whose positivity obligation is discharged by norm_num.
Claim. Let $1$ denote the element of the subtype $PosReal := {x : ℝ | 0 < x}$ constructed as the pair $⟨1, 0 < 1⟩$.
background
PosReal is the subtype of strictly positive reals that serves as the carrier for the canonical cost algebra. The CostAlgebra module equips this domain with multiplication, inversion, and the J-functional satisfying the Recognition Composition Law. The supplied definition furnishes one of the distinguished constants required to close the automorphism argument.
proof idea
One-line definition that applies the subtype constructor to the real number 1 and invokes norm_num to confirm the positivity predicate.
why it matters
The constant appears in eq_id_of_map_two_eq_two, which proves that any JAut fixing posTwo equals the identity, and in the statements of posInv_one and two_mul_inv_eq_two_mul_iff. It thereby supports algebraic closure of the automorphism group for the J-cost function, consistent with the Recognition Science derivation of the functional equation from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.