Foundation Primitive Recognition Calculus Grow Ratio Orbit Mul Pos Zero Lt Q Iff

The positive-orbit test

In the recognition framework, a discrete record of events, growth is tracked by ratios of two natural-number counts. The theorem zero_ltQ_iff_num states that one ratio orbit is positive exactly when its numerator's positive count exceeds its negative count. In plain terms: if you write a ratio as a pair of counts, the ratio is greater than zero precisely when the first count is larger than the second. The proof is a direct rewrite of the definition, so the statement is a theorem, not a definitional choice.

The supporting theorem mul_strictpos_cf shows that the product of two positive ratio orbits is again positive. The proof expands the product into the four count products, uses the hypothesis that each factor's positive count exceeds its negative count, and finishes with arithmetic and the omega tactic. This closure property matters because it means the positive ratios form a multiplicative structure: once you know two ratios are positive, their product is positive too. The theorem ltQ_mul_pos packages this for the ratio-orbit type, using the first theorem to translate the positivity hypothesis into count inequalities.

What the declaration does not claim is broader. It does not say that positivity of a ratio corresponds to any physical measurement, nor that the ratio orbit itself is a real number. It only establishes an equivalence between two formal conditions inside the framework's own language. The theorem is a stepping stone for later results about growth ordering, not a statement about the empirical world. The library is a machine-checked collection of formal theorems, and this one is a small, exact link in that chain.

theorem zero_ltQ_iff_num (r : RatioOrbit) : ltQ RatioOrbit.zero r ↔ r.num.neg.toNat < r.num.pos.toNat := by
  unfold ltQ leQ RatioOrbit.crossEq
  constructor
  · rintro ⟨hle, hne⟩
    rw [le_iff_toNat_cf] at hle
    rw [SignedOrbit.balanced_iff_toNat_eq] at hne
    simp only [RatioOrbit.zero, SignedOrbit.mul, SignedOrbit.ofOrbit, SignedOrbit.zero, SignedOrbit.scaleByNat, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero, DistinctionNat.toNat_succ] at hle hne
    omega
  · intro h
    refine ⟨?_, ?_⟩
    · rw [le_iff_toNat_cf]
      simp only [RatioOrbit.zero, SignedOrbit.mul, SignedOrbit.ofOrbit, SignedOrbit.zero, SignedOrbit.scaleByNat, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero, DistinctionNat.toNat_succ]
      omega
    · intro hbal
      rw [SignedOrbit.balanced_iff_toNat_eq] at hbal
      simp only [RatioOrbit.zero, SignedOrbit.mul, SignedOrbit.ofOrbit, SignedOrbit.zero, SignedOrbit.scaleByNat, DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_zero, DistinctionNat.toNat_succ] at hbal
      omega

theorem mul_strictpos_cf (a b : SignedOrbit) (ha : a.neg.toNat < a.pos.toNat) (hb : b.neg.toNat < b.pos.toNat) : (SignedOrbit.mul a b).neg.toNat < (SignedOrbit.mul a b).pos.toNat := by
  have hpos : (SignedOrbit.mul a b).pos.toNat = a.pos.toNat * b.pos.toNat + a.neg.toNat * b.neg.toNat := by
    show (a.pos * b.pos + a.neg * b.neg).toNat = _
    rw [DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul]
  have hneg : (SignedOrbit.mul a b).neg.toNat = a.pos.toNat * b.neg.toNat + a.neg.toNat * b.pos.toNat := by
    show (a.pos * b.neg + a.neg * b.pos).toNat = _
    rw [DistinctionNat.toNat_add, DistinctionNat.toNat_mul, DistinctionNat.toNat_mul]
  rw [hpos, hneg]; obtain ⟨s, hs⟩ := Nat.exists_eq_add_of_lt ha; obtain ⟨t, ht⟩ := Nat.exists_eq_add_of_lt hb; rw [hs, ht]; ring_nf; omega

What this page does not claim

This does not claim that the theorem assigns physical meaning to positivity. This does not claim that ratio orbits are real numbers. This does not claim that the product-closure property holds for all signed orbits without the positivity hypothesis.

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