xorBool_true
plain-language theorem explainer
The theorem states that exclusive-or with true implements boolean negation inside the strict discrete Boolean realization. Researchers verifying the Lawvere natural-number object across carriers would cite it when confirming that iteration survives the collapse to a two-element set. The proof is a one-line term-mode case split on the boolean argument followed by reflexivity.
Claim. For every boolean value $b$, the operation $xor(true, b)$ equals the negation of $b$.
background
The NaturalNumberObject module characterizes the forced arithmetic via the Lawvere natural-number object: a triple $(N, z, s)$ such that for any pointed endomap $(X, x, f)$ there is a unique $h: N → X$ with $h(z)=x$ and $h∘s = f∘h$. The strict discrete Boolean realization supplies a two-element carrier whose step operation is realized by the xorBool function, defined as ordinary boolean exclusive-or. This lemma isolates the concrete action of one forcing step in that carrier.
proof idea
The proof is a one-line term-mode wrapper. It performs exhaustive case analysis on the boolean argument b and closes each branch by reflexivity.
why it matters
The result is invoked by interpret_eq_parity, which shows that the interpretation of any LogicNat element under the strict Boolean realization coincides with the parity map Nat.bodd ∘ toNat. It thereby confirms that the iteration object itself remains unchanged even when the orbit-as-set collapses to {false, true}, directly supporting the module claim that the natural-number object is independent of the concrete carrier. This closes one link in the chain from the universal forcing to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.