Foundation Primitive Recognition Calculus Rational Field Div Mul Cancel

The cancellation law

In ordinary arithmetic, the fraction a/b times b equals a, provided b is not zero. The declaration div_mul_cancel proves that this same cancellation law holds inside the Recognition Science framework's number system, known as PRC rationals. The proof is machine-checked in the framework's library of formal theorems. It states that for any PRC rationals a and b, if b's value is not zero, then (a / b) * b = a. Division here is defined in the standard way: a divided by b means a multiplied by the reciprocal of b.

What makes this worth stating is what the number system is built from. PRC rationals are not defined by choosing axioms for arithmetic; they are constructed from ratio orbits, which are discrete records of recognition events. A ratio orbit pairs a signed numerator with a nonzero denominator, and the denominator being nonzero means it is positive in the verifier display. The framework then lifts ordinary field laws, including associativity, distributivity, and the cancellation law, onto this constructed system. The div_mul_cancel theorem is one of those lifted laws, verified by translating the statement to ordinary rational numbers and applying standard field simplification.

The theorem also connects to positivity. A PRC rational is positive exactly when its value is greater than zero, and a positive rational is never zero. The cancellation law uses the weaker condition that the denominator's value is nonzero, not that it is positive. So the law applies to negative denominators as well, as long as they are not zero. This keeps the field structure complete: every nonzero element has a reciprocal, and division by any nonzero element behaves as expected.

In Recognition Science, this law is part of a bundled certificate that the constructed rationals form a field. The certificate packages the field laws into a single structure, and div_mul_cancel is one of its components. The practical consequence is that the framework's rational numbers support the same algebraic manipulations as the rationals of classical mathematics, despite being built from a very different starting point. A reader can divide and cancel without worrying that the unusual construction has broken ordinary arithmetic.

theorem div_mul_cancel {a b : PRCRat} (h : b.toRat ≠ 0) :
    (a / b) * b = a := by
  apply toRat_injective
  rw [toRat_mul', toRat_div]
  field_simp [h]

/-- Division on PRC rationals, defined from PRC multiplication and reciprocal. -/
def div (a b : PRCRat) : PRCRat :=
  a * b⁻¹

theorem positive_iff_toRat_pos (q : RatioOrbit) :
    positive q ↔ 0 < q.toRat := by
  unfold positive RatioOrbit.toRat
  have hdenNat : 0 < q.den.toNat := Nat.pos_of_ne_zero q.den_toNat_ne_zero
  have hdenQ : 0 < (q.den.toNat : ℚ) := by exact_mod_cast hdenNat
  constructor
  · intro h
    have hnum_nonneg : 0 ≤ q.num.toInt :=
      (SignedOrbit.nonneg_iff_toInt_nonneg q.num).mp h.1
    have hnum_ne : q.num.toInt ≠ 0 := by
      intro hz
      exact h.2 ((SignedOrbit.balanced_iff_toInt_eq q.num SignedOrbit.zero).mpr (by
        rw [hz, SignedOrbit.zero_toInt]))
    have hnum_pos : 0 < q.num.toInt := by omega
    have hnumQ : 0 < (q.num.toInt : ℚ) := by exact_mod_cast hnum_pos
    positivity
  · intro h
    have hnum_pos : 0 < q.num.toInt := by
      have hden_ne : (q.den.toNat : ℚ) ≠ 0 := q.den_cast_ne_zero
      have hmul : 0 < ((q.num.toInt : ℚ) / (q.den.toNat : ℚ)) * (q.den.toNat : ℚ) :=
        mul_pos h hdenQ
      have hnumQ : 0 < (q.num.toInt : ℚ) := by
        field_simp [hden_ne] at hmul
        exact hmul
      exact_mod_cast hnumQ
    constructor
    · exact (SignedOrbit.nonneg_iff_toInt_nonneg q.num).mpr (by omega)
    · intro hbal
      have hnum_zero : q.num.toInt = 0 := by
        have := (SignedOrbit.balanced_iff_toInt_eq q.num SignedOrbit.zero).mp hbal
        simpa using this
      omega

structure RationalFieldCertificate : Prop where
  add_comm : ∀ a b : PRCRat, a + b = b + a
  add_assoc : ∀ a b c : PRCRat, (a + b) + c = a + (b + c)
  zero_add : ∀ a : PRCRat, 0 + a = a
  add_zero : ∀ a : PRCRat, a + 0 = a
  add_left_neg : ∀ a : PRCRat, -a + a = 0
  mul_comm : ∀ a b : PRCRat, a * b = b * a
  mul_assoc : ∀ a b c : PRCRat, (a * b) * c = a * (b * c)
  one_mul : ∀ a : PRCRat, 1 * a = a
  mul_one : ∀ a : PRCRat, a * 1 = a
  left_distrib : ∀ a b c : PRCRat, a * (b + c) = a * b + a * c
  right_distrib : ∀ a b c : PRCRat, (a + b) * c = a * c + b * c
  zero_ne_one : (0 : PRCRat) ≠ 1
  inv_zero : (0 : PRCRat)⁻¹ = 0
  mul_inv_cancel : ∀ a : PRCRat, a.toRat ≠ 0 → a * a⁻¹ = 1
  inv_mul_cancel : ∀ a : PRCRat, a.toRat ≠ 0 → a⁻¹ * a = 1
  div_display : ∀ a b : PRCRat, (a / b).toRat = a.toRat / b.toRat
  positive_display : ∀ q : PRCRat, PRCRat.positive q ↔ 0 < q.toRat
  ratio_positive_display : ∀ q : RatioOrbit, RatioOrbit.positive q ↔ 0 < q.toRat
  jcost_display :
    ∀ q : PRCRat, (PRCJCost.onPRCRat q).toRat = (q.toRat + q.toRat⁻¹) / 2 - 1
  jcost_normalized_representative :
    ∀ q : RatioOrbit,
      PRCJCost.onPRCRat (PRCRat.mk q) =
        PRCJCost.onPRCRat (PRCRat.mk (DistinctionNat.normalizeRatio q))

What this page does not claim

The theorem does not claim that division by zero is defined or meaningful in the framework. It does not claim that the recognition calculus itself, including the J-cost function, is a field under these operations. It does not claim that the positivity condition is required for cancellation; only nonzero is needed.

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/RationalField.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: