toInt
plain-language theorem explainer
Maps a signed orbit (a pair of distinction naturals read as positive and negative parts) to the ordinary integer given by the difference of their iteration counts. Cited wherever a verifier needs a concrete ℤ readout of a PRC integer carrier. The body is a direct cast-and-subtract of the two toNat projections; no proof obligations.
Claim. For a signed orbit $z=(p,n)$ consisting of two distinction naturals, set $\mathrm{display}(z) := \#p - \#n \in \mathbb{Z}$, where $\#$ is the iteration count of the underlying logic natural.
background
In the Primitive Recognition Calculus, integers are packaged as signed differences of orbits. A signed orbit is a structure with two distinction-natural fields, positive and negative, whose intended meaning is the difference of those parts (K4.6).
Distinction naturals inherit the forward map from logic naturals that reads off the iteration count: the identity orbit maps to $0$, and each step increments by one. Casting that count into $\mathbb{Z}$ and subtracting yields a classical integer display.
The same pattern appears upstream in the logic-integer development, where pairs of logic naturals are quotiented to form a carrier and a recovery map sends each class to an ordinary integer. Here the carrier is still the raw pair; the display does not yet impose the usual equivalence.
proof idea
Pure definition, not a theorem. Project the positive and negative distinction naturals, apply the iteration-count map on each, cast both results to $\mathbb{Z}$, and subtract. No lemmas and no tactics.
why it matters
Gives the verifier-facing integer display for signed orbits in the PRC foundation layer. Parallel recovery maps on the logic-integer side power the carrier equivalence with $\mathbb{Z}$, the transfer principle that an equation of logic integers holds exactly when it holds after display, and the no-zero-divisors and cancellation laws proved by reduction to ordinary $\mathbb{Z}$. This definition is the corresponding readout on the recognition-calculus carrier, so later arithmetic identities and ring facts can be stated against a concrete integer rather than an abstract pair.
It sits early in the arithmetic-from-logic stack that underwrites the forcing chain's discrete counting structure (octave ticks, rung indices on the $\varphi$-ladder), without yet claiming a full ring isomorphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.