boolCost
plain-language theorem explainer
Boolean comparison cost assigns zero to equal propositions and one to distinct ones in the strict discrete setting. Researchers constructing LogicRealization instances for propositional logic under the Recognition forcing chain cite it when realizing discrete carriers. The definition proceeds by direct case distinction on boolean equality.
Claim. The comparison cost function on boolean values is defined by $c(p,q)=0$ if $p=q$ and $c(p,q)=1$ otherwise, for $p,q$ in the boolean type.
background
The Strict/DiscreteBoolean module develops the strict Boolean realization. The carrier orbit is periodic, yet the forced arithmetic is the free iteration object derived from the native generator rather than the finite image inside Bool. The boolCost supplies the comparison function for this realization.
proof idea
Direct definition via conditional expression on equality of the two boolean arguments, returning the corresponding natural number.
why it matters
This definition is used to construct boolRealization and to prove boolCost_self and boolCost_symm. It anchors the discrete propositional Law-of-Logic realization inside the Universal Forcing Strict module and supports the transition from logic to arithmetic costs in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.