Foundation Primitive Recognition Calculus Rational Field Positive Ne Zero

What positivity means

A positive rational number is one that is greater than zero. The declaration positive_ne_zero in the Recognition Science library establishes this basic fact for its own system of rational numbers, called PRC rationals. It proves that if a PRC rational is positive, then its value is not zero. This is a formal, machine-checked theorem, not a definition or a convention.

The framework builds its rational numbers from ratio orbits, which are pairs of signed integers. A ratio orbit is positive when its numerator is non-negative and not balanced, meaning the ratio is not zero. The key theorem positive_iff_toRat_pos connects this internal definition to the ordinary mathematical meaning: a PRC rational is positive if and only if its value as a rational number is greater than zero. The theorem positive_ne_zero then follows directly: a number greater than zero cannot equal zero.

This result is part of a larger structure. The library also proves that positivity is preserved under normalization, and it defines division for PRC rationals. The theorem positive_ne_zero is a small but necessary step: it ensures that positive numbers behave as expected when used in calculations, such as canceling terms in division.

In Recognition Science, this fits into the broader project of building the rational numbers from primitive recognition calculus. The framework models a ledger of recognition events and derives mathematical structure from the cost of recognition. Within this account, the rational numbers are constructed from ratio orbits, and positivity is defined on those orbits. The theorem positive_ne_zero is a foundational check that this constructed system behaves like the rational numbers we already know.

theorem positive_ne_zero {q : PRCRat}
    (h : positive q) : q.toRat ≠ 0 :=
  ne_of_gt ((positive_iff_toRat_pos q).mp h)

theorem positive_iff_toRat_pos (q : RatioOrbit) :
    positive q ↔ 0 < q.toRat := by
  unfold positive RatioOrbit.toRat
  have hdenNat : 0 < q.den.toNat := Nat.pos_of_ne_zero q.den_toNat_ne_zero
  have hdenQ : 0 < (q.den.toNat : ℚ) := by exact_mod_cast hdenNat
  constructor
  · intro h
    have hnum_nonneg : 0 ≤ q.num.toInt :=
      (SignedOrbit.nonneg_iff_toInt_nonneg q.num).mp h.1
    have hnum_ne : q.num.toInt ≠ 0 := by
      intro hz
      exact h.2 ((SignedOrbit.balanced_iff_toInt_eq q.num SignedOrbit.zero).mpr (by
        rw [hz, SignedOrbit.zero_toInt]))
    have hnum_pos : 0 < q.num.toInt := by omega
    have hnumQ : 0 < (q.num.toInt : ℚ) := by exact_mod_cast hnum_pos
    positivity
  · intro h
    have hnum_pos : 0 < q.num.toInt := by
      have hden_ne : (q.den.toNat : ℚ) ≠ 0 := q.den_cast_ne_zero
      have hmul : 0 < ((q.num.toInt : ℚ) / (q.den.toNat : ℚ)) * (q.den.toNat : ℚ) :=
        mul_pos h hdenQ
      have hnumQ : 0 < (q.num.toInt : ℚ) := by
        field_simp [hden_ne] at hmul
        exact hmul
      exact_mod_cast hnumQ
    constructor
    · exact (SignedOrbit.nonneg_iff_toInt_nonneg q.num).mpr (by omega)
    · intro hbal
      have hnum_zero : q.num.toInt = 0 := by
        have := (SignedOrbit.balanced_iff_toInt_eq q.num SignedOrbit.zero).mp hbal
        simpa using this
      omega

What this page does not claim

The theorem does not claim that the framework's rational numbers are the only possible construction. It does not claim that positivity is defined for all ratio orbits, only for those with a non-negative numerator and a non-zero denominator. It does not claim that the framework's rational numbers are identical to the standard rational numbers, only that they behave equivalently under the defined operations.

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