Encyclopedia Foundation Foundation Primitive Recognition Calculus Orbit Divisibility

ARTICLE 5 claims 4 theorems 1 model

Foundation Primitive Recognition Calculus Orbit Divisibility

A machine-checked library proves that the divisibility structure of a primitive counting system exactly matches the divisibility of the natural numbers, including a native definition of prime numbers.

Verify this page

Orbit divisibility

In the Recognition Science framework, the foundational objects are not sets but ledger entries: a discrete record of distinct events. The primitive counting system, called DistinctionNat, is built from two operations: zero and successor. This is the same starting point as the Peano axioms for the natural numbers, but here it is derived from the structure of recognition events rather than assumed as a mathematical primitive.

The system establishes a native notion of divisibility. A number a divides b when there exists some k such that a times k equals b. The expected properties are proved: divisibility is reflexive, transitive, and antisymmetric. The divisibility relation in DistinctionNat is exactly equivalent to the standard divisibility relation on natural numbers, via a translation function toNat that maps each DistinctionNat to its corresponding natural number.

The central achievement is a native definition of prime numbers, called primeOrbit. A number is prime in this system when it is not zero, not one, and has no nontrivial factorization. A fundamental theorem holds: if a prime divides a product, then it must divide one of the factors. This is the key lemma that makes unique factorization work. This native prime definition is equivalent to the standard prime definition on natural numbers, and the system satisfies the orbit divisibility certificate, a formal statement that the divisibility structure is complete and consistent.

In Recognition Science, this result matters because it shows that the arithmetic structure of the natural numbers is not an arbitrary choice. The framework derives it from the forced structure of recognition events. The divisibility properties are not assumed; they are proved from the primitive ledger operations. This is a concrete example of how the framework's foundational claims are machine-checked, not merely asserted.

THEOREM divides_iff_toNat_dvd · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean
divides_iff_toNat_dvd · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean:114 
/-- Divisibility is native, but it displays as Nat divisibility. -/
theorem divides_iff_toNat_dvd (a b : DistinctionNat) :
    divides a b ↔ a.toNat ∣ b.toNat := by
  constructor
  · intro h
    rcases h with ⟨k, hk⟩
    refine ⟨k.toNat, ?_⟩
    have hnat := congrArg DistinctionNat.toNat hk
    rw [toNat_mul] at hnat
    exact hnat.symm
  · intro h
    rcases h with ⟨k, hk⟩
    refine ⟨ofNat k, ?_⟩
    apply toNat_inj
    rw [toNat_mul, toNat_ofNat]
    exact hk.symm
MODEL primeOrbit · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean
primeOrbit · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean:69 
/-- Native prime orbit position: nonzero, non-unit, and with no nontrivial
factorization. -/
def primeOrbit (p : DistinctionNat) : Prop :=
  p ≠ zero ∧ ¬ unit p ∧ ¬ nontrivialFactorization p
THEOREM unit_or_unit_of_mul_eq_prime · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean
unit_or_unit_of_mul_eq_prime · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean:242 
/-- 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⟩
THEOREM primeOrbit_iff_toNat_no_nontrivial_factor · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean
primeOrbit_iff_toNat_no_nontrivial_factor · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean:218 
/-- 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])
THEOREM orbit_divisibility_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean
orbit_divisibility_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitDivisibility.lean:331 
/-- The native orbit divisibility surface is closed. -/
theorem orbit_divisibility_certificate : OrbitDivisibilityCertificate where
  divides_display := divides_iff_toNat_dvd
  divides_reflexive := divides_refl
  divides_transitive := by
    intro a b c hab hbc
    exact divides_trans hab hbc
  divides_mul_right_factor := divides_mul_right
  divides_mul_left_factor := divides_mul_left
  one_divides_all := one_divides
  zero_divides_only_zero := zero_divides_iff_eq_zero
  unit_display := unit_iff_toNat_eq_one
  divides_one_exactly_units := divides_one_iff_unit
  divisor_of_unit_is_unit := by
    intro a b hb hdiv
    exact unit_of_divides_unit hb hdiv
  divides_antisymmetric := by
    intro a b hab hba
    exact divides_antisymm hab hba
  nontrivial_factorization_display := nontrivialFactorization_iff_toNat
  prime_orbit_display := primeOrbit_iff_toNat_no_nontrivial_factor
  prime_factor_property := by
    intro a b p hp hmul
    exact unit_or_unit_of_mul_eq_prime hp hmul
  prime_divisor_property := by
    intro a p hp hdiv
    exact unit_or_eq_of_divides_prime hp hdiv

What this page does not claim

This module does not prove the Riemann Hypothesis or any other statement about the distribution of primes in the natural numbers. This module does not claim that the natural numbers are the only possible counting system derived from recognition events. This module does not establish that the primeOrbit definition is the only sensible notion of primality within the framework.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND