mul
plain-language theorem explainer
Defines multiplication on signed orbits by the classical difference-of-naturals rule: the product of two (pos − neg) pairs expands to a new signed pair with positive part p₁p₂ + n₁n₂ and negative part p₁n₂ + n₁p₂. Anyone building the integer or rational layer of the primitive recognition calculus cites this as the ring operation. The body is a pure structure constructor, no proof obligations.
Claim. For signed orbits $a = (p_1, n_1)$ and $b = (p_2, n_2)$, each intended as the difference of two distinction-naturals, their product is the signed orbit $(p_1 p_2 + n_1 n_2,\, p_1 n_2 + n_1 p_2)$, so that $(p_1 - n_1)\cdot(p_2 - n_2)$ holds in the intended integer interpretation.
background
A signed orbit is a pair of distinction-naturals (pos, neg) whose intended meaning is the integer difference pos − neg (K4.6). Distinction-naturals carry the additive and multiplicative structure lifted from the orbit arithmetic layer; the present module packages those pairs into a pre-integer type before quotienting by balanced equivalence.
The same difference-pair pattern appears upstream in IntegersFromLogic, where integers are quotients of pairs of logic-naturals and negation swaps the two components. Multiplication here is the unquotiented counterpart of that construction: expand $(p_1-n_1)(p_2-n_2)$ and collect positive and negative summands separately.
Local setting is the primitive recognition calculus integer/rational scaffold: signed orbits sit between raw orbit arithmetic and the eventual balanced-equivalence quotient that yields genuine integers.
proof idea
Pure definitional constructor. The two fields of the result are filled by the classical bilinears on distinction-naturals: positive part is the sum of the two same-sign products, negative part is the sum of the two opposite-sign products. No lemmas are invoked; well-typedness follows from the ambient * and + on DistinctionNat.
why it matters
This is the multiplicative half of the ring structure on signed orbits inside the foundation layer of Recognition Science. Together with addition (and the balanced-equivalence relation already present in-module), it supplies the arithmetic needed before one can form rationals or embed into the real/protocol layer.
No downstream theorems currently depend on it in the graph, so it is infrastructure rather than a cited lemma. It mirrors the classical construction used in IntegersFromLogic and keeps the recognition calculus self-contained: integers arise from distinction counts, not from an external ℤ. Framework-wise it sits well below the forcing chain (T0–T8); it is pure arithmetic scaffolding for later cost and ladder work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.