SignedOrbit
plain-language theorem explainer
Signed orbits package a pair of finite distinction orbits as an integer difference: positive part minus negative part. Anyone building integer arithmetic, divisibility, or delta-forced physical carriers on the primitive recognition calculus cites this carrier. It is a bare structure definition with decidable equality, not a proved claim.
Claim. A signed orbit is a pair $(p, n)$ of finite distinction orbits (base-neutral iterated distinctions), intended to mean the integer difference $p - n$. Equality of signed orbits is decidable.
background
In the primitive recognition calculus, DistinctionNat is the inductive carrier of finite orbits of repeated distinction: zero and successor, with no preferred base. It plays the role of the naturals built only from recognition steps.
Signed orbits lift that carrier to differences. The construction mirrors the classical pair model of integers and the logic-level negation that swaps components: a signed orbit is two distinction orbits, read as positive minus negative. The module sits after orbit arithmetic and feeds integer growth, divisibility, and delta-forced physical reality.
K4.6 names the intended meaning explicitly as that difference. Downstream code displays a signed orbit as an ordinary integer via a verifier map, so the pair is the native object and $\mathbb{Z}$ is the readout.
proof idea
No proof body: this is a structure declaration. Two fields of type distinction-orbit, with derived decidable equality and a printable representation. All content lives in the namespace that follows (integer readout, zero, arithmetic, balance).
why it matters
This is the integer carrier inside primitive recognition calculus. Grow.IntegerDivisibility builds balanced pairs, integer readout equality, and the divisibility relation dvdZ on signed orbits; additivity and reflexivity of that relation go through the integer display. DeltaForced identifies physically real carriers with delta-forced ones, and signed orbits supply the discrete signed counts those certificates manipulate.
In the broader forcing picture, integers arise from logic-level distinction before continuum structure. Signed orbits are the K4.6 step that turns unsigned distinction orbits into differences, so later mass-ladder, gap, and ledger constructions can talk about signed tallies without smuggling classical $\mathbb{Z}$ as a primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.