Foundation Primitive Recognition Calculus Orbit Euclidean Quotient Mul Divisor A

The division identity

In ordinary arithmetic, division with remainder obeys a simple rule: if you divide a number by a divisor, then multiply the quotient by the divisor and add the remainder, you get the original number back. For example, 17 divided by 5 gives quotient 3 and remainder 2, and 3 times 5 plus 2 equals 17. This identity, known as the division algorithm, is one of the first facts taught about numbers.

The Recognition Science framework builds its own arithmetic on a discrete record of events, called a ledger (a finite sequence of recognition events). Within this ledger arithmetic, the framework's machine-checked library of formal theorems proves the same division identity holds. The theorem, named quotient_mul_divisor_add_remainder_eq, states that for any two ledger numbers n and d, where d is not zero, multiplying the quotient of n by d with d and adding the remainder yields exactly n.

The proof works by showing that the ledger arithmetic matches ordinary natural number arithmetic. The framework defines quotient and remainder by repeated subtraction, a fuel-based process that subtracts the divisor from the dividend until the dividend is smaller than the divisor. The theorem then verifies that this process produces the same result as the standard division and modulo operations on natural numbers, and the familiar identity follows.

In Recognition Science, this identity is a building block. It underpins the framework's ratio normalization, the process of reducing a ratio of ledger numbers to lowest terms, similar to simplifying a fraction. The theorem guarantees that dividing by the greatest common divisor and multiplying back recovers the original numbers, which is essential for the framework's treatment of ratios and orbits.

What the theorem does not claim is broader significance. It does not assert that the division identity is unique to Recognition Science, nor does it say anything about the physical or philosophical meaning of the ledger. It is a formal result about a specific arithmetic structure, proved within the framework's library, and its value lies in the foundation it provides for further derivations.

/-- The quotient and remainder reconstruct the dividend in orbit arithmetic. -/
theorem quotient_mul_divisor_add_remainder_eq
    (n d : DistinctionNat) (hd : d ≠ zero) :
    quotient n d hd * d + remainder n d hd = n := by
  apply toNat_inj
  rw [toNat_add, toNat_mul, quotient_toNat, remainder_toNat]
  rw [Nat.mul_comm (n.toNat / d.toNat) d.toNat]
  exact Nat.div_add_mod n.toNat d.toNat

/-- The quotient and remainder reconstruct the dividend in orbit arithmetic. -/
theorem quotient_mul_divisor_add_remainder_eq
    (n d : DistinctionNat) (hd : d ≠ zero) :
    quotient n d hd * d + remainder n d hd = n := by
  apply toNat_inj
  rw [toNat_add, toNat_mul, quotient_toNat, remainder_toNat]
  rw [Nat.mul_comm (n.toNat / d.toNat) d.toNat]
  exact Nat.div_add_mod n.toNat d.toNat

/-- The quotient and remainder reconstruct the dividend in orbit arithmetic. -/
theorem quotient_mul_divisor_add_remainder_eq
    (n d : DistinctionNat) (hd : d ≠ zero) :
    quotient n d hd * d + remainder n d hd = n := by
  apply toNat_inj
  rw [toNat_add, toNat_mul, quotient_toNat, remainder_toNat]
  rw [Nat.mul_comm (n.toNat / d.toNat) d.toNat]
  exact Nat.div_add_mod n.toNat d.toNat

/-- Fuelled quotient/remainder by repeated subtraction. The first argument is
an orbit fuel, not verifier `Nat`. -/
def divModFuel : DistinctionNat → DistinctionNat → DistinctionNat → DistinctionNat × DistinctionNat
  | zero, n, _ => (zero, n)
  | succ fuel, n, d =>
      if DistinctionNat.leq d n then
        let qr := divModFuel fuel (DistinctionNat.truncatedSub n d) d
        (succ qr.1, qr.2)
      else
        (zero, n)

What this page does not claim

The division identity is not claimed to be unique to Recognition Science; it is a standard arithmetic fact. The theorem does not assert any physical or philosophical significance for the ledger beyond its formal role. The framework's quotient and remainder are not claimed to be more efficient than standard division algorithms.

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