orbitDirection_mul_crossEq
plain-language theorem explainer
If three nonzero distinction naturals satisfy a·b = p, the directed ratio orbit of p is cross-equivalent to the product of the directed orbits of a and b. Anyone building multiplicative characters on ratio orbits, or proving native-cost uniqueness via orbit-product display compatibility, cites this. The proof reduces cross-equivalence to rational equality and transports the multiplication law through toNat.
Claim. Let $a,b,p$ be nonzero distinction naturals with $a\cdot b=p$. Then the directed ratio orbit of $p$ is cross-equivalent to the ratio-orbit product of the directed orbits of $a$ and of $b$: $\mathrm{crossEq}(\mathrm{dir}(p),\,\mathrm{dir}(a)\cdot\mathrm{dir}(b))$.
background
In the primitive recognition calculus, distinction naturals are the discrete counting type built from the logic-arithmetic layer. Nonzero elements carry a directed ratio orbit: a representative of the positive rational class associated to that count. Ratio-orbit multiplication is the group law on those classes; cross-equivalence identifies two orbits when they display the same rational (same toRat value).
The arithmetic recovery map toNat reads iteration count from the logic-natural encoding and is a monoid homomorphism: toNat(a·b)=toNat(a)·toNat(b). That recovery is the bridge from distinction multiplication to ordinary Nat multiplication, and thence to rationals on orbits.
This module develops native-cost uniqueness for PRC characters. Characters act on ratio orbits; for a character to respect native display of products, the orbit of a product must match the product of orbits up to cross-equivalence. The present lemma is exactly that matching statement for directed orbits.
proof idea
Term-mode rewrite chain. Unfold cross-equivalence via the iff that equates it to equality of rational displays. Rewrite both sides with the lemmas that send directed orbits and orbit products to their toRat values, so the goal becomes an equality of rationals built from the three counts.
Apply congrArg of DistinctionNat.toNat to the hypothesis a·b=p, then rewrite with the recovery theorem toNat_mul so the natural numbers multiply. Finish by exact_mod_cast on the symmetric equality, casting the Nat identity into the rational display equality.
why it matters
Native-cost uniqueness needs characters that respect orbit products in display, not merely abstract cross-equivalence. Downstream, PRCCharacterOrbitProductDisplayCompatible_of_crossEq_respect applies this lemma pointwise: any character that respects cross-equivalence automatically respects product display on directed orbits. That compatibility feeds the identity-identity and reciprocal-reciprocal product laws for PRC ratio characters, and sits on the path into the native-cost uniqueness blocker certificate and the refutation that prime calibration forces nonunit local orientation.
In the broader forcing picture this is bookkeeping on the discrete multiplicative skeleton that later supports J-cost uniqueness (T5) and the recognition composition law: characters and costs must see products the same way the underlying counts multiply. Without directed-orbit product matching, the quotient-respect step called out in the module (character value on the product orbit versus on the ratio product of factors) cannot even be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.