boolCost_symm
Symmetry of the Boolean comparison cost, which returns zero on equal propositions and one on distinct ones. Researchers building discrete logic realizations within the Recognition framework cite this to confirm the cost acts as an undirected comparison. The proof splits on whether the inputs agree and simplifies directly against the cost definition in each case.
claimFor all Boolean values $p$ and $q$, the comparison cost satisfies $cost(p,q)=cost(q,p)$, where $cost$ equals zero if $p=q$ and one otherwise.
background
The Boolean comparison cost is defined to return zero when its two inputs are equal and one when they differ. This module develops the strict discrete Boolean realization of propositional logic, in which the carrier is the Boolean type but the forced arithmetic is the free iteration object derived from the native generator rather than any finite image inside Bool.
proof idea
Case analysis on whether $p$ equals $q$. When they agree, substitution reduces both sides to the zero case of the cost definition. When they differ, the definition yields one on each side after the symmetric inequality is recorded.
why it matters in Recognition Science
The result is invoked in the construction of boolRealization, the discrete propositional Law-of-Logic realization, and strictBooleanRealization, the strict discrete Boolean realization. It supplies the symmetry required for the compare operation inside these structures, thereby supporting the development of strict forcing within the UniversalForcing chain.
scope and limits
- Does not establish symmetry for carriers other than Bool.
- Does not relate the cost to J-cost or the phi-ladder.
- Does not prove arithmetic equivalence of the strict realization.
- Does not extend to continuous or real-valued propositions.
formal statement (Lean)
25theorem boolCost_symm (p q : Bool) : boolCost p q = boolCost q p := by
proof body
Tactic-mode proof.
26 by_cases h : p = q
27 · subst h
28 simp [boolCost]
29 · have h' : q ≠ p := by intro hq; exact h hq.symm
30 simp [boolCost, h, h']
31