shiftedComposeH
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not prove associativity, commutativity or other algebraic laws for the operation.
- Does not identify the operation with multiplication of underlying variables.
- Does not incorporate the full Recognition Composition Law beyond closure.
- Does not reference the phi-ladder, active edge count A or dimension D = 3.
formal statement (Lean)
277def shiftedComposeH (A B : ShiftedHValue) : ShiftedHValue := by
proof body
Definition body.
278 refine ⟨2 * A.1 * B.1, ?_⟩
279 nlinarith [A.2, B.2]
280
281instance : Mul ShiftedHValue := ⟨shiftedComposeH⟩
282