H_ge_one
plain-language theorem explainer
The shifted cost H satisfies H(x) ≥ 1 for every positive real x. Researchers constructing the shifted monoid or defect pseudometric in Recognition Science cite this bound to place H-values in the closed interval [1, ∞). The proof is a one-line wrapper that unfolds the definition of H and reduces the claim to non-negativity of J via linear arithmetic.
Claim. For every positive real number $x$, the shifted cost $H(x) := J(x) + 1 = ½(x + x^{-1})$ satisfies $H(x) ≥ 1$.
background
In CostAlgebra the shifted cost is introduced by the definition H(x) := J(x) + 1, which equals half the sum of x and its reciprocal. This reparametrization converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The local setting is the algebra of costs derived from the functional equation, where J encodes deviation cost and H shifts the range to begin at 1.
proof idea
The proof unfolds the definition of H, applies the sibling lemma establishing non-negativity of J on positive reals, and finishes with linear arithmetic.
why it matters
The bound is invoked directly by the definitions shiftedHValueOf and shiftedOfH that construct the canonical shifted-carrier elements. It anchors the positive branch of the cost functions used in the defect pseudometric d(x,y) = J(x/y) and feeds the downstream development of the phi-ladder. In the framework it closes the range statement required after J-uniqueness (T5) and before the eight-tick octave and D = 3 constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.