toInt_mul
plain-language theorem explainer
Multiplication on PRC integers commutes with the integer display map: the product of two quotient classes maps to the ordinary product in ℤ. Anyone assembling the ring laws for recognition-derived integers cites this as the multiplicative half of the display homomorphism. The proof is double quotient induction that reduces immediately to the signed-orbit identity mul_toInt.
Claim. For PRC integers $a,b$ (quotient classes of signed orbits under the balanced-length relation), the integer display of their product equals the product of their displays: $\mathrm{toInt}(a\cdot b)=\mathrm{toInt}(a)\cdot\mathrm{toInt}(b)$ in $\mathbb{Z}$.
background
PRC integers are the quotient type PRCInt := Quot signedOrbitSetoid. A signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg; the setoid identifies pairs that differ by a balanced length (the internal equivalence that makes the difference well-defined). The display map toInt : PRCInt → ℤ sends a class to the integer value of any representative.
Multiplication is defined first on signed orbits by the usual difference-of-products rule (positive part pos₁pos₂ + neg₁neg₂, negative part pos₁neg₂ + neg₁pos₂), then descended to the quotient. The sibling lemma SignedOrbit.mul_toInt already records that this representative-level product matches ordinary multiplication in ℤ.
The local setting is K4.8 of the primitive recognition calculus: integers built from signed orbit differences before the continuum bridge, with the verifier display into ℤ treated as a downstream theorem rather than a definitional equality.
proof idea
Term-mode proof by double Quot.induction_on on a and b. After induction both sides are evaluated on signed-orbit representatives, and the goal reduces exactly to SignedOrbit.mul_toInt a b, which expands the product formula
((pos_a pos_b + neg_a neg_b) - (pos_a neg_b + neg_a pos_b))
and matches it against (pos_a - neg_a)(pos_b - neg_b) in ℤ. No further algebraic work is needed at the quotient level; the setoid respects the operation by construction of the descended mul.
why it matters
This is the multiplicative half of the display homomorphism from PRC integers into ℤ. Downstream, the IntegersFromLogic layer uses the corresponding toInt_mul identity to discharge the ring axioms by transport: mul_assoc', mul_comm', mul_one', one_mul', mul_add', add_mul', mul_right_cancel, and the no-zero-divisors statement mul_eq_zero all rewrite through eq_iff_toInt_eq and this (or the parallel LogicInt) identity, then finish by ring in ℤ.
In the Recognition foundation stack this sits inside K4.8 (integers as signed-orbit quotient classes). It does not itself invoke the forcing chain T0–T8 or the J-cost, but it is part of the arithmetic substrate those later layers assume when they treat integers as already available from pure recognition structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.