Foundation Primitive Recognition Calculus Integer Rational

The primitive number line

Integers and rational numbers are the most basic tools of counting and measuring. An integer is a whole number, positive, negative, or zero. A rational number is a ratio of two integers, like 2/3 or 7/4. In the Recognition Science framework, these familiar objects are not assumed as given. The construction called foundation primitive recognition calculus integer rational builds them from a more primitive starting point: the discrete record of distinctions that the framework calls a ledger, a record of events that are either marked or not.

The construction begins with signed orbits, which are pairs of natural numbers representing a count and a sign. The integer type PRCInt is defined as a quotient of these orbits, meaning that different pairs which represent the same integer, such as (2, 0) and (3, 1), are identified. This is the standard mathematical technique of building integers from natural numbers. The construction then proves the basic facts one expects: zero maps to 0, one maps to 1, and the operations of addition, subtraction, and multiplication behave correctly. The same pattern extends to rationals, where PRCRat is built from ratio orbits, pairs of integers representing a numerator and a denominator.

In Recognition Science, this is the first rung of a ladder. The framework's central theorem derives a unique cost function from five plain conditions, and from that cost function it forces the golden ratio, an eight-tick recognition cycle, and three spatial dimensions. But before any of that can happen, the framework needs a number system to state its own laws. This construction supplies that foundation: a machine-checked construction of integers and rationals from the primitive ledger, with the arithmetic laws proved rather than assumed.

The practical consequence is that the framework's later results do not rest on an unexamined import of ordinary arithmetic. When the framework speaks of costs, scalings, or particle masses, it is using numbers that were themselves derived from the same primitive distinctions. This construction is a piece of the framework's self-contained starting point, the ground floor on which the forcing chain is built.

/-- K4.8. PRC integers as signed-orbit quotient classes. The quotient is
taken by the internal balanced-length relation; the verifier display into
`ℤ` is a downstream theorem. -/
def PRCInt : Type :=
  Quot signedOrbitSetoid

/-- K4.8. PRC rationals as nonzero-denominator ratio-orbit quotient classes,
identified by cross-multiplication of orbit-level numerator and denominator. -/
def PRCRat : Type :=
  Quot ratioOrbitSetoid

@[simp] theorem zero_toInt :
    zero.toInt = 0 := by
  rfl

@[simp] theorem one_toInt :
    one.toInt = 1 := by
  rfl

What this page does not claim

Not a claim that this construction derives the cost function or any later forcing result. Not a claim that the constructed numbers are the only way to build arithmetic in 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/IntegerRational.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: