xorBool
xorBool supplies the composition operation for the strict discrete Boolean realization in the forcing chain. It implements exclusive disjunction on the two-element carrier. Researchers constructing the natural number object cite it when showing that the interpretation map recovers parity after orbit collapse to {false, true}. The definition is a direct one-line alias to the built-in Boolean exclusive-or primitive.
claimThe binary operation of exclusive disjunction on the Boolean domain is defined by $poplus q := neg(p leftrightarrow q)$.
background
The module sets the strict Boolean realization of universal forcing, with carrier the periodic orbit on the two-element set but arithmetic given by the free iteration object from the native generator rather than any finite image inside Bool. The composition law is the required operation that keeps the iteration free. This sits downstream of the PositiveRatio import and supplies the compose field for the realization used in the natural number object.
proof idea
The definition is a one-line wrapper that applies the standard Boolean exclusive-or primitive directly to the input pair.
why it matters in Recognition Science
This definition populates the compose field of strictBooleanRealization, which is invoked to prove interpret_eq_parity establishing that the Boolean interpretation equals the parity map on LogicNat. It thereby shows iteration count survives collapse of the orbit to {false, true}. In the Recognition framework this discretizes the Boolean case of the T7 eight-tick octave for the natural number object construction.
scope and limits
- Does not extend the operation beyond the two-element Boolean domain.
- Does not prove algebraic properties such as associativity or commutativity.
- Does not define or use the cost or comparison functions, which appear in sibling definitions.
- Does not address continuous or non-discrete realizations of the forcing chain.
Lean usage
def strictBooleanRealization : StrictLogicRealization where Carrier := Bool Cost := Nat zeroCost := inferInstance compare := boolCost compose := xorBoolformal statement (Lean)
32def xorBool (p q : Bool) : Bool :=
proof body
Definition body.
33 xor p q
34
35/-- Strict discrete Boolean realization. -/