mul_pos
plain-language theorem explainer
For two signed orbit differences, the positive component of their product equals the sum of the products of matching signs. Anyone building integer or rational arithmetic on orbits cites this as the definitional expansion of multiplication. The proof is pure reflexivity: the identity is the defining clause of mul.
Claim. Let $a=(a_+,a_-)$ and $b=(b_+,b_-)$ be signed orbit differences (intended value $a_+-a_-$ and $b_+-b_-$). Writing $a\cdot b$ for their product in the same representation, the positive component satisfies $(a\cdot b)_+ = a_+ b_+ + a_- b_-$.
background
The ambient module builds integers and rationals from primitive recognition data. A SignedOrbit is a pair of distinction naturals (pos, neg) whose intended meaning is the difference pos − neg (K4.6). This is the same difference-pair pattern used for logic integers elsewhere in the foundation, where negation swaps the two components.
Multiplication of difference pairs follows the usual expansion $(a_+-a_-)(b_+-b_-)$: the non-negative part collects the like-sign products $a_+b_+ + a_-b_-$, and the negative part collects the cross terms. The present lemma names only the positive projection of that product.
Distinction naturals carry the additive and multiplicative structure inherited from the orbit arithmetic layer; the identity here is purely structural on those components.
proof idea
One-line definitional proof (rfl). The multiplication operation on signed orbits is defined so that its .pos field is exactly a.pos * b.pos + a.neg * b.neg; the theorem is the corresponding projection equation, marked @[simp] for automatic unfolding.
why it matters
This is a foundational simp fact for the multiplicative structure of signed orbits inside Primitive Recognition Calculus. It lets later arithmetic (integer embedding via toInt, rational constructions, cost ledgers) reduce products componentwise without unfolding definitions by hand.
Downstream, positivity and product reasoning in cost algebra, path interpolation, and rung-scaled astrophysical and chemical formulae repeatedly need the positive part of a product to stay under control; the signed-orbit form of that identity sits at the base of the integer/rational stack those developments rely on. In the broader RS forcing picture it is scaffolding for the arithmetic that underwrites J-cost evaluations and phi-ladder bookkeeping, not a forcing step itself (T5–T8 live higher up).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.