Foundation Primitive Recognition Calculus Orbit Divisibility Prime Orbit Of Unit

The prime orbit test

A prime number is classically defined by its divisors: an integer greater than 1 is prime when its only positive divisors are 1 and itself. The Recognition Science framework's library of machine-checked formal theorems contains a parallel definition built not from divisors but from multiplication alone. In this setting, a distinction number is a counting object built from zero by repeated successors, and the unit is the number one, the multiplicative identity. A distinction number is called a prime orbit when it is not zero, not one, and cannot be written as a product of two numbers that are both different from one. This mirrors the classical definition: a number with no nontrivial factorization is prime.

The theorem primeOrbit_of_unit_or_unit states the reverse direction. It says that if a distinction number is not zero, is not one, and has the property that whenever it equals a product of two numbers, at least one of those two numbers is one, then it is a prime orbit. In plainer terms: if a number can only be split into a product when one of the factors is the number one, then that number is prime. The proof is direct. Given a hypothetical nontrivial factorization, the theorem's hypothesis forces one of the factors to be one, which contradicts the requirement that both factors differ from one.

This result is the mirror image of a companion theorem, unit_or_unit_of_mul_eq_prime, which starts from a prime orbit and concludes that any product equal to it must have a unit as a factor. Together the two theorems form an equivalence: the property of having no nontrivial factorization and the property that every factorization contains a unit are the same property. The framework's library proves both directions, and the definitions are tied to ordinary natural numbers through a translation map, so the prime orbits of the framework correspond exactly to the usual prime numbers.

In Recognition Science, this correspondence matters because the framework builds arithmetic from recognition events, discrete records of distinctions, rather than assuming numbers as a starting point. The theorem shows that the classical notion of primality survives the translation into this recognition-based setting. It is a structural check: the framework's arithmetic behaves like ordinary arithmetic where it counts. The result does not, however, establish anything about the distribution of primes, the infinitude of primes, or any deep number-theoretic fact. It is a local equivalence between two ways of defining what a prime is.

/-- Native prime orbit position: nonzero, non-unit, and with no nontrivial
factorization. -/
def primeOrbit (p : DistinctionNat) : Prop :=
  p ≠ zero ∧ ¬ unit p ∧ ¬ nontrivialFactorization p

/-- Converse native factor theorem: if a nonzero non-unit orbit position has
only unit factors, then it is a prime orbit. -/
theorem primeOrbit_of_unit_or_unit
    {p : DistinctionNat}
    (hp0 : p ≠ zero)
    (hp1 : ¬ unit p)
    (hfac : ∀ a b : DistinctionNat, a * b = p → unit a ∨ unit b) :
    primeOrbit p := by
  refine ⟨hp0, hp1, ?_⟩
  intro hnon
  rcases hnon with ⟨a, b, _ha0, _hb0, ha1, hb1, hmul⟩
  rcases hfac a b hmul with ha | hb
  · exact ha1 ha
  · exact hb1 hb

/-- If an orbit is prime, every native factorization has a unit factor. -/
theorem unit_or_unit_of_mul_eq_prime {a b p : DistinctionNat}
    (hp : primeOrbit p) (hmul : a * b = p) :
    unit a ∨ unit b := by
  by_cases ha0 : a = zero
  · exfalso
    rcases hp with ⟨hp0, _, _⟩
    apply hp0
    rw [← hmul, ha0, zero_mul_eq]
  · by_cases hb0 : b = zero
    · exfalso
      rcases hp with ⟨hp0, _, _⟩
      apply hp0
      rw [← hmul, hb0, mul_zero_eq]
    · by_cases ha1 : unit a
      · exact Or.inl ha1
      · by_cases hb1 : unit b
        · exact Or.inr hb1
        · exfalso
          rcases hp with ⟨_, _, hnf⟩
          exact hnf ⟨a, b, ha0, hb0, ha1, hb1, hmul⟩

/-- Native prime-orbit predicate displays as the Nat no-nontrivial-factor
predicate, without defining primality by importing Nat prime theory. -/
theorem primeOrbit_iff_toNat_no_nontrivial_factor (p : DistinctionNat) :
    primeOrbit p ↔
      p.toNat ≠ 0 ∧ p.toNat ≠ 1 ∧
        ¬ ∃ a b : Nat,
          a ≠ 0 ∧ b ≠ 0 ∧ a ≠ 1 ∧ b ≠ 1 ∧ a * b = p.toNat := by
  unfold primeOrbit
  rw [unit_iff_toNat_eq_one, nontrivialFactorization_iff_toNat]
  constructor
  · intro h
    rcases h with ⟨hp0, hp1, hfac⟩
    refine ⟨?_, hp1, hfac⟩
    intro hz
    have : p = zero := by
      apply toNat_inj
      rw [hz, toNat_zero]
    exact hp0 this
  · intro h
    rcases h with ⟨hp0, hp1, hfac⟩
    refine ⟨?_, hp1, hfac⟩
    intro hz
    exact hp0 (by rw [hz, toNat_zero])

What this page does not claim

The theorem does not prove the infinitude of primes or any statement about the distribution of primes. The theorem does not establish unique factorization for distinction numbers. The framework's arithmetic is not claimed to be identical to ordinary arithmetic in every respect, only in the properties proved in the library.

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