ShiftedHValue
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that H attains every value in [1, ∞).
- Does not equip the subtype with operations or a metric.
- Does not reference physical constants, dimensions, or the phi-ladder.
- Does not address multi-agent or higher-dimensional extensions.
formal statement (Lean)
274abbrev ShiftedHValue := {A : ℝ // 1 ≤ A}
proof body
Definition body.
275
276/-- The shifted operation is closed on the `H`-value range `[1, ∞)`. -/