ofInt_zero
plain-language theorem explainer
Embedding the ordinary integer 0 into the primitive recognition calculus integers recovers the PRC zero element. Anyone simplifying ofInt expressions or normalizing integer displays will cite this simp lemma. The proof is a two-line injectivity argument: both sides agree under the toInt display, so injectivity forces equality.
Claim. The canonical embedding of the verifier integer $0$ into the PRC integers equals the PRC zero: $\iota(0) = 0_{\mathrm{PRC}}$.
background
In the primitive recognition calculus, integers are built as signed distinction orbits rather than as a bare copy of $\mathbb{Z}$. The constructor that lifts a verifier integer $n$ routes its positive and negative parts through the $\delta$-orbit and packages them as a PRC integer. The zero element of that type is the orbit pair with both sides trivial.
A display map sends each PRC integer back to an ordinary verifier integer. Upstream result K4.8 records that this display is injective: distinct PRC integers have distinct verifier displays. That injectivity is the only nontrivial lemma needed here.
The local module develops the integer and rational layer of the primitive recognition calculus, sitting above orbit arithmetic and feeding the broader foundation forcing chain.
proof idea
Term-mode proof in two steps. Apply injectivity of the toInt display to reduce the goal to an equality of ordinary integers. Then simp closes both sides: the display of the embedded zero and the display of the PRC zero are definitionally the same verifier $0$.
why it matters
This is a basic normalization fact for the PRC integer embedding. Without it, simp-driven rewrites involving the zero rung stall. It sits in the foundation layer that constructs integers from distinction orbits, upstream of the forcing chain landmarks (T5 J-uniqueness through T8 dimension three), though it does not itself invoke J-cost, phi, or the eight-tick octave.
No downstream theorems currently list it as a direct dependency in the graph; its value is as a tagged simp lemma that keeps integer identities in normal form across the IntegerRational development. It closes a small but necessary coherence gap between the verifier $\mathbb{Z}$ and the orbit-based PRC integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.