Foundation Primitive Recognition Calculus Grow Integer Divisibility

Integer divisibility in signed orbits

Divisibility is the relation that says one whole number goes evenly into another: 6 divides 12 because 6 times 2 equals 12. It is the backbone of prime numbers, greatest common divisors, and much of arithmetic. The question here is whether this relation still behaves when numbers are not the familiar integers but signed orbits, objects that represent how far a discrete record of recognition events has grown, with a sign attached for direction. The framework's library, a machine-checked collection of formal theorems, shows that the answer is yes.

In Recognition Science, a ledger, a discrete record of events, grows in ticks. Each signed orbit encodes an integer amount of growth: positive for forward steps, negative for backward, zero for none. The library defines divisibility for these orbits exactly as one would hope: an orbit a divides an orbit b when there exists some orbit c such that multiplying a by c lands on b. This mirrors the classical definition, where a divides b if b equals a times some integer.

The module then proves the standard properties that make divisibility useful. It is reflexive: every orbit divides itself. It is transitive: if a divides b and b divides c, then a divides c. It respects addition: if a divides both b and c, then a divides their sum. The orbit representing one divides everything, and every orbit divides the zero orbit. These are not asserted as assumptions; each is a theorem checked by the machine.

The proofs work by translating each signed orbit to an ordinary integer, proving the property there, and translating back. The library establishes that two orbits are balanced, meaning they represent the same integer, exactly when their translated integers are equal. This bridge is what lets familiar integer arithmetic carry over to the recognition setting. The result is that the entire edifice of divisibility, and with it the theory of primes and factorization, stands intact on the ledger.

What this establishes in plain language is that the recognition framework does not distort one of the most basic structures in mathematics. If the ledger is real, then the integers and their divisibility relations are not an external imposition; they emerge from the growth of discrete records. A reader can now trust that any number-theoretic argument that relies on divisibility, from Euclid's lemma to the fundamental theorem of arithmetic, has a counterpart inside the framework.

def dvdZ (a b : SignedOrbit) : Prop :=
  ∃ c : SignedOrbit, SignedOrbit.balanced (SignedOrbit.mul a c) b

theorem dvdZ_refl (a : SignedOrbit) : dvdZ a a := by
  refine ⟨SignedOrbit.one, balanced_of_toInt_eq ?_⟩
  rw [SignedOrbit.mul_toInt, SignedOrbit.one_toInt]
  omega

theorem dvdZ_trans (a b c : SignedOrbit) (hab : dvdZ a b) (hbc : dvdZ b c) : dvdZ a c := by
  obtain ⟨w, hw⟩ := hab
  obtain ⟨v, hv⟩ := hbc
  refine ⟨SignedOrbit.mul w v, balanced_of_toInt_eq ?_⟩
  have hw' := balanced_toInt_eq hw
  have hv' := balanced_toInt_eq hv
  rw [SignedOrbit.mul_toInt] at hw' hv'
  rw [SignedOrbit.mul_toInt, SignedOrbit.mul_toInt]
  linear_combination v.toInt * hw' + hv'

theorem dvdZ_add (a b c : SignedOrbit) (hab : dvdZ a b) (hac : dvdZ a c) :
    dvdZ a (SignedOrbit.add b c) := by
  obtain ⟨w, hw⟩ := hab
  obtain ⟨v, hv⟩ := hac
  refine ⟨SignedOrbit.add w v, balanced_of_toInt_eq ?_⟩
  have hw' := balanced_toInt_eq hw
  have hv' := balanced_toInt_eq hv
  rw [SignedOrbit.mul_toInt] at hw' hv'
  rw [SignedOrbit.mul_toInt, SignedOrbit.add_toInt, SignedOrbit.add_toInt]
  linear_combination hw' + hv'

theorem balanced_toInt_eq {x y : SignedOrbit} (h : SignedOrbit.balanced x y) :
    x.toInt = y.toInt := by
  have hn := (SignedOrbit.balanced_iff_toNat_eq x y).mp h
  unfold SignedOrbit.toInt
  omega

theorem balanced_of_toInt_eq {x y : SignedOrbit} (h : x.toInt = y.toInt) :
    SignedOrbit.balanced x y := by
  rw [SignedOrbit.balanced_iff_toNat_eq]
  unfold SignedOrbit.toInt at h
  omega

What this page does not claim

This module does not prove the fundamental theorem of arithmetic or any theorem about prime factorization. It does not define or prove properties of greatest common divisors or least common multiples. It does not connect divisibility to the physical constants or the dimension forcing results.

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/Grow/IntegerDivisibility.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: