interpret_eq_parity
plain-language theorem explainer
The theorem states that under the strict Boolean realization the interpretation of any element of the logic-forced natural numbers equals the boolean parity of its iteration count. Researchers deriving arithmetic from the Law of Logic or studying Lawvere natural-number objects would cite it to confirm that iteration count is recovered even after carrier collapse. The proof is by induction on the inductive structure of LogicNat, with the successor step reduced by rewriting with the xor-true identity and the standard parity successor lemma.
Claim. Let $N$ be the natural-number object generated by the Law of Logic, with elements built from the zero-cost identity and the successor step. For the strict Boolean realization, the interpretation map satisfies $interpret(n) = bodd(toNat(n))$ for every $n$ in $N$, where $toNat$ extracts the iteration count and $bodd$ returns the boolean parity.
background
The module shows that LogicNat, the inductive type with constructors identity (zero-cost element) and step (one further iteration of the generator), satisfies the Lawvere natural-number object universal property: it is initial among pointed endomap algebras. The toNat function is the unique homomorphism to the standard naturals, sending identity to 0 and step n to successor of toNat n. The strict Boolean realization is the model whose carrier collapses to two elements while preserving the iteration structure; its interpret function is defined via the Boolean operations on that carrier.
proof idea
Proof by induction on the LogicNat structure. The identity case is immediate by reflexivity. The step case reduces the goal to xorBool true applied to the interpretation of the predecessor equaling bodd of the successor of toNat n; this follows by three rewrites using the xorBool_true lemma, the inductive hypothesis, and Nat.bodd_succ.
why it matters
The result feeds directly into interpret_collapses, which uses it to prove the interpretation map is not injective. It supplies the formal answer, noted in the module documentation, to the objection that iteration counting was smuggled in: the parity of the count is recovered from the collapsed carrier, confirming that the iteration object itself is the unchanged natural-number object. The theorem therefore closes one step in the program of obtaining arithmetic from the Law of Logic without presupposing the naturals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.