Foundation Primitive Recognition Calculus Orbit Euclidean Signed Quotient Mul Di

The exactness of division

In ordinary arithmetic, division is exact when the divisor goes into the dividend a whole number of times with nothing left over. For example, 12 divided by 3 is exactly 4, and multiplying back, 4 times 3, returns 12. The theorem signedQuotient_mul_divisor_toInt_of_divides states that this same property holds inside the Recognition Science framework's arithmetic of orbits, its discrete records of counted events. The framework's machine-checked library of formal theorems proves that if a divisor divides the absolute value of a signed orbit, then the signed quotient times the divisor equals the original signed orbit.

The statement is precise about its terms. A signed orbit is an orbit with a sign flag, so it can represent negative as well as positive counts. The theorem requires the divisor to be nonzero, and it requires the divisor to divide the absolute value of the signed orbit, meaning the division leaves no remainder. Under those conditions, the equality holds in the integers: the signed quotient multiplied by the divisor equals the original signed orbit. This is the signed analogue of a simpler theorem in the same library, which proves the same property for unsigned orbits.

The theorem is a building block, not a standalone discovery. It is used to prove that normalizing a ratio, reducing it to lowest terms, preserves the ratio's value. The library shows that after dividing both numerator and denominator by their greatest common divisor, the new numerator times the gcd recovers the original numerator, and similarly for the denominator. This is the framework's version of reducing a fraction like 6/8 to 3/4.

What the theorem does not claim is as important as what it proves. It does not say that every division is exact; it only applies when the divisor divides the dividend. It does not define what division means, it proves a property of a division that the framework has already defined by repeated subtraction. It does not connect this arithmetic to the framework's physical claims about recognition costs or the golden ratio. It is a piece of internal bookkeeping, a guarantee that the framework's arithmetic behaves the way ordinary arithmetic does.

theorem signedQuotient_mul_divisor_toInt_of_divides
    (z : SignedOrbit) (d : DistinctionNat) (hd : d ≠ zero)
    (hdiv : divides d z.abs) :
    (signedQuotient z d hd).toInt * (d.toNat : ℤ) = z.toInt := by
  have hquotNat :
      (quotient z.abs d hd).toNat * d.toNat = z.abs.toNat :=
    quotient_mul_divisor_toNat_of_divides (n := z.abs) (d := d) hd hdiv
  have hquotInt :
      ((quotient z.abs d hd).toNat : ℤ) * (d.toNat : ℤ) =
        (z.abs.toNat : ℤ) := by
    exact_mod_cast hquotNat
  unfold signedQuotient
  by_cases hflag : z.nonnegFlag = true
  · have hnonneg : 0 ≤ z.toInt :=
      (SignedOrbit.nonnegFlag_eq_true_iff z).mp hflag
    have habs : (z.abs.toNat : ℤ) = z.toInt := by
      rw [SignedOrbit.abs_toNat]
      exact Int.ofNat_natAbs_of_nonneg hnonneg
    simp [hflag, SignedOrbit.ofOrbit_toInt]
    rw [hquotInt, habs]
  · have hflagFalse : z.nonnegFlag = false := by
      cases h : z.nonnegFlag with
      | false => rfl
      | true =>
          exfalso
          exact hflag h
    have hneg : z.toInt < 0 :=
      (SignedOrbit.nonnegFlag_eq_false_iff z).mp hflagFalse
    have habs : (z.abs.toNat : ℤ) = -z.toInt := by
      rw [SignedOrbit.abs_toNat]
      exact Int.ofNat_natAbs_of_nonpos (le_of_lt hneg)
    simp [hflagFalse, SignedOrbit.ofOrbit_toInt, SignedOrbit.negate_toInt]
    rw [hquotInt, habs]
    ring

theorem normalizeRatio_num_mul_gcd_toInt (q : RatioOrbit) :
    (normalizeRatio q).num.toInt *
      ((gcd q.num.abs q.den).toNat : ℤ) = q.num.toInt := by
  unfold normalizeRatio
  exact signedQuotient_mul_divisor_toInt_of_divides
    q.num (gcd q.num.abs q.den)
    (gcd_ne_zero_of_right_ne_zero q.num.abs q.den q.den_ne_zero)
    (gcd_divides_left q.num.abs q.den)

theorem normalizeRatio_den_mul_gcd_toNat (q : RatioOrbit) :
    (normalizeRatio q).den.toNat *
      (gcd q.num.abs q.den).toNat = q.den.toNat := by
  unfold normalizeRatio
  exact quotient_mul_divisor_toNat_of_divides
    (n := q.den) (d := gcd q.num.abs q.den)
    (gcd_ne_zero_of_right_ne_zero q.num.abs q.den q.den_ne_zero)
    (gcd_divides_right q.num.abs q.den)

What this page does not claim

The theorem does not claim that every division is exact, only those where the divisor divides the dividend. The theorem does not define division, it proves a property of a division already defined by repeated subtraction. The theorem does not connect this arithmetic to the framework's physical claims about recognition costs or the golden ratio.

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: