mul_neg
plain-language theorem explainer
For signed orbit differences (pairs meaning pos − neg), the negative component of a product is the cross term a₊b₋ + a₋b₊. Anyone expanding products of signed orbits in the primitive recognition calculus cites this. The proof is pure definitional equality (rfl), so simp rewrites it automatically.
Claim. Let $a=(a_+,a_-)$ and $b=(b_+,b_-)$ be signed orbit differences (intended meaning $a_+-a_-$). Then the negative component of the product satisfies $(a\cdot b)_- = a_+ b_- + a_- b_+$.
background
In the primitive recognition calculus, integers are built before classical $\mathbb{Z}$ by tracking distinction counts. A SignedOrbit is a pair of distinction naturals $(pos, neg)$ with intended meaning $pos - neg$ (K4.6). This mirrors the LogicInt construction, where negation swaps components: $-(a,b)=(b,a)$.
Multiplication of signed differences expands as ordinary difference-of-products: $(a_+-a_-)(b_+-b_-)$ has positive part $a_+b_+ + a_-b_-$ and negative (cross) part $a_+b_- + a_-b_+$. The module sits under Foundation.PrimitiveRecognitionCalculus and imports orbit arithmetic, so these component identities are the native ring laws before embedding into reals or rationals.
Upstream, analogous neg operations appear for LogicInt, LogicRat, and Protocol approximations; all swap or flip the signed data. The present lemma is the component-level statement for the product's negative half.
proof idea
One-line definitional proof: rfl. The multiplication of signed orbits is defined so that the .neg field of mul a b is exactly a.pos * b.neg + a.neg * b.pos. No lemmas are applied; simp can fire the equality by unfolding.
why it matters
This simp rule is infrastructure for signed-orbit arithmetic used throughout Grow lemmas (order comparisons via toNat, right-multiplication inequalities under nonneg flags, balanced-product congruences) and feeds ratio-orbit density arguments such as ltQ_iff_toNat.
Downstream cost and d'Alembert pipelines (dAlembert_to_ODE_general, dAlembert_to_ODE_theorem, FourthGate dalembert_deriv_ode) depend on clean signed arithmetic when reducing functional equations to ODEs. In the Recognition forcing chain, the cost $J$ and the Recognition Composition Law sit on top of this integer/rational substrate; component identities like mul_neg keep the discrete ledger honest before continuum limits.
It is not a deep theorem: it closes the algebraic interface so later uniqueness and ODE bootstrap steps do not re-prove cross-term bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.