boolCost_self
plain-language theorem explainer
The Boolean comparison cost vanishes on the diagonal. Researchers constructing discrete logic realizations within the Recognition Science forcing chain cite this when confirming that the zero element of the cost structure is attained inside the Bool carrier. The proof is a one-line wrapper that reduces the statement directly to the definition of the comparison cost.
Claim. For any Boolean value $p$, the Boolean comparison cost satisfies $C(p,p)=0$, where $C$ returns zero on equality and one on distinction.
background
The module supplies the strict discrete Boolean realization inside UniversalForcing.Strict.DiscreteBoolean. Its carrier is the type Bool and its cost function takes values in the naturals. The Boolean comparison cost is the function that returns zero precisely when its two arguments are equal and one otherwise. This self-cost theorem is the diagonal case of that definition and is required before the realization can serve as the zero-cost element in downstream constructions.
proof idea
The proof is a one-line wrapper that applies simplification using the definition of the Boolean comparison cost.
why it matters
The result feeds the discrete propositional Law-of-Logic realization and the strict discrete Boolean realization. It supplies the required zero on the diagonal of the cost structure, which is a prerequisite for lifting the propositional carrier into the arithmetic and forcing steps of the T0-T8 chain. The theorem therefore anchors the logic layer before the phi-ladder and spatial-dimension constructions are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.