abs_mul_eq_of_balanced
plain-language theorem explainer
If two pairs of signed orbits are balanced (same integer values), the absolute values of their products coincide as orbit positions. Order and arithmetic developers cite it to show that |·| on products is well-defined on the PRC integer quotient. The proof injects through the Nat display, rewrites abs and mul into Int, and substitutes the balanced-to-Int equalities.
Claim. Let $a,a',b,b'$ be signed orbits. If $a$ is balanced with $a'$ and $b$ is balanced with $b'$ (equivalently $a$ and $a'$ display the same integer, and likewise for $b,b'$), then $\lvert a\cdot b\rvert = \lvert a'\cdot b'\rvert$ as distinction-Nat orbit positions.
background
In the Primitive Recognition Calculus, integers are carried by signed orbits: each SignedOrbit has positive and negative distinction-Nat coordinates. Absolute value is the orbit position absDiff of those coordinates; multiplication is defined componentwise so that the verifier display satisfies (mul a b).toInt = a.toInt * b.toInt.
Balance is the internal equivalence of K4.9: a.pos + b.neg = b.pos + a.neg. The bridge lemma balanced_iff_toInt_eq states that this relation holds exactly when the two orbits display the same integer. The IntegerOrder module builds the order surface on these internal objects without leaving the δ-orbit language.
Upstream, abs_toNat identifies the internal absolute value with Int.natAbs of the display, and mul_toInt is the multiplicative homomorphism for the display map. Together they let absolute-value identities on products be checked on ordinary integers.
proof idea
Term-mode proof by display injection. Apply DistinctionNat.toNat_inj so it suffices that the Nat displays of the two absolute values agree. Rewrite both sides with abs_toNat and both products with mul_toInt, obtaining Int.natAbs (a.toInt * b.toInt) versus the primed pair. Convert the balance hypotheses via balanced_iff_toInt_eq into a.toInt = a'.toInt and b.toInt = b'.toInt, then substitute. Equality of the NatAbs products follows immediately.
why it matters
Absolute value of a product must be independent of balanced representatives before the signed-orbit order can be treated as an integer order. This lemma supplies that invariance for multiplication.
It is consumed by integer_order_certificate, whose doc-comment states that "the internal signed-orbit order surface is closed." That certificate packages display lemmas (truncated subtraction, leq, abs-diff, nonneg flags) that seal the order layer of PRC integers.
In the broader Recognition stack this sits under Foundation ledger forcing: balanced ledgers and signed-orbit arithmetic are the discrete substrate from which later forcing steps (J-cost uniqueness, φ, eight-tick structure) draw their integer bookkeeping. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.