abs_mul_eq_of_balanced_left
plain-language theorem explainer
If two signed orbits represent the same integer, their products with any third orbit have equal absolute values. Order and magnitude lemmas in the primitive recognition calculus cite this when reducing absolute values under the internal balance relation. The proof is a short term chain: injectivity of the natural display, absolute-value and multiplication bridges to ℤ, then substitution of equal integer displays.
Claim. Let $a$, $a'$, and $b$ be signed orbits. If $a$ and $a'$ are balanced (equivalently, they display the same integer), then $\lvert a \cdot b \rvert = \lvert a' \cdot b \rvert$ as distinction naturals.
background
In the primitive recognition calculus, integers are carried internally by signed orbits: pairs of distinction-natural positions (positive and negative legs). Two signed orbits are balanced when $a.\mathrm{pos}+a'.\mathrm{neg}=a'.\mathrm{pos}+a.\mathrm{neg}$; by the bridge lemma this is equivalent to equality of their conservative $\mathbb{Z}$ displays.
Absolute value of a signed orbit is the distinction-natural absolute difference of its legs, and its natural display equals $\mathrm{natAbs}$ of the integer display. Multiplication of signed orbits is defined so that the integer display of a product is the product of the displays.
This module builds the order surface on those internal objects. The present lemma is the left-factor compatibility of absolute value with the balance relation under multiplication.
proof idea
Apply injectivity of DistinctionNat.toNat to reduce equality of absolute values to equality of naturals. Rewrite both sides via abs_toNat (absolute value displays as Int.natAbs of toInt) and mul_toInt (product displays as the product of displays). Convert the balance hypothesis to equality of integer displays by balanced_iff_toInt_eq, then substitute. The two sides become natAbs(a.toInt * b.toInt) and natAbs(a'.toInt * b.toInt) with equal left factors, hence equal.
why it matters
Absolute value must be well-defined on balance classes if signed orbits are to serve as the internal integers of Recognition Science. This lemma supplies the left-multiplication half of that invariance.
It is consumed by integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed. That certificate packages display bridges for truncated subtraction, order, absolute difference, and nonnegativity flags; magnitude lemmas such as this one keep those bridges coherent under the ring operations.
In the broader foundation stack this sits under the ledger and forcing layer that eventually feeds the T0–T8 chain. It does not itself force $\phi$ or dimension; it keeps the integer substrate of the recognition calculus consistent before those steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.