num_mul_recipNonzero_num_balanced_ofOrbit_den_mul_abs
plain-language theorem explainer
For a nonzero ratio orbit a, the product of a.num with the numerator of its nonzero reciprocal is balanced against the unsigned orbit of den·|num|. Anyone proving that a·(1/a) equals one via cross-equality cites this identity. The proof splits on the numerator sign flag, rewrites the reciprocal numerator, and finishes by integer arithmetic after transporting through toInt.
Claim. Let $a$ be a ratio orbit whose numerator is not balanced with zero. Then the signed-orbit product of $a$'s numerator with the numerator of the nonzero reciprocal of $a$ is balanced with the orbit embedding of (denominator of $a$) times (absolute value of the numerator of $a$).
background
Ratio orbits package a signed numerator and an unsigned denominator as the primitive rational objects of the recognition calculus. Signed orbits carry a nonnegativity flag; balanced means the two sides have equal integer images under toInt. The absolute-value map on a signed orbit recovers the nonnegative magnitude, with abs_toInt_of_nonnegFlag and abs_toInt_of_negativeFlag relating that magnitude back to toInt.
The nonzero reciprocal recipNonzero is defined only when the numerator is unbalanced with zero. Its numerator is the orbit of the denominator when the original numerator is nonnegative, and the negation of that orbit when the numerator is negative (recipNonzero_num_eq_of_nonnegFlag / recipNonzero_num_eq_of_negativeFlag). Sign flags are exclusive: negative flag holds exactly when the nonneg flag is false.
Local setting is the integer-order layer of Primitive Recognition Calculus, which builds ordered arithmetic on signed orbits before certifying the full order surface. Multiplication of underlying distinction naturals recovers ordinary Nat multiplication via toNat_mul.
proof idea
Case-split on whether the numerator nonneg flag is true.
Nonneg branch: apply abs_toInt_of_nonnegFlag and rewrite the reciprocal numerator by recipNonzero_num_eq_of_nonnegFlag. Transport balance to integer equality (balanced_iff_toInt_eq), expand multiplication and orbit embeddings through mul_toInt / ofOrbit_toInt, replace distinction-nat multiplication by toNat_mul, insert the absolute-value identity, and close by ring.
Neg branch: first force the nonneg flag false, then obtain the negative flag via negativeFlag_eq_true_iff_nonnegFlag_eq_false. Apply abs_toInt_of_negativeFlag and rewrite the reciprocal numerator by recipNonzero_num_eq_of_negativeFlag (which inserts a negation). Same transport through toInt, now also using negate_toInt, then ring again.
why it matters
This is the numerator half of the identity needed to show a ratio orbit times its reciprocal is cross-equal to one. Immediate consumer is mul_recipNonzero_crossEq_one, which assembles the full inverse law; the symmetric product order is handled by recipNonzero_num_mul_num_balanced_ofOrbit_den_mul_abs, and a companion lemma extends the same balance to the total reciprocal. Those inverse facts feed the closed integer-order certificate (integer_order_certificate), whose doc-comment states that the internal signed-orbit order surface is closed.
In the Recognition forcing chain the certificate sits under the arithmetic substrate that later supports the eight-tick octave (T7) and dimension forcing (T8). No open scaffold remains here: the claim is fully proved and only packages sign-case bookkeeping already established upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.