posHalf
plain-language theorem explainer
posHalf supplies the concrete element one half inside the positive reals that serve as the domain of the cost algebra. Algebraists verifying the inversion automorphism cite it to establish the mutual mapping between one half and two. The definition is a direct subtype construction whose positivity obligation is discharged by norm_num.
Claim. Let $1/2$ denote the subtype element $⟨1/2, 0 < 1/2⟩$ of the positive reals ${x : ℝ | 0 < x}$.
background
PosReal is the subtype ${x : ℝ | 0 < x}$ that forms the genuine positive domain of the canonical cost algebra. The CostAlgebra module equips this domain with multiplication, inversion, and composition operations that satisfy the Recognition Composition Law imported from FunctionalEquation and FunctionalEquationAczel. The constant one half is required for the basic scaling checks that confirm the inversion map is an automorphism.
proof idea
The definition is a one-line wrapper that applies the subtype constructor to the real 1/2 and discharges the positivity proof obligation with norm_num.
why it matters
posHalf is the concrete scaling element required by the downstream theorems posInv_half and posInv_two, which establish that inversion sends one half to two and conversely. These results supply the first consistency check for the automorphism group of the positive reals under the cost structure and anchor the discrete scaling steps that later connect to the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.