add_mk
plain-language theorem explainer
Embedding two signed orbits and adding them equals embedding their sum under the integer-orbit display. Anyone simplifying arithmetic on distinction-based integers will fire this simp rule. The equality is definitional: both sides reduce by constructor unfolding, so the proof is a one-line rfl.
Claim. Let $a,b$ be signed orbits (pairs of distinction naturals read as positive minus negative part). If $\iota$ embeds a signed orbit into the integer-orbit display and $+$ is addition on that display, then $\iota(a)+\iota(b)=\iota(a+_{\mathrm{so}}b)$, where $+_{\mathrm{so}}$ is componentwise signed-orbit addition.
background
In the Primitive Recognition Calculus, integers are not taken as a primitive type. They are rebuilt from distinction data. A signed orbit is a pair (pos, neg) of distinction naturals, with intended meaning pos - neg (K4.6). That structure is the carrier for integer differences before any embedding into classical Int.
The ambient module then packages those signed orbits into an integer (and later rational) display. The map mk is the canonical embedding of a signed orbit into that display; add is addition on the display. A parallel structure RatioOrbit (K4.7) places a signed-orbit numerator over a nonzero distinction-natural denominator, so the same embedding discipline feeds both integer and rational layers.
Local arithmetic lemmas therefore split into two jobs: define operations on the raw orbit structures, and prove that the display operations commute with embedding. This declaration is the addition half of that commuting square.
proof idea
One-line definitional proof. After unfolding add on the integer display and mk on each argument, both sides are the same constructor application of the embedded SignedOrbit.add, so rfl closes the goal. No lemmas are invoked; the @[simp] attribute exists so downstream rewrites can discharge the commuting square automatically.
why it matters
Recognition Science rebuilds number systems from recognition/distinction data before any continuum or measure structure appears. This simp lemma is bookkeeping for that rebuild: it guarantees that integer addition on the display is exactly the image of signed-orbit addition, so later cost, ladder, and uniqueness arguments can move freely between the two presentations without hidden coercion gaps.
It sits in the K4.6 signed-orbit layer that underpins the K4.7 rational-orbit display. No downstream theorems currently list it as a direct dependency in the graph, but as a @[simp] rule it is meant to fire invisibly inside any proof that adds embedded integers. It does not itself touch the forcing chain (T5–T8), the Recognition Composition Law, or the mass ladder; it only keeps the integer substrate coherent for those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.