Foundation Primitive Recognition Calculus Integer Order Recip Num Not Balanced N

Reciprocal order law

In ordinary arithmetic, the reciprocal of a positive number is positive, and the reciprocal of a negative number is negative. The declaration recip_num_not_balanced_negate_ofOrbit_den_iff_nonnegFlag_of_not_balanced_zero is the framework's version of that fact, stated for its own discrete objects: a signed orbit, a discrete record of a number's sign and magnitude, and a ratio orbit, a pair of signed orbits standing for a fraction. The theorem says that when the numerator of a ratio orbit is not balanced with zero, meaning it is not zero, then the sign of the reciprocal's numerator is the same as the sign of the original numerator. In symbols, for a ratio orbit a, if the numerator is not zero, then the reciprocal's numerator has the same nonnegative flag as the original numerator.

The declaration is one of several closed order laws for the signed-orbit surface. It works by a direct computation: the reciprocal of a ratio orbit with numerator n and denominator d is the ratio orbit with numerator d and denominator n, and the sign flag is carried along unchanged. The theorem recipNonzero_num_nonnegFlag_eq states this equality, and the declaration in question is a corollary that applies it to the special case where the numerator is the negation of an orbit built from a natural number. The result is that the sign of the reciprocal is determined by the sign of the original numerator, exactly as in ordinary arithmetic.

The theorem does not claim anything about the magnitude of the reciprocal, nor does it say what happens when the numerator is zero. It also does not establish that the reciprocal operation is defined for all ratio orbits; it requires the numerator to be nonzero. The declaration is a small, precise statement about sign preservation under reciprocation, and it is part of a larger library of machine-checked theorems about the order structure of these discrete objects.

theorem recipNonzero_num_nonnegFlag_eq (a : RatioOrbit)
    (h : ¬ SignedOrbit.balanced a.num SignedOrbit.zero) :
    (RatioOrbit.recipNonzero a h).num.nonnegFlag = a.num.nonnegFlag := by
  by_cases hnonneg : a.num.nonnegFlag = true
  · rw [RatioOrbit.recipNonzero_num_eq_of_nonnegFlag (a := a) (h := h) hnonneg,
      SignedOrbit.nonnegFlag_ofOrbit, hnonneg]
  · have hnonnegFalse : a.num.nonnegFlag = false := by
      cases hflag : a.num.nonnegFlag with
      | false => rfl
      | true =>
          exfalso
          exact hnonneg hflag
    have hneg : a.num.negativeFlag = true := by
      rw [SignedOrbit.negativeFlag_eq_true_iff_nonnegFlag_eq_false]
      exact hnonnegFalse
    rw [RatioOrbit.recipNonzero_num_eq_of_negativeFlag (a := a) (h := h) hneg,
      SignedOrbit.nonnegFlag_negate_ofOrbit_of_ne_zero a.den a.den_ne_zero,
      hnonnegFalse]

What this page does not claim

The theorem does not state the magnitude of the reciprocal. The theorem does not define the reciprocal for a zero numerator. The theorem does not connect the sign-preservation law to any physical measurement.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: