boolCost_self
plain-language theorem explainer
boolCost p p equals zero for any Boolean p, confirming zero cost on self-comparison in the discrete Boolean carrier. Researchers building logic realizations cite this when establishing the zeroCost instance for Bool. The proof reduces directly via simp on the cost definition.
Claim. For any Boolean value $p$, the comparison cost satisfies $boolCost(p,p)=0$, where $boolCost$ returns zero on equality and one on distinction.
background
boolCost is the Boolean comparison cost: zero for equality, one for distinction, defined by the conditional if p = q then 0 else 1. The module DiscreteBoolean supplies a strict version of the Boolean realization whose carrier is Bool but whose arithmetic derives from the native generator rather than the finite image inside Bool. An identical definition and self-cost theorem appear upstream in DiscreteLogicRealization.
proof idea
One-line wrapper that applies the simp tactic to the definition of boolCost.
why it matters
The result supplies the zero-cost property required by boolRealization (the discrete propositional Law-of-Logic realization with Carrier Bool and compare boolCost) and by strictBooleanRealization (the strict discrete Boolean realization that also installs xorBool as compose). It therefore anchors the discrete Boolean case inside UniversalForcing.Strict.DiscreteBoolean before any lift to the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.