shiftedUnit_val
plain-language theorem explainer
The theorem fixes the value of the shifted unit element at one half in the reals. Algebraists working with monoid structures on the cost carrier would cite it to simplify neutral-element cases in composition expressions. The proof reduces to a single reflexivity step that matches the upstream definition of shiftedUnit.
Claim. The identity element of the shifted monoid satisfies $shiftedUnit = 1/2$.
background
ShiftedUnit is the identity element of the shifted monoid on the shifted carrier, defined as the pair consisting of one half together with the trivial lower bound. The CostAlgebra module constructs this monoid structure on top of the cost functional equation and its Aczel form, supplying the One instance for ShiftedCarrier. The upstream definition supplies the concrete value and the carrier membership proof.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of shiftedUnit.
why it matters
The result supplies the concrete neutral element required for algebraic simplifications inside the cost monoid. It supports later uses of costCompose and related associativity lemmas even though no direct downstream citations appear in the current mirror. Within the Recognition framework it aligns with the J-uniqueness step and the RCL by fixing the monoid unit in the shifted setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.