boolCost
plain-language theorem explainer
The boolCost definition supplies a natural-number distance on pairs of boolean values, returning zero when the inputs match and one when they differ. Workers on discrete logic realizations inside the Recognition Science forcing chain cite it to equip the boolean carrier with a comparison metric. The definition is introduced by a direct case split on equality.
Claim. For propositions $p,q$ in the two-element boolean domain, the cost function returns $0$ when $p=q$ and $1$ otherwise.
background
The DiscreteBoolean module constructs the strict propositional realization whose carrier is the boolean type. The upstream DiscreteLogicRealization supplies the identical boolean comparison cost, described as zero for equality and one for distinction. The module documentation states that the carrier orbit remains periodic while the forced arithmetic is the free iteration object derived from the native generator.
proof idea
The declaration is a direct definition that evaluates the conditional expression if p = q then 0 else 1.
why it matters
This supplies the compare operation for boolRealization, the discrete propositional Law-of-Logic realization. It is invoked by the self and symmetry lemmas that follow and by the strictBooleanRealization construction inside UniversalForcing.Strict.DiscreteBoolean. The definition therefore anchors the boolean case of the discrete logic layer that feeds the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.