interpret_eq_parity
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert injectivity of the interpretation map.
- Does not derive the full set of Peano axioms in the realized structure.
- Does not extend to non-Boolean realizations or continuous carriers.
- Does not provide explicit computation of the interpretation beyond parity equivalence.
formal statement (Lean)
255theorem interpret_eq_parity (n : LogicNat) :
256 StrictLogicRealization.interpret strictBooleanRealization n =
257 Nat.bodd (LogicNat.toNat n) := by
proof body
Term-mode proof.
258 induction n with
259 | identity => rfl
260 | step n ih =>
261 show xorBool true (StrictLogicRealization.interpret strictBooleanRealization n) =
262 Nat.bodd (Nat.succ (LogicNat.toNat n))
263 rw [xorBool_true, ih, Nat.bodd_succ]
264
265/-- Even though the carrier image collapses, the iteration object is the
266full `LogicNat`. Concretely: the interpretation map is not injective. -/