shiftedComposeH_val
plain-language theorem explainer
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.
Claim. For $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.