Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitZeroLtOne

show as:
view Lean formalization →

Establishes the strict inequality $0 < 1$ on the cross-multiplication order of ratio orbits. Anyone building ordered arithmetic on choice-free signed orbits cites this base fact. The argument reduces the claim to nonnegativity and trichotomy already proved for signed orbits, then applies the ratio-orbit lift of $<$.

claimOn the ordered type of ratio orbits (fractions of signed orbits under cross-multiplication), the zero orbit is strictly less than the unit orbit: $0 <_{Q} 1$.

background

Primitive Recognition Calculus builds integers and rationals from orbits of distinctions, deliberately avoiding classical choice in the order. A signed orbit is an integer-like object; a ratio orbit is a fraction $p = n/d$ with numerator a signed orbit and denominator a positive orbit.

Order on ratio orbits is defined by cross-multiplication: $p \le_Q q$ iff the signed product $p.n \cdot q.d$ is $\le$ $q.n \cdot p.d$ in the choice-free signed-orbit order. Upstream modules supply reflexivity/totality of $\le_Q$, trichotomy for the strict order $<_Q$, and a choice-free foundation for signed-orbit comparison that does not route through Mathlib $\mathbb{Z}$ and Classical.choice.

This module sits in the Grow layer that lifts integer order facts to ratio orbits, so that later rungs can treat $0$ and $1$ as ordered constants without reintroducing choice.

proof idea

The module is a thin theorem layer around a single named fact zero_ltQ_one. It imports the choice-free signed-orbit order, the cross-multiplication $\le_Q$ package (reflexive/total), and the $<_Q$ trichotomy package. The proof identifies the zero and unit ratio orbits, reduces $0 <_Q 1$ to a signed-orbit comparison of the cross-multiplied numerators and denominators, and discharges that comparison with the already-proved positive/nonnegative facts on signed orbits together with trichotomy. No new order axioms are introduced.

why it matters in Recognition Science

Without $0 < 1$ on ratio orbits, every later positivity, reciprocal, and interval argument in the primitive calculus is blocked. The module closes a base rung in the choice-free Grow stack that begins at signed-orbit order and climbs through ratio-orbit $\le$ and $<$. Downstream consumers (not yet wired in the graph) are expected to be positivity lemmas, reciprocal bounds, and any construction that needs a strict unit interval on $Q$. In the broader Recognition forcing chain this is infrastructure rather than a T5–T8 landmark: it keeps the rational scaffold free of classical choice so later uniqueness and dimension arguments remain constructive.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (1)