shiftedComposeH
plain-language theorem explainer
shiftedComposeH equips the subtype of reals at least 1 with a binary operation that returns 2AB. A researcher using the shifted cost H in the Recognition Composition Law would cite this to guarantee closure of the H-range under the operation that corresponds to H(xy) + H(x/y). The definition is a one-line wrapper that builds the subtype element and discharges the bound 2AB ≥ 1 by nlinarith on the input proofs.
Claim. For $A, B$ in the subtype of reals satisfying $A, B ≥ 1$, the operation is defined by $A ⊙ B := 2AB$, which again lies in the same subtype.
background
ShiftedHValue is the subtype {r : ℝ | 1 ≤ r}, the range of the shifted cost function. The function H is defined by H(x) = J(x) + 1, or equivalently H(x) = ½(x + x⁻¹). Under this shift the Recognition Composition Law takes the d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y). The CostAlgebra module constructs algebraic structure on these H-values after importing the base cost definitions and the functional equation results.
proof idea
The definition refines a subtype pair whose first component is the real 2 * A.1 * B.1. The second component, the proof that this value is at least 1, is discharged by nlinarith using the two hypotheses A.2 and B.2 that record the input lower bounds. The same operation is then installed as the multiplication for the Mul instance on ShiftedHValue.
why it matters
The definition supplies the multiplicative closure needed for the H-values so that the d'Alembert form of the Recognition Composition Law can be used algebraically. It sits inside the cost algebra that supports the transition from the base J-cost to the shifted H-cost used in the forcing chain. No immediate downstream theorems are recorded, yet the operation is a prerequisite for any further ring or monoid structure on costs that would feed into mass formulas or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.