mul_balanced_zero_of_balanced_zero_right_cf
plain-language theorem explainer
If a signed orbit w is balanced against the zero orbit, then any left product z·w is also balanced against zero. Used when closing the balanced-zero cone under multiplication in the primitive recognition calculus. Proof rewrites balance as equality of natural valuations, unfolds the product formulas, and substitutes the hypothesis.
Claim. Let $z$ and $w$ be signed orbits. If $w$ is balanced with respect to the zero signed orbit, then the product $z\cdot w$ is balanced with respect to the zero signed orbit.
background
In the primitive recognition calculus, signed orbits package a pair of distinction counts (positive and negative limbs) together with orbit data. Balance against the zero orbit means those limbs agree under the natural-number valuation toNat: the positive and negative sides contribute equally, matching the zero orbit.
Multiplication of signed orbits acts componentwise on the limbs (via mul_pos and mul_neg). The underlying arithmetic is the logic-derived natural numbers of ArithmeticFromLogic, recovered into ordinary Nat by the theorems toNat_add, toNat_mul, and toNat_zero. Those recovery maps are the bridge that lets balance statements reduce to ordinary natural equalities.
The local module sits in the Grow layer of PRC: it develops multiplicative closure properties of the balanced-zero class without choice principles on the right factor.
proof idea
Short tactic proof. First rewrite the balance hypothesis and the goal through SignedOrbit.balanced_iff_toNat_eq, so both become equalities of toNat values. Then simp only unfolds mul_pos, mul_neg, and zero, and applies the recovery lemmas toNat_add, toNat_mul, toNat_zero together with Nat.add_zero and Nat.zero_add. After simplification the goal is literally the rewritten hypothesis, discharged by rw [hw].
why it matters
Keeps the balanced-zero class of signed orbits closed under left multiplication. That closure is a structural prerequisite for treating balanced ledgers and orbits as a multiplicative monoid fragment inside Recognition Science foundations, before the forcing chain (T5 J-uniqueness through T8 dimension) is applied at higher layers.
No downstream consumers are wired yet (used_by is empty), so this is currently a leaf lemma in the Grow stack: it packages a right-factor, choice-free fact that later ratio-orbit and ledger-forcing arguments can import without re-proving the valuation arithmetic. It sits beside the ledger notion of balance (an event list is balanced) by giving the corresponding statement at the signed-orbit level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.