ShiftedHValue
plain-language theorem explainer
A subtype of the reals bounded below by 1 captures the image of the shifted cost H. Researchers extending cost composition laws in Recognition Science reference it to close algebraic operations on H-values. The declaration is a direct subtype abbreviation that encodes the range property H(x) >= 1 for x > 0.
Claim. Let $H(x) = J(x) + 1 = ½(x + x^{-1})$ for $x > 0$, where $J$ satisfies the Recognition Composition Law. The shifted H-value range is the set of reals $A$ such that $A ≥ 1$.
background
In the CostAlgebra module the shifted cost is introduced by H(x) := J(x) + 1, which converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). This reparametrization is imported from the FunctionalEquation module, where an analogous H appears as G_F + 1. The local setting is the algebraic closure of cost functions under composition, with J defined upstream as the cost function whose fixed point yields the golden ratio.
proof idea
The declaration is a direct abbreviation that introduces the subtype {A : ℝ // 1 ≤ A} with no lemmas or tactics applied.
why it matters
It supplies the carrier type for the semigroup structure built in shiftedComposeH and the instance shiftedComposeH_val, which in turn feeds shiftedHValueOf. The construction sits inside the defect pseudometric development and supports the translation of the Recognition Composition Law into an algebraic semigroup on the H-range, consistent with the eight-tick octave and phi-ladder structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.