shiftedOfH
The definition maps each positive real x to the element H(x) inside the shifted carrier subtype. Researchers formalizing the monoid structure on cost functions cite this embedding when lifting the domain of the Recognition Composition Law. It proceeds by direct construction that pairs H(x) with the already-established bound H(x) ≥ 1.
claimFor every real number $x > 0$, the value $H(x) = J(x) + 1 = (x + x^{-1})/2$ satisfies $H(x) ≥ 1$ and therefore belongs to the shifted carrier subtype $A ∈ ℝ$ with $A ≥ 1/2$.
background
The shifted carrier is the subtype of real numbers bounded below by 1/2 that underlies the shifted monoid whose binary operation is defined by $A • B = 2AB$. The auxiliary function H is obtained from the J-cost by the translation H(x) = J(x) + 1, which converts the Recognition Composition Law into the classical d'Alembert functional equation H(xy) + H(x/y) = 2 H(x) H(y). The upstream result H_ge_one states that H(x) ≥ 1 whenever x > 0, which is the only fact needed to guarantee membership in the carrier.
proof idea
The definition is a one-line wrapper that applies the theorem H_ge_one x hx to obtain the inequality 1 ≤ H x and then uses linarith to witness the subtype predicate.
why it matters in Recognition Science
This definition supplies the canonical embedding of positive reals into the shifted monoid carrier required by the monoid structure of Theorem 2.7. It therefore sits at the interface between the cost algebra and the forcing chain (T5–T7) that produces the eight-tick octave and three spatial dimensions. No downstream uses are recorded yet, but the construction is a prerequisite for any later development that applies the shifted operation to physically realized quantities.
scope and limits
- Does not define or prove properties of the shifted monoid operation.
- Does not extend the map to non-positive reals.
- Does not compute explicit numerical values or relate H(x) to physical constants.
- Does not address the phi-ladder or mass formula.
formal statement (Lean)
268noncomputable def shiftedOfH (x : ℝ) (hx : 0 < x) : ShiftedCarrier :=
proof body
Definition body.
269 ⟨H x, by
270 have hHx : 1 ≤ H x := H_ge_one x hx
271 linarith⟩
272
273/-- The narrower `[1, ∞)` range supporting the actual values of `H`. -/