Foundation Primitive Recognition Calculus Integer Order Num Mul Recip Num Balanc

Reciprocal balance

The declaration num_mul_recip_num_balanced_ofOrbit_den_mul_abs_of_not_balanced_zero is a formal statement inside the Recognition Science framework. It concerns RatioOrbit, a structure that represents a ratio of two SignedOrbit values, which are themselves integers with a sign flag. The theorem says that when you take a ratio, swap its numerator and denominator (the reciprocal), and then multiply the numerator of the result by the original numerator, you get a value that is balanced with the product of the original denominator and the absolute value of the original numerator, provided the original numerator is not balanced with zero.

In plainer terms, this is a statement about how the framework handles the reciprocal of a non-zero number. It shows that the reciprocal operation, when combined with multiplication, preserves a certain kind of equality, called balanced, which is the framework's way of saying two values are the same in its ledger. The condition that the numerator is not balanced with zero is essential: it ensures the reciprocal is well-defined, since dividing by zero is not allowed. The theorem then guarantees that the sign of the original numerator is carried through the reciprocal operation correctly, and that the magnitude is swapped between numerator and denominator.

What this declaration does not claim is that it defines the reciprocal operation or that it proves the reciprocal of any number exists. The reciprocal is a separate definition, and this theorem only describes a property of it under a specific condition. It also does not claim that the reciprocal of a number balanced with zero is defined, or that the reciprocal operation is its own inverse in general. The theorem is a precise, conditional statement about the interaction of reciprocal, multiplication, and the balance relation, not a general law of arithmetic.

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

What this page does not claim

The reciprocal operation is defined by this theorem. The reciprocal of a number balanced with zero is defined. The reciprocal operation is its own inverse in general.

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: