abs_mul_eq_of_balanced_right
plain-language theorem explainer
If two signed orbits are balanced (same internal integer), right-multiplication by a fixed signed orbit yields products with equal absolute value. Order and arithmetic lemmas on the PRC integer surface cite this to keep absolute value well-defined on equivalence classes. The proof reduces both sides to Int.natAbs of the product of verifier integers and substitutes equality of toInt.
Claim. For signed orbits $a,b,b'$, if $b$ and $b'$ are balanced (i.e. $b.\mathrm{pos}+b'.\mathrm{neg}=b'.\mathrm{pos}+b.\mathrm{neg}$, equivalently $b$ and $b'$ display the same integer), then $\lvert a\cdot b\rvert=\lvert a\cdot b'\rvert$ as orbit positions.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: pairs of distinction-orbit positions (pos, neg). Absolute value is the orbit position absDiff pos neg. Two signed orbits are balanced when a.pos + b.neg = b.pos + a.neg; that internal relation is exactly equality of the conservative verifier display toInt (K4.9).
Multiplication of signed orbits is defined so that toInt is a ring homomorphism: (mul a b).toInt = a.toInt * b.toInt. Absolute value on the verifier side is ordinary Int.natAbs, linked by abs_toNat: z.abs.toNat = Int.natAbs z.toInt.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign flags). The present lemma is a compatibility fact: absolute value of a product depends on the right factor only through its balanced class.
proof idea
Term-mode proof by injectivity of DistinctionNat.toNat. Rewrite both absolute values via abs_toNat and both products via mul_toInt, so the goal becomes equality of Int.natAbs (a.toInt * b.toInt) and Int.natAbs (a.toInt * b'.toInt). Convert the balanced hypothesis with balanced_iff_toInt_eq to b.toInt = b'.toInt, then substitute.
why it matters
Feeds integer_order_certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, leq, abs-diff, and nonnegativity flags). Without absolute-value invariance under balanced right factors, abs would not descend to the integer quotient and the certificate could not treat order as well-defined on PRC integers.
In the Recognition foundation this sits under ledger forcing and the primitive calculus that precedes the T0–T8 chain: integers must be recovered choice-free from δ-orbit data before J-cost, φ, and dimension forcing. It is a small but necessary algebraic hygiene step on that path, not a physics claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.