Foundation Primitive Recognition Calculus Grow Ratio Orbit Le Trans Antisymm

The orbit order

A ratio orbit is a discrete record of ratios generated by repeated growth: each step multiplies the previous ratio by a fixed growth factor. The module RatioOrbitLeTransAntisymm studies the order leQ on these orbits, defined by comparing cross products. For two orbits p and q, leQ p q holds when the cross product of p's numerator with q's denominator is at most the cross product of q's numerator with p's denominator, a standard way to compare fractions without dividing.

The module proves two properties of this order. First, transitivity: if leQ p q and leQ q r, then leQ p r. The proof multiplies through by the positive outer denominators, chains the inequalities, and cancels the shared positive denominator. Second, antisymmetry: if leQ p q and leQ q p, then the cross products are equal, which is exactly the rational equivalence crossEq. Both proofs are choice-free, routed through integer cancellation lemmas.

Together these establish that leQ is a partial order on ratio orbits up to rational equivalence. This matters because the framework's growth processes generate orbits that must be comparable in a consistent way: transitivity ensures that comparisons chain without contradiction, and antisymmetry ensures that distinct orbits are not mutually ordered unless they represent the same ratio. The module is a small but load-bearing piece of the foundation: it guarantees the order used in later growth arguments is well-behaved.

In Recognition Science, the framework models physical structure as a ledger of recognition events, and ratio orbits arise naturally when growth is applied repeatedly. The order leQ provides a way to compare these orbits, and the two theorems ensure that comparison is coherent. The machine-checked library of formal theorems verifies these proofs, so the ordering properties hold with certainty within the framework's axioms.

/-- Transitivity of the delta-native cross-multiplication order `leQ` on `RatioOrbit`.
    From the two cross-product inequalities, multiply through by the (positive) outer
    denominators, chain, and cancel the shared positive denominator `q.den`.
    Choice-free: routed through the purified `SignedOrbit.le_iff_toInt_le` bridge and
    `Int` cancellation lemmas only. -/
theorem leQ_trans (p q r : RatioOrbit) (hpq : leQ p q) (hqr : leQ q r) : leQ p r := by
  unfold leQ at hpq hqr ⊢
  rw [SignedOrbit.le_iff_toInt_le] at hpq hqr ⊢
  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt] at hpq hqr ⊢
  -- hpq : p.num.toInt * q.den.toNat ≤ q.num.toInt * p.den.toNat
  -- hqr : q.num.toInt * r.den.toNat ≤ r.num.toInt * q.den.toNat
  -- goal: p.num.toInt * r.den.toNat ≤ r.num.toInt * p.den.toNat
  have hq : (0 : ℤ) < (q.den.toNat : ℤ) := by
    have := q.den_toNat_ne_zero
    omega
  have hp : (0 : ℤ) ≤ (p.den.toNat : ℤ) := Int.natCast_nonneg _
  have hr : (0 : ℤ) ≤ (r.den.toNat : ℤ) := Int.natCast_nonneg _
  have hchain : p.num.toInt * (r.den.toNat : ℤ) * (q.den.toNat : ℤ)
      ≤ r.num.toInt * (p.den.toNat : ℤ) * (q.den.toNat : ℤ) := by
    calc p.num.toInt * (r.den.toNat : ℤ) * (q.den.toNat : ℤ)
        = p.num.toInt * (q.den.toNat : ℤ) * (r.den.toNat : ℤ) := by ring
      _ ≤ q.num.toInt * (p.den.toNat : ℤ) * (r.den.toNat : ℤ) :=
          Int.mul_le_mul_of_nonneg_right hpq hr
      _ = q.num.toInt * (r.den.toNat : ℤ) * (p.den.toNat : ℤ) := by ring
      _ ≤ r.num.toInt * (q.den.toNat : ℤ) * (p.den.toNat : ℤ) :=
          Int.mul_le_mul_of_nonneg_right hqr hp
      _ = r.num.toInt * (p.den.toNat : ℤ) * (q.den.toNat : ℤ) := by ring
  exact Int.le_of_mul_le_mul_right hchain hq

/-- Antisymmetry of `leQ` up to the rational equivalence `crossEq`: mutual `leQ`
    forces the cross products to be equal, which is exactly `crossEq` through the
    purified `crossEq_iff_toIntCross` bridge. Choice-free. -/
theorem leQ_antisymm (p q : RatioOrbit) (hpq : leQ p q) (hqp : leQ q p) :
    RatioOrbit.crossEq p q := by
  unfold leQ at hpq hqp
  rw [SignedOrbit.le_iff_toInt_le] at hpq hqp
  simp only [SignedOrbit.mul_toInt, SignedOrbit.ofOrbit_toInt] at hpq hqp
  rw [RatioOrbit.crossEq_iff_toIntCross]
  exact Int.le_antisymm hpq hqp

What this page does not claim

This module does not define the growth factor or prove any properties about specific growth values. The order leQ is not shown to be total; the module only establishes transitivity and antisymmetry.

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