boolCost
plain-language theorem explainer
The definition supplies the comparison cost for two boolean values in the strict discrete propositional realization. Workers constructing LogicRealization instances for discrete carriers in Recognition Science cite this when building the compare operation. It is introduced by a direct conditional on equality with no further reduction.
Claim. The cost of comparing two boolean values $p$ and $q$ equals zero when they are identical and equals one when they differ.
background
The Strict/DiscreteBoolean module supplies the strict Boolean/propositional realization. Its carrier orbit is periodic, yet the forced arithmetic remains the free iteration object derived from the native generator rather than the finite image inside Bool. The definition imports from PositiveRatio and re-uses the upstream comparison cost from DiscreteLogicRealization, whose doc-comment states it is the Boolean comparison cost: zero for equality, one for distinction.
proof idea
This is the base definition expressed by a single conditional expression that returns zero on equality and one on distinction. No lemmas or tactics are invoked.
why it matters
The definition supplies the compare field inside boolRealization, the discrete propositional Law-of-Logic realization. It is invoked by the self-cost and symmetry theorems in both DiscreteLogicRealization and Strict.DiscreteBoolean, and by strictBooleanRealization. It therefore anchors the discrete carrier used in the Universal Forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.