add
plain-language theorem explainer
Pointwise sum of two signed orbits: add the positive legs and the negative legs separately. Anyone building integer or rational arithmetic on recognition orbits cites this as the raw carrier operation before quotienting by balanced equivalence. The body is a two-field structure constructor, not a proof.
Claim. If $a=(a_+,a_-)$ and $b=(b_+,b_-)$ are signed orbits (pairs of distinction naturals, read as $a_+-a_-$ and $b_+-b_-$), their sum is the signed orbit $a+b:=(a_++b_+,\,a_-+b_-)$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg (K4.6). Distinction naturals are the non-negative counting objects built earlier in the foundation stack; signed orbits are the pre-quotient carriers for integers.
This module sits under Foundation and imports orbit arithmetic. The same pattern appears upstream in IntegersFromLogic, where integers are pairs of logic-naturals modulo the usual cross-sum relation, and negation swaps the two legs. Here the carrier is still unquotiented: addition is defined on representatives first.
A later private lemma records that this pointwise sum respects balanced equivalence (equality of integer displays), so the operation descends to the quotient when that layer is introduced.
proof idea
Definition only. The structure SignedOrbit has two fields; add fills pos by ordinary addition of the positive legs and neg by ordinary addition of the negative legs. No tactics, no lemmas in the body.
why it matters
Raw additive structure on signed orbits is the first arithmetic operation needed before integers and rationals can be recovered from recognition data. Downstream well-definedness (add_respects_balanced, add_respects_cross) and the integer display toInt rely on this carrier map. In the Recognition stack this is foundation scaffolding toward number systems forced from the recognition calculus, not yet a physics constant or forcing-chain step (T0–T8). No used-by edges are recorded yet; the definition exists so those respect lemmas and the eventual quotient group law can cite a single named operation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.