Foundation Primitive Recognition Calculus Orbit Divisibility Of Nat Ne Zero Of N

The zero distinction

The declaration ofNat_ne_zero_of_ne_zero is a small but load-bearing result in the Recognition Science library. It states that if a natural number n is not zero, then its image under the map that converts natural numbers into distinction positions (the discrete slots on a recognition orbit) is also not the zero position. In plain terms: a nonzero counting number never lands on the empty slot. The proof is a one-line argument by contradiction: if the image were zero, then converting back to a natural number would force n to be zero, contradicting the assumption.

The statement is a theorem, not a definition. It is proved in the machine-checked library of formal theorems, and it is used to ensure that the arithmetic of distinction positions behaves like ordinary arithmetic on nonzero natural numbers. The declaration is a private helper, meaning it is not part of the public interface, but it supports the public theorem divides_iff_toNat_dvd, which states that divisibility on distinction positions is exactly the same as divisibility on the underlying natural numbers. That equivalence is what lets the framework treat orbit positions as a faithful copy of the natural numbers for divisibility questions.

What the declaration does not claim is just as precise. It does not say that every nonzero natural number has a distinct position; injectivity is a separate statement. It does not say that the zero position is unreachable from any nonzero input under all operations; it only covers the conversion map. And it does not say anything about prime positions or factorization. Those results, such as primeOrbit_iff_toNat_no_nontrivial_factor, are separate theorems in the same file, and they rely on this zero-result as a stepping stone but are not consequences of it alone.

The practical upshot is that the framework's arithmetic on recognition orbits is grounded in ordinary natural-number arithmetic. When a reader sees a divisibility statement about orbit positions, they can translate it into a statement about natural numbers and check it there. The zero-result is the guard that makes that translation safe for the nonzero case, and it is one of the small facts that let the larger structure of the framework stand on a proved foundation rather than on an assumption.

private theorem ofNat_ne_zero_of_ne_zero {n : Nat} (h : n ≠ 0) :
    ofNat n ≠ zero := by
  intro hz
  have hnat := congrArg DistinctionNat.toNat hz
  rw [toNat_ofNat, toNat_zero] at hnat
  exact h hnat

private theorem ofNat_ne_zero_of_ne_zero {n : Nat} (h : n ≠ 0) :
    ofNat n ≠ zero := by
  intro hz
  have hnat := congrArg DistinctionNat.toNat hz
  rw [toNat_ofNat, toNat_zero] at hnat
  exact h hnat

/-- 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

What this page does not claim

The declaration does not state that the conversion map is injective. The declaration does not say anything about prime positions or factorization. The declaration does not cover the behavior of the zero position under all operations.

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: