interpret_collapses
plain-language theorem explainer
The interpretation map from the forced natural numbers to the Boolean carrier in the strict realization is not injective. Researchers verifying Lawvere natural-number objects across realizations in Recognition Science cite this to confirm the iteration structure survives carrier collapse. The proof assumes injectivity, shows two distinct terms map to the same parity value via an auxiliary parity lemma, and reaches a contradiction with the zero-not-successor axiom.
Claim. The map sending each element of the Lawvere natural-number object to its parity bit under the strict Boolean realization is not injective.
background
The module establishes the Lawvere characterization of natural numbers in the forced arithmetic: a triple (N, z, s) is a natural-number object when for every (X, x, f) there is a unique h : N → X with h z = x and h ∘ s = f ∘ h. LogicNat is the inductive type generated by identity (zero-cost element) and step (one iteration of the generator), mirroring the orbit under multiplication by the self-similar fixed point. The strict Boolean realization collapses its carrier to the parity image Nat.bodd ∘ toNat, yet the iteration object itself remains unchanged.
proof idea
Assume the interpretation map is injective. Apply the parity lemma to obtain that identity maps to bodd 0 and step(step identity) maps to bodd 2. These Boolean values coincide by direct computation. The two LogicNat terms are nevertheless distinct by the zero-not-successor theorem. The assumed injectivity then forces them to be equal, yielding the contradiction.
why it matters
This theorem closes the critic's objection that iteration counting is smuggled into the Boolean case: the natural-number object is identical to the one in the continuous positive-ratio realization. It directly supports the claim that every realization's forced arithmetic is a natural-number object and that any two such objects are canonically isomorphic. The result sits inside the universal forcing chain and addresses the discrete Boolean carrier collapse while preserving the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.