boolCost_symm
plain-language theorem explainer
Symmetry of the Boolean comparison cost, zero on equality and one on distinction, follows from case analysis on whether the inputs match. Discrete logic workers in the Recognition framework cite this to confirm the compare operator is symmetric before assembling the full realization. The proof splits on equality, substitutes when true, and simplifies the definition in both branches.
Claim. $forall p, q in {true, false}, cost(p, q) = cost(q, p)$, where $cost(p, q) = 0$ if $p = q$ and $1$ otherwise.
background
The DiscreteLogicRealization module supplies the second Law-of-Logic realization via a discrete Boolean carrier, the first non-continuous test case for Universal Forcing. Its central definition is boolCost, which returns zero when two Booleans agree and one when they differ. The module imports UniversalForcing and draws on the step operation from CellularAutomata to enforce locality of updates.
proof idea
Case analysis via by_cases on p = q. The equal branch substitutes the hypothesis and simplifies directly from the boolCost definition. The unequal branch constructs the symmetric inequality q ≠ p and again simplifies the cost expression using the supplied inequalities.
why it matters
The result feeds boolRealization, which assembles the discrete propositional Law-of-Logic realization, and strictBooleanRealization in Strict.DiscreteBoolean. It supplies the required symmetry for the compare field in these structures, closing a basic algebraic check inside the discrete Boolean carrier for Universal Forcing. No direct tie to the phi-ladder or T5-T8 steps appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.