Foundation Primitive Recognition Calculus Grow Integer Divisibility One Dvd Z

The divisibility statement

The statement one_dvdZ is a formal theorem inside the Recognition Science framework's machine-checked library of formal theorems. It says: for every signed orbit, a discrete record of recognition events that carries an integer value, the special orbit called one divides that orbit. In ordinary integer arithmetic, the analogous fact is that 1 divides every integer n, because n = 1 · n. The framework's theorem is the same idea translated into its own objects: given any signed orbit a, there exists another signed orbit c such that multiplying one by c yields a. The proof is short and rests on the definition of divisibility and on the fact that the integer value of one is 1.

The theorem is one of several basic properties of the framework's divisibility relation, called dvdZ. The library also proves reflexivity (every orbit divides itself), transitivity (if a divides b and b divides c, then a divides c), and closure under addition (if a divides b and a divides c, then a divides b + c). These are the standard elementary properties one expects of a divisibility relation. They are proved from the definitions using integer arithmetic and the framework's notion of balanced orbits, which identifies orbits that have the same integer value.

In Recognition Science, the framework models recognition events as discrete records, and the signed orbit is one of its primitive objects. The library's purpose is to show that the structure forced by recognition costs reproduces ordinary arithmetic facts. The theorem one_dvdZ is a small but necessary step: it confirms that the framework's divisibility relation behaves like the usual one on integers, at least for the special case of division by one. Without this fact, the later development of arithmetic within the framework would lack a basic foundation.

The theorem does not claim anything about the integer value of a signed orbit beyond what is needed for divisibility. It does not say that one is the only divisor of any orbit, nor does it say anything about prime factorization or the distribution of divisors. It also does not claim that the framework's divisibility relation is identical to integer divisibility in all respects; it only establishes the specific property that one divides every orbit. The theorem is a lemma in a larger development, not a standalone result about the nature of recognition.

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

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'

What this page does not claim

The theorem does not claim that one is the only divisor of any orbit. The theorem does not claim anything about prime factorization or divisor distribution. The theorem does not claim that the framework's divisibility relation is identical to integer divisibility in all respects.

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: