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

Ordering the rationals

The rational numbers, the fractions like 3/4 and 22/7, come with a natural ordering: one fraction is less than another when its value is smaller. A basic property of any ordering is reflexivity, the rule that every number is less than or equal to itself. The declaration leQ_refl establishes exactly this in the Recognition Science framework's machine-checked library of formal theorems: for any rational p, the statement p ≤ p holds.

The proof works by cross-multiplication. To compare two fractions, the framework multiplies each numerator by the other's denominator, a standard way to compare fractions without decimals. For p ≤ p, both sides of the comparison become the same product, so the proof reduces to showing a signed orbit is less than or equal to itself, which follows directly from reflexivity of the underlying order. The companion theorem leQ_total shows the ordering is total: for any two rationals p and q, either p ≤ q or q ≤ p.

In the broader Recognition Science account, this ordering lives on RatioOrbit, a structure representing rational numbers as orbits under a growth operation. The reflexivity result is a foundational building block, one of the small facts that let the framework reason about ratios and comparisons in its primitive recognition calculus. It is not a claim about the physical world, about recognition costs, or about the golden ratio; it is a purely logical statement about the ordering of rationals, verified by the framework's formal library.

/-- 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 result does not claim anything about the physical world or about recognition costs. It does not derive the golden ratio or any other constant from the ordering. It does not establish that the ordering is well-founded or has any property beyond reflexivity and totality.

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: