shiftedCompose_val
plain-language theorem explainer
The equality states that the shifted monoid product on reals at least 1/2 projects back to twice the ordinary product of the components. Algebraists checking the monoid induced by the reparametrized cost H would cite this when confirming the concrete multiplication rule. The proof is immediate reflexivity from the definition of the shifted operation.
Claim. For all $A, B$ in the shifted carrier set of reals bounded below by $1/2$, the underlying real value of their product under the shifted multiplication equals $2AB$.
background
The CostAlgebra module equips the shifted cost with monoid structure. ShiftedCarrier is the subtype of reals $x$ satisfying $x >= 1/2$. The shifted operation is defined by $A • B = 2AB$, selected so the reparametrized function $H(x) = J(x) + 1 = (x + x^{-1})/2$ satisfies the d'Alembert form of the Recognition Composition Law. Upstream, H is introduced in CostAlgebra.H as the convenience shift of J, and the same H appears in FunctionalEquation.H as $G_F + 1$. Arithmetic lemmas mul, mul_one and one_mul from the foundation modules supply the ring identities used in the surrounding CommMonoid instance.
proof idea
The theorem is a one-line wrapper. It reduces directly to the definition of multiplication on ShiftedCarrier via reflexivity, with no additional lemmas required beyond the subtype projection.
why it matters
The result supplies the explicit evaluation rule for the shifted monoid operation that underlies the CommMonoid instance on ShiftedCarrier. It completes the algebraic translation of the Recognition Composition Law into the H-variable, linking to T5 J-uniqueness and the phi-ladder construction. No downstream uses are recorded yet, so the declaration remains local scaffolding for later cost-algebra theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.