orbit_mul_not_unit_of_left_not_unit
plain-language theorem explainer
If a finite distinction orbit is not the multiplicative unit, no right product of it is a unit either. Orbit-arithmetic and native-cost uniqueness arguments cite this to keep non-unit factors closed under multiplication. The proof reduces units to toNat = 1 and uses that a Nat product equals 1 only if both factors are 1.
Claim. Let $p,r$ be finite distinction orbits (base-neutral $\delta$-orbits). If $p$ is not the multiplicative unit (equivalently, not the one-step orbit), then the product orbit $p\cdot r$ is not a unit either.
background
In Primitive Recognition Calculus, DistinctionNat is the inductive finite orbit of repeated distinction: zero and successor steps, the base-neutral carrier for orbit arithmetic (K2.12). Its verifier display toNat reads the orbit as an ordinary natural number.
Multiplication on orbits is defined so that the display is a ring homomorphism: $(a\cdot b).\mathrm{toNat}=a.\mathrm{toNat}\cdot b.\mathrm{toNat}$ (K4.7). The native unit predicate is equality to the one-step orbit; equivalently, by the divisibility layer, an orbit is a unit iff its toNat is $1$. Only that one-step orbit is multiplicatively invertible in the finite $\delta$-orbit.
The ambient module develops uniqueness of the native cost functional on ratio characters. Non-unit orbit factors appear in orientation and factorization constraints that feed the uniqueness blocker certificate.
proof idea
Tactic proof by contradiction. Assume the product is a unit; the unit-iff-toNat lemma gives $(p\cdot r).\mathrm{toNat}=1$. From the hypothesis that $p$ is not a unit, the same equivalence yields $p.\mathrm{toNat}\neq 1$. Rewrite the product identity with the orbit multiplication display theorem, so $p.\mathrm{toNat}\cdot r.\mathrm{toNat}=1$. Nat.eq_one_of_mul_eq_one_right forces $p.\mathrm{toNat}=1$, contradicting the non-unit hypothesis on $p$.
why it matters
Closes a basic multiplicative permanence fact for non-units in the distinction orbit monoid: non-units cannot become units by right multiplication. Downstream, PRCCharacterNoMixedNonunitOrbitOrientation_of_product_no_mixed applies it when lifting product-level no-mixed-orientation hypotheses to non-unit orbit orientation constraints on ratio characters.
That orientation hygiene feeds refutations such as PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_refuted and is packaged into prc_native_cost_uniqueness_blocker_certificate, which records which native-cost uniqueness targets are proved versus refuted. In the broader Recognition stack this sits under the Primitive Recognition Calculus path toward J-cost uniqueness (forcing chain T5 and the Recognition Composition Law), keeping factorization and orientation side-conditions algebraically consistent before cost calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.