ShiftedCarrier
plain-language theorem explainer
ShiftedCarrier denotes the set of real numbers bounded below by 1/2. This supplies the underlying carrier for the shifted monoid whose multiplication is A • B = 2AB. Workers extending the cost algebra to satisfy the Recognition Composition Law reference it to guarantee closure under that operation. The declaration is a direct subtype abbreviation with no lemmas or tactics.
Claim. $A = { x : ℝ | x ≥ 1/2 }$, the carrier set for the shifted monoid on reals.
background
The CostAlgebra module equips the J-cost with monoid operations compatible with the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). ShiftedCarrier restricts to the interval [1/2, ∞) so that the operation 2AB remains inside the set, matching the lower bound required by the shifted monoid of Theorem 2.7.
proof idea
Direct abbreviation to the subtype {A : ℝ // 1/2 ≤ A}. No lemmas are invoked; the definition simply packages the inequality for use in later monoid instances.
why it matters
ShiftedCarrier is the base type for shiftedCompose, shiftedUnit, and the CommMonoid instance that realize the algebraic structure demanded by the Recognition Composition Law. It implements the carrier of Theorem 2.7, supporting the phi-ladder scalings and the eight-tick octave by furnishing a closed domain for cost compositions. It closes the scaffolding step that lets downstream cost algebra connect to the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.