Foundation Primitive Recognition Calculus Grow Ratio Orbit Le Refl Total

Ordering the rationals

The rational numbers, fractions like 2/3 or 7/4, have a familiar ordering: one fraction is less than another when its value is smaller. The classical way to compare two fractions a/b and c/d without computing decimals is cross-multiplication: a/b ≤ c/d exactly when a×d ≤ c×b. This definition is simple, but it carries a subtlety. The sign of the comparison depends on the signs of the denominators, and the classical rule quietly assumes positive denominators.

In the Recognition Science framework, the rationals appear as ratio orbits, discrete records of a growth process where each step multiplies by a fixed ratio. The framework's library, a machine-checked collection of formal theorems, builds an ordering on these orbits that handles signs explicitly. The module RatioOrbitLeReflTotal defines the order leQ by cross-multiplication, but it casts each denominator through a signed orbit construction so that the comparison is valid for positive and negative rationals alike.

The module then proves two properties that any useful ordering must have. Reflexivity, leQ p p, says every rational is less than or equal to itself; the proof observes that the cross-product on both sides is literally the same signed orbit. Totality, leQ p q or leQ q p, says any two rationals are comparable: one is always less than or equal to the other. Both proofs are short and direct, relying on the corresponding properties of the signed orbit ordering at the cross-product level.

In Recognition Science, the framework proves that a specific cost function, J(x) = (x + 1/x)/2 - 1, is forced by five plain conditions, and from that cost the framework derives a chain of consequences including the golden ratio and the eight-tick recognition cycle. The total order on ratio orbits is part of the primitive recognition calculus, the foundational layer on which those later results rest. Establishing that the ordering is total means the framework can compare any two growth states unambiguously, a prerequisite for defining which states are reachable from which.

The practical consequence is that the framework's growth dynamics have a well-defined notion of progress: given any two ratio orbits, one is always ahead of the other. This is not a deep mathematical surprise, but it is a load-bearing piece of infrastructure. Without totality, comparisons between growth states would sometimes be undefined, and the forcing chain that produces the framework's constants could not get off the ground.

/-- Cross-multiplication order on `RatioOrbit`: `leQ p q` iff the signed orbit
    `p.num * q.den` is `≤` the signed orbit `q.num * p.den`, where the positive
    distinctions (dens) are cast in via `SignedOrbit.ofOrbit`. -/
def leQ (p q : RatioOrbit) : Prop :=
  SignedOrbit.le
    (SignedOrbit.mul p.num (SignedOrbit.ofOrbit q.den))
    (SignedOrbit.mul q.num (SignedOrbit.ofOrbit p.den))

/-- Reflexivity of `leQ`: every rational is ≤ itself. Proved by `le_refl_cf`
    at the cross-product, which is literally the same signed orbit on both sides. -/
theorem leQ_refl (p : RatioOrbit) : leQ p p := by
  unfold leQ
  exact le_refl_cf _

/-- Totality of `leQ`: for any two rationals, one is ≤ the other. Proved by
    `le_total_cf` at the two cross-products. -/
theorem leQ_total (p q : RatioOrbit) : leQ p q ∨ leQ q p := by
  unfold leQ
  exact le_total_cf _ _

What this page does not claim

This module does not derive the cost function J or any of the framework's physical constants. The totality proof does not establish that the ordering is transitive, which would require a separate theorem. The signed orbit construction is a definitional choice, not a derived consequence of the framework's axioms.

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/RatioOrbitLeReflTotal.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: