interpret_eq_parity
plain-language theorem explainer
The theorem equates the strict Boolean realization's interpretation of any LogicNat element to the parity of its iteration count. Researchers examining how arithmetic persists under carrier collapse in categorical foundations would cite it. The proof runs by induction on the LogicNat constructors, with the successor case reducing via the parity successor identity.
Claim. Let $n$ be an element of the logic-forced natural numbers. The interpretation of $n$ under the strict Boolean realization equals the parity of the natural-number iteration count of $n$.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step (one more iteration of the generator), as defined in ArithmeticFromLogic; toNat extracts the iteration count by recursing on the step constructor. StrictBooleanRealization is the discrete realization whose carrier is the two-element Boolean set, with interpretation defined by repeated application of the Boolean operation. The module establishes that LogicNat with identity and step forms a natural-number object in the Lawvere sense, and that every realization's forced arithmetic is likewise an NNO. The upstream result LogicNat.toNat supplies the forward map from the orbit to iteration count.
proof idea
The proof is by induction on n. The identity case holds by reflexivity. In the step case, the left-hand side is rewritten using xorBool_true to flip the parity, the inductive hypothesis is applied, and the right-hand side is matched using Nat.bodd_succ.
why it matters
This declaration is invoked by interpret_collapses to prove that the interpretation map fails to be injective. It thereby confirms that the iteration object remains the full LogicNat even when the carrier image collapses to the parity set. The result fills the module's claim that the strict Boolean realization preserves the natural-number object structure while collapsing the carrier, addressing the worry that iteration counting is presupposed rather than forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.