rat_mul_num_den_cross
plain-language theorem explainer
For any rationals t₁ and t₂, the product of the reduced numerator of t₁t₂ with the product of the two denominators equals the product of the two numerators with the reduced denominator of t₁t₂. Anyone proving multiplicative identities for integer-valued functions of reduced fractions (here the Liouville sign) cites this cross-cancellation identity. The proof lifts Rat.num_div_den to ℚ, cancels by ring, and casts back to ℤ.
Claim. For all rationals $t_1,t_2\in\mathbb{Q}$, if $n(\cdot)$ and $d(\cdot)$ denote the reduced numerator and positive denominator, then $n(t_1 t_2)\, d(t_1)\, d(t_2) = n(t_1)\, n(t_2)\, d(t_1 t_2)$ as an equality in $\mathbb{Z}$.
background
Every rational $t$ is stored in reduced form $t = n(t)/d(t)$ with $d(t)>0$ and $\gcd(|n(t)|,d(t))=1$. The defining relation is $n(t) = t\cdot d(t)$ in $\mathbb{Q}$, which is Rat.num_div_den after clearing the nonzero denominator.
When two rationals are multiplied, the raw products $n(t_1)n(t_2)$ and $d(t_1)d(t_2)$ share a common positive integer factor that is cancelled to reach the reduced form of $t_1 t_2$. The cross identity records exactly that the cancelled factor is the same on both sides, so the two integer products remain equal.
The ambient module builds a certificate that the native recognition cost is minimal. A signed Liouville-type character on nonzero rationals is defined from the parity of prime factors in the reduced numerator and denominator; multiplicativity of that character needs this integer identity first.
proof idea
Three applications of Rat.num_div_den give, after div_eq_iff and den_ne_zero, the equalities $n(t_1 t_2)=t_1 t_2, d(t_1 t_2)$, $n(t_1)=t_1, d(t_1)$, and $n(t_2)=t_2, d(t_2)$ in $\mathbb{Q}$. Substitute all three into the desired cross product; ring rearranges the rational expression to an identity. Finish by exact_mod_cast to recover the integer statement.
why it matters
The sole downstream consumer is liouvilleSign_mul, which asserts complete multiplicativity of the Liouville sign on nonzero rationals: cancellation removes the same factors from numerator and denominator, so total parity is preserved. That multiplicativity is part of the PRC native-cost minimality certificate, which sits in the foundation layer that feeds the forcing chain (T5 J-uniqueness through the Recognition Composition Law). Without the cross identity, the sign of a product could not be reduced to the product of signs after reduction, and the certificate would stall at a bookkeeping gap rather than a structural claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.