Foundation Primitive Recognition Calculus Grow Ratio Orbit Le Refl Total Le Q

The order on ratio orbits

A rational number is a ratio of two whole numbers, like 3/4 or 7/2. To decide which of two rationals is larger, the standard school method is cross-multiplication: compare a/b and c/d by comparing a times d with c times b. The Recognition Science declaration leQ formalizes exactly this comparison as an ordering on ratio orbits, where a ratio orbit is a signed pair of whole numbers representing a rational. The definition states that one orbit is at most another precisely when its cross-product with the other's denominator is at most the other's cross-product with its denominator.

The declaration proves two properties of this ordering. First, reflexivity: every rational is at most itself, which holds because the cross-product of a ratio with itself is literally the same signed orbit on both sides. Second, totality: for any two rationals, one is at most the other, proved by comparing the two cross-products and using the fact that whole numbers are totally ordered. Together these establish that leQ is a reflexive, total relation on ratio orbits, a foundational step for ordering the discrete ledger of recognition events that the framework builds upon.

In Recognition Science, the framework models reality as a discrete record of recognition events, and ratio orbits provide the arithmetic backbone for comparing quantities that arise in that record. The leQ declaration is a machine-checked theorem in the framework's library of formal theorems, meaning its proof has been verified by a computer to follow from the axioms of the underlying type theory. It establishes that the cross-multiplication order behaves as expected: it is complete in the sense that every pair of rationals is comparable, and it is consistent in that nothing exceeds itself.

What leQ does not claim is more modest than its name might suggest. It does not assert that this ordering is transitive, antisymmetric, or a total order in the full mathematical sense; those properties would require separate proofs. It does not claim anything about the physical content of recognition events, only about the arithmetic order on their ratio orbits. And it does not derive the golden ratio, the eight-tick cycle, or any other structure from the framework's forcing chain; it is a preliminary lemma about ordering, not a conclusion about the universe.

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

leQ does not prove transitivity or antisymmetry of the ordering. leQ does not derive the golden ratio or any other constant from the forcing chain. leQ does not make any physical claim about recognition events themselves.

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: