Foundation Primitive Recognition Calculus Grow Integer Divisibility Dvd Z Refl

Divisibility of signed orbits

In mathematics, divisibility is the relation "a divides b" when some whole number c makes a times c equal b. Every number divides itself, since a times 1 equals a. The declaration dvdZ_refl proves the same reflexive property for a new kind of object: a signed orbit, which is a discrete record of recognition events that carries a sign, like a positive or negative integer. The proof shows that for any signed orbit a, there exists a signed orbit c such that a times c is balanced with a. The witness c is the multiplicative identity, the signed orbit that behaves like the number 1.

The theorem is one of six in a machine-checked library of formal theorems. Together they establish that signed orbits form a commutative ring under divisibility: the relation is reflexive, transitive, closed under addition, and has the expected behavior for one and zero. Each proof reduces the claim to a statement about ordinary integers, where the arithmetic is already proved. The reflexivity proof, in particular, uses the fact that multiplying by the identity leaves the integer value unchanged, then applies a solver for linear arithmetic.

In Recognition Science, this divisibility structure is not an arbitrary choice. The framework models integers as signed orbits, and the divisibility relation is defined through a balancing condition: a divides b when some multiplier makes the product balanced with b. The library proves that this definition satisfies the standard algebraic laws, so the usual integer divisibility facts carry over to the recognition-event setting. This is a definitional bridge: it shows the framework's primitive objects reproduce a familiar mathematical structure.

What the theorem does not claim is more limited than it might appear. It does not say that signed orbits are integers, only that they behave like them under divisibility. It does not establish that the divisibility relation is total, antisymmetric, or unique in its witnesses. It does not connect this divisibility to the framework's deeper results about cost functions, golden ratio scaling, or spatial dimensions. Those connections, if they exist, are targets for future formal work, not consequences of this single reflexivity proof.

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

Signed orbits are not claimed to be integers, only to behave like them under divisibility. The divisibility relation is not claimed to be total, antisymmetric, or unique in its witnesses. No connection is claimed between this divisibility and the framework's results on cost functions, golden ratio, or spatial dimensions.

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: