boolCost
plain-language theorem explainer
Boolean comparison cost assigns zero to equal Boolean pairs and one to unequal pairs. Researchers working on discrete realizations of logic cite it as the compare operation inside the Boolean carrier of the second Law-of-Logic realization. The definition is a direct conditional on equality of the two inputs.
Claim. The function $c : Bool × Bool → ℕ$ is defined by $c(p,q) = 0$ if $p = q$ and $c(p,q) = 1$ otherwise.
background
The module DiscreteLogicRealization supplies the second Law-of-Logic realization, using a discrete Boolean/propositional carrier as the first non-continuous test case for Universal Forcing. The upstream definition in UniversalForcing.Strict.DiscreteBoolean provides the identical cost function, which is redeclared here to serve as the compare map. In the LogicRealization structure this cost pairs with the Carrier := Bool and zero := false to form a concrete instance.
proof idea
The definition is implemented directly as a conditional expression returning zero on equality and one on distinction.
why it matters
This supplies the compare function for boolRealization, the discrete propositional Law-of-Logic realization. It is invoked by the downstream theorems boolCost_self and boolCost_symm that verify the zero and symmetry axioms required for any valid cost. The declaration therefore anchors the discrete case inside the Universal Forcing chain before continuous extensions are considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.