signedQuotient_abs_toNat
plain-language theorem explainer
The natural number read from the absolute value of a signed orbit quotient equals the ordinary Nat division of the absolute values. Anyone cancelling a common divisor when normalizing orbit ratios cites this bridge. The proof cases on the sign flag and reduces both branches to the unsigned quotient-to-Nat identity.
Claim. For every signed orbit $z$ and every nonzero distinction $d$, if $q$ is the signed quotient of $z$ by $d$, then the natural number underlying $|q|$ equals $|z|_{\mathrm{nat}}\,/\,d_{\mathrm{nat}}$.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: a pair of distinction positions with a computable nonnegative flag. Absolute value of a signed orbit is the distinction obtained by absolute difference of the two sides; toNat reads that distinction as an ordinary natural number (the iteration count of the underlying logic-nat).
Division is first defined on unsigned distinctions (the Euclidean quotient of two orbit positions, with nonzero divisor). The signed quotient lifts that construction: when the flag is nonnegative it wraps the unsigned quotient as a positive signed orbit; when negative it wraps the negation. The present lemma is the display identity that this signed construction, after taking absolute value and reading to Nat, agrees with ordinary Nat division of the absolute values.
Upstream, abs_toNat identifies internal absolute value with Int.natAbs of the integer view, ofOrbit_toInt and negate_toInt control the integer reading of the two wrappers, and quotient_toNat is the corresponding identity for the unsigned quotient.
proof idea
Unfold the signed quotient definition and case on whether the nonnegative flag of $z$ is true.
In the true branch, the signed quotient is ofOrbit of the unsigned quotient of $|z|$ by $d$. A short simp using abs_toNat and ofOrbit_toInt shows that the absolute value of that wrapper, read to Nat, equals the unsigned quotient's toNat. Finish by simpa with the unsigned lemma quotient_toNat.
In the false branch, first force the flag to be literally false (the only other Bool value). The signed quotient is then the negation of the same ofOrbit wrapper. Simp with abs_toNat, ofOrbit_toInt, and negate_toInt again collapses the absolute value to the unsigned quotient's Nat, and quotient_toNat finishes.
why it matters
This is the absolute-value bridge needed to move coprimality statements from signed orbit arithmetic down to ordinary Nat gcd. The sole direct consumer is normalizeRatio_coprime, which proves that after cancelling gcd(|num|, den) from a ratio of orbits, the resulting numerator absolute value and denominator are coprime: it rewrites through this lemma and quotient_toNat, then appeals to the Nat-level gcd identity.
In the broader Recognition foundation, orbit-level Euclidean division is how rational structure is recovered from pure distinction arithmetic before the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3) is applied. Without a clean abs-to-Nat quotient identity, normalization of ratios would stay stuck in the signed layer and could not inherit Nat coprimality. The lemma is fully proved scaffolding for that handoff; it does not itself touch physical constants or the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.