shiftedCompose
plain-language theorem explainer
The declaration defines the binary operation on the set of reals bounded below by 1/2 by doubling the ordinary product. Algebraists working on the monoid structure for J-cost composition would cite it when building the shifted carrier from Theorem 2.7. The proof is a direct pair construction that applies nlinarith to the input lower bounds to confirm closure.
Claim. Define the binary operation on the set $S = { x : ℝ | x ≥ 1/2 }$ by $x • y := 2xy$.
background
ShiftedCarrier is the set of real numbers at least 1/2, introduced as the carrier of the shifted monoid in Theorem 2.7. The module CostAlgebra develops algebraic operations on costs that are compatible with the J-functional and the Recognition Composition Law. Upstream results include the ShiftedCarrier abbrev itself together with A constants from IntegrationGap and Masses.Anchor that fix the active edge count per tick at 1.
proof idea
The definition builds a new element of ShiftedCarrier whose value is 2 times the product of the input values, then applies nlinarith to the lower-bound proofs A.2 and B.2 to discharge the membership obligation.
why it matters
This supplies the multiplication that immediately yields the Mul instance on ShiftedCarrier, completing the algebraic setup for the shifted monoid in Theorem 2.7. The construction supports later cost-composition lemmas in the same module and sits inside the T5 J-uniqueness step of the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.