mul_one
plain-language theorem explainer
Right-multiplication by the multiplicative unit leaves every PRC integer fixed: a·1 = a on the signed-orbit quotient. Anyone assembling the monoid or ring structure on these integers, or simplifying cost-algebra and Φ-ring calculations that land in ℤ, cites this unit law. The proof pushes equality through the injective toInt display and closes by simplification against the underlying LogicNat unit law.
Claim. For every PRC integer $a$ (a balanced-length quotient class of signed orbits), right-multiplication by the unit satisfies $a \cdot 1 = a$.
background
PRC integers are the quotient of signed orbits by the internal balanced-length relation (K4.8). The type is Quot signedOrbitSetoid; the map into ordinary integers is a downstream display theorem, not part of the definition. Multiplication on signed orbits is defined componentwise on positive and negative legs so that it agrees with integer multiplication under that display (mul_toInt).
The unit is the class whose display is $1$. Upstream, LogicNat already carries a right-unit law n * succ zero = n, recovered into ordinary Nat by toNat_mul. Cross-equality of ratio orbits is characterized choice-free by integer cross-products (crossEq_iff_toIntCross), and equal cross-products yield equal quotient classes (mk_eq_mk_of_crossEq). Those facts underwrite well-defined arithmetic on the quotient; the present lemma is the integer-level right unit.
proof idea
One short tactic proof. Apply injectivity of the integer display toInt to reduce mul a one = a to an equality in ℤ. Then simp unfolds multiplication and the unit on the quotient, rewrites via mul_toInt, one_num_toInt, and one_den_toNat, and discharges the resulting integer identity using the LogicNat right-unit law and its recovery under toNat. No manual case split is required.
why it matters
This is a basic monoid axiom for PRC integers. Downstream it is used heavily in CostAlgebra (exact J level-set classification J_eq_iff_eq_or_inv, shifted composition values, window-sum equivariance), in the Φ-ring structure PhiInt (pairs $a+b\varphi$ with integer coefficients), and in constants and chemistry lemmas that simplify products against 1 (e.g. Einstein kappa identity, alpha-genesis resummation, LJ minimum bounds).
In the Recognition framework it sits under the foundation layer that rebuilds arithmetic from recognition orbits before the forcing chain (T5 J-uniqueness, T6 φ fixed point) and cost algebra are stated. Without the unit laws, the monoid instances that feed J-composition and φ-ladder arithmetic do not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.