Foundation Primitive Recognition Calculus Grow Integer Divisibility Balanced To

Balanced orbits and the integer they share

In mathematics, a recognition event is a discrete record of a comparison. The Recognition Science framework builds arithmetic from such records. Its objects are called signed orbits, and each one carries an integer value, its toInt. The theorem balanced_toInt_eq states a simple bridge: if two signed orbits are balanced, meaning they stand in a certain structural relation of equal magnitude, then their integer values are equal.

The converse also holds. A companion theorem, balanced_of_toInt_eq, says that if two signed orbits have the same integer value, then they are balanced. Together the two theorems make balance and equality of integer values equivalent. This is not a deep result about numbers; it is a definitional consistency check. The framework defines balance in terms of underlying natural-number magnitudes, and toInt is defined by a sign and a magnitude. The theorem simply unpacks those definitions and verifies that the two notions agree.

This equivalence matters because it lets the framework transfer integer arithmetic onto its own objects. A later definition, dvdZ, uses balance to define divisibility for signed orbits: a divides b when there exists a c such that a * c is balanced with b. The theorems dvdZ_refl, dvdZ_trans, dvdZ_add, one_dvdZ, and dvdZ_zero then prove that this divisibility relation is reflexive, transitive, closed under addition, and has the expected behavior for one and zero. These are the standard properties of divisibility, now derived inside the framework from its own primitive notions.

The theorem balanced_toInt_eq does not claim that the framework's arithmetic is the only possible arithmetic, nor that balance is the only way to define equality of integers. It does not say anything about the physical world, about recognition costs, or about the golden ratio. It is a narrow, internal consistency result: within the framework's definitions, balance and integer equality coincide. Its value is architectural, not empirical. It shows that the framework's structural relations line up with the familiar arithmetic that ordinary mathematics uses, so that later results built on divisibility can be trusted to behave as expected.

theorem balanced_toInt_eq {x y : SignedOrbit} (h : SignedOrbit.balanced x y) :
    x.toInt = y.toInt := by
  have hn := (SignedOrbit.balanced_iff_toNat_eq x y).mp h
  unfold SignedOrbit.toInt
  omega

theorem balanced_of_toInt_eq {x y : SignedOrbit} (h : x.toInt = y.toInt) :
    SignedOrbit.balanced x y := by
  rw [SignedOrbit.balanced_iff_toNat_eq]
  unfold SignedOrbit.toInt at h
  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'

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_zero (a : SignedOrbit) : dvdZ a SignedOrbit.zero := by
  refine ⟨SignedOrbit.zero, balanced_of_toInt_eq ?_⟩
  rw [SignedOrbit.mul_toInt, SignedOrbit.zero_toInt]
  omega

What this page does not claim

The theorem does not say that balance is the only way to define equality of integers. It does not claim anything about physical constants, recognition costs, or the golden ratio. It does not establish that the framework's arithmetic is the only possible arithmetic.

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: