shiftedHValueOf
plain-language theorem explainer
shiftedHValueOf packages the shifted cost H(x) together with the proof that it is at least 1 into the subtype of reals bounded below by 1, for any positive real x. Researchers working inside the cost algebra of Recognition Science cite it when they need a canonical inhabitant of the H-monoid from a raw positive input. The definition is realized as a one-line constructor that applies the H function and the H_ge_one theorem.
Claim. For any real number $x > 0$, the map returns the pair $(H(x), 1 ≤ H(x))$ as an element of the subtype $A ∈ ℝ$ with $1 ≤ A$, where $H(x) = ½(x + x^{-1})$.
background
In the CostAlgebra module the shifted cost is introduced by the definition H(x) := J(x) + 1, which equals ½(x + x^{-1}). This reparametrization converts the Recognition Composition Law into the d'Alembert functional equation H(xy) + H(x/y) = 2 H(x) H(y). The subtype ShiftedHValue is the narrower interval [1, ∞) that actually contains the image of H on positive reals.
proof idea
The definition is a one-line wrapper that applies the H function to x and pairs the result with the proof term supplied by the upstream theorem H_ge_one x hx.
why it matters
The constructor supplies the basic embedding of positive reals into the H-value subtype that the rest of the cost algebra relies upon. It immediately precedes the Defect Pseudometric section, where distances are defined via J(x/y). In the Recognition framework it closes the passage from the raw positive line to the shifted monoid underlying the eight-tick octave and the forcing of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.