signedQuotient_mul_divisor_toInt_of_divides
plain-language theorem explainer
If a nonzero distinction $d$ exactly divides the absolute value of a signed orbit $z$, then the integer value of the signed quotient of $z$ by $d$, times $d$, recovers $z$ as an integer. Ratio-normalization cites this when canceling a GCD from a signed numerator. The proof lifts the unsigned exact-division identity and cases on the nonnegativity flag.
Claim. Let $z$ be a signed orbit and $d$ a nonzero natural distinction that divides $|z|$. Write $q$ for the signed quotient of $z$ by $d$. Then $q^{\mathrm{to}\,\mathbb{Z}}\cdot d = z^{\mathrm{to}\,\mathbb{Z}}$ in $\mathbb{Z}$.
background
This lives in the orbit Euclidean layer of Primitive Recognition Calculus: division, remainder, and GCD are defined on distinction orbits (native naturals built by iterated recognition steps), then lifted to signed orbits and ratios.
A signed orbit packages two distinction positions with a nonnegativity flag; its recovery map toInt reads the difference of the two iteration counts as an ordinary integer. Absolute value is the orbit absolute difference of those positions, and the verifier identity abs_toNat says that absolute value recovers Int.natAbs of the recovered integer. Negation flips the recovered sign.
The unsigned sibling already proves that when $d$ divides $n$, the native quotient satisfies $q\cdot d = n$ on naturals. The present statement is the signed exact-division counterpart needed before ratios can cancel a GCD while preserving orientation.
proof idea
First apply the unsigned exact-division lemma quotient_mul_divisor_toNat_of_divides to $|z|$ and $d$, then cast the natural identity to $\mathbb{Z}$.
Unfold the signed quotient. Case on the nonnegativity flag of $z$.
- If nonnegative:
nonnegFlag_eq_true_iffgives $z^{\mathrm{to},\mathbb{Z}}\ge 0$, soabs_toNatplusInt.ofNat_natAbs_of_nonnegidentifies $|z|$ with $z$ in $\mathbb{Z}$; simplify and rewrite. - If negative: force the flag false, obtain $z^{\mathrm{to},\mathbb{Z}}<0$, identify $|z|$ with $-z$ via
ofNat_natAbs_of_nonpos, then simplify withofOrbit_toIntandnegate_toIntand finish byring.
why it matters
Exact signed cancellation is the bridge from orbit GCD to reduced ratios. The sole direct consumer is normalizeRatio_num_mul_gcd_toInt, which states that after dividing a ratio's numerator magnitude and denominator by their native GCD, the signed numerator times that GCD recovers the original numerator integer. That identity is how ratio normalization restores orientation via the nonnegativity flag while canceling common factors.
In the broader foundation stack this is bookkeeping, not a forcing-chain landmark: it equips the recognition-native integers and rationals so later arithmetic (mass ladder bookkeeping, dimensionless ratios) can run on reduced fractions without leaving the orbit calculus. It does not itself force $\varphi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.