Foundation Primitive Recognition Calculus Integer Rational Ratio Orbit Equiv Iff

The equivalence

A rational number is a fraction of whole numbers, like 3/4 or 22/7. In the Recognition Science framework, numbers are built from a discrete record of events, a ledger that tracks distinctions step by step. The framework's own rational type, PRCRat, packages these records into a structure that supports addition, multiplication, and reciprocals, mirroring the arithmetic of ordinary fractions.

The theorem ratioOrbitEquiv_iff_toRat_eq states a precise bridge: two framework rationals are equivalent in the ledger sense exactly when they map to the same ordinary rational number. In plainer terms, the ledger cannot tell two fractions apart unless they are the same fraction. This is a proved result in the machine-checked library of formal theorems, not a definitional choice or a hypothesis.

What the theorem does not claim is equally important. It does not say that the framework's rational type is identical to the conventional rational numbers; it only establishes a correspondence through the conversion function toRat. The theorem also does not assert that every ordinary rational number has a ledger representative, nor does it address how arithmetic operations behave under this correspondence. Those questions remain separate targets.

The practical consequence is that the framework's discrete arithmetic is faithful to familiar rational arithmetic at the level of equality. When a proof in the framework needs to know whether two ledger fractions are the same, it can check their ordinary rational values instead. This makes the framework's internal reasoning compatible with standard mathematics wherever rational equality is involved.

/-- Subtraction on signed orbits via the negation. -/
def sub (a b : SignedOrbit) : SignedOrbit :=
  add a (negate b)

What this page does not claim

The framework's rational type is identical to conventional rational numbers. The theorem covers how arithmetic operations behave under the conversion. The theorem asserts that every ordinary rational has a ledger representative.

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: