shiftedComposeH_val
The theorem states that for shifted H-values A and B (reals at least 1), the underlying real of their product under the shifted multiplication equals twice the product of those reals. Algebraists building the cost semigroup in Recognition Science would cite it to confirm the multiplication rule on the H-image. The proof is immediate reflexivity because the operation on the subtype is defined to satisfy exactly this identity.
claimFor $A, B$ in the subtype of reals with $A, B ≥ 1$, if $⋅$ is the shifted multiplication on this subtype, then the underlying real of $A ⋅ B$ equals $2AB$.
background
ShiftedHValue is the subtype {A : ℝ // 1 ≤ A}, the closed range [1, ∞) that contains all actual values of the shifted cost. The upstream definition H(x) := J(x) + 1 rewrites the Recognition Composition Law as the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). This theorem lives inside CostAlgebra and depends on the H definition in the same module together with the functional-equation reparametrization imported from Cost.FunctionalEquation.
proof idea
The proof is a one-line reflexivity tactic. The multiplication on ShiftedHValue is defined so that casting the product back to ℝ immediately yields 2 A.1 B.1; no further lemmas are required. The CommSemigroup instance that follows then invokes this identity inside ring tactics to obtain associativity and commutativity.
why it matters in Recognition Science
The result supplies the concrete multiplication rule needed to equip the image of H with a commutative semigroup structure, which is the algebraic setting in which the d'Alembert form of the Recognition Composition Law is realized. It closes the local algebraic layer before cost-composition theorems are stated. No downstream uses are recorded yet, but the declaration directly supports the transition from the J-cost to the H-cost throughout the framework.
formal statement (Lean)
283@[simp] theorem shiftedComposeH_val (A B : ShiftedHValue) :
284 ((A * B : ShiftedHValue) : ℝ) = 2 * A.1 * B.1 := rfl
proof body
Tactic-mode proof.
285
286instance : CommSemigroup ShiftedHValue where
287 mul := (· * ·)
288 mul_assoc A B C := by
289 apply Subtype.ext
290 change 2 * (2 * A.1 * B.1) * C.1 = 2 * A.1 * (2 * B.1 * C.1)
291 ring
292 mul_comm A B := by
293 apply Subtype.ext
294 change 2 * A.1 * B.1 = 2 * B.1 * A.1
295 ring
296
297/-- The `H`-value of a positive real belongs to the closed range `[1, ∞)`. -/