abs_mul_eq_zero_of_balanced_zero_left
plain-language theorem explainer
If a signed orbit is balanced against zero, its product with any other signed orbit has absolute value zero. Order-surface and integer-arithmetic lemmas in the primitive recognition calculus cite this zero-absorption fact. The proof rewrites through the integer-display bridge and finishes by ring on integers.
Claim. Let $z,w$ be signed orbits. If $z$ is balanced with the zero orbit (equivalently, the integer display of $z$ is $0$), then the absolute value of the product $z\cdot w$ equals the zero distinction natural.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: pairs of distinction-natural positions (a positive leg and a negative leg). Absolute value is the absolute difference of those legs, valued in distinction naturals. Two signed orbits $a,b$ are balanced when $a.pos+b.neg=b.pos+a.neg$; the bridge lemma states this is exactly equality of their conservative integer displays.
Multiplication is defined so that the integer display of a product is the product of the displays. Absolute value vanishes if and only if the integer display is zero. The local module builds the internal order surface on these structures, keeping the integer bridge choice-free.
proof idea
Rewrite the goal with the absolute-value zero test and the product-display law, reducing to $z^{\mathrm{toInt}}\cdot w^{\mathrm{toInt}}=0$. Convert the balanced-with-zero hypothesis through the balanced-display bridge and the zero-display identity to obtain $z^{\mathrm{toInt}}=0$. Substitute that equality and close by ring.
why it matters
Used by the integer-order certificate, which asserts that the internal signed-orbit order surface is closed (display lemmas for truncated subtraction, comparison, absolute difference, and nonnegativity flags). Zero-absorption under multiplication is a basic algebraic sanity check on the PRC integer model: the zero class annihilates under product and remains zero in absolute value. It sits in the Foundation layer that underwrites later forcing-chain arithmetic; a coherent integer and order substrate is presupposed by the T5–T8 landmarks. The claim is fully proved, with no scaffold remaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.