shiftedUnit
plain-language theorem explainer
shiftedUnit supplies the unit element 1/2 of the shifted monoid whose carrier consists of reals bounded below by 1/2. Researchers formalizing the cost algebra in Recognition Science reference this definition when instantiating the monoid structure. The construction is a one-line subtype pairing of the value 1/2 with the reflexivity of its lower bound.
Claim. The unit element of the shifted monoid is $1/2$ in the carrier set $A : {A : ℝ // 1/2 ≤ A}$.
background
The CostAlgebra module develops the algebraic operations for the Recognition Science cost functional. ShiftedCarrier is the subtype of real numbers A satisfying A ≥ 1/2, equipped with the operation A • B = 2AB that stays within the carrier. This monoid structure originates from Theorem 2.7 in the framework.
proof idea
This is a direct definition that constructs the subtype element by supplying the real value 1/2 together with the proof le_rfl that the bound holds with equality. It immediately enables the One instance on ShiftedCarrier defined in the same module.
why it matters
shiftedUnit completes the monoid unit for the shifted carrier, which is invoked by the theorem shiftedUnit_val to recover the real value 1/2. Within Recognition Science, this algebraic unit supports the composition law RCL and the J-cost functional by providing the neutral element under the shifted multiplication. It closes a basic step in the algebra underlying the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.