Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitZeroLtOne

show as:
view Lean formalization →

Establishes that the zero ratio-orbit is strictly below the unit ratio-orbit under the cross-multiplication order on RatioOrbit. Anyone building ordered rationals from signed orbits without classical choice cites this base inequality. The argument reduces 0 < 1 to a nonnegativity fact on signed orbits via the already-proved trichotomy and reflexivity/totality layers.

claimOn ratio orbits ordered by cross-multiplication, the zero orbit is strictly less than the unit orbit: $\mathrm{ltQ}(0,1)$ holds, equivalently $0\cdot 1 < 1\cdot 1$ after casting positive denominators into signed orbits.

background

Primitive Recognition Calculus grows ordered rationals from orbits of distinctions rather than from Mathlib's $\mathbb{Z}$ and $\mathbb{Q}$. A ratio orbit is a pair of a signed numerator orbit and a positive denominator orbit. The order leQ is defined by cross-multiplication: $p \le q$ iff the signed product $p.\mathrm{num}\cdot q.\mathrm{den}$ is $\le$ $q.\mathrm{num}\cdot p.\mathrm{den}$, with dens cast via SignedOrbit.ofOrbit.

Upstream, RatioOrbitLeReflTotal supplies reflexivity and totality of that order, and RatioOrbitLtTrichotomy supplies the strict order and trichotomy. SignedOrbitOrderChoiceFree removes classical choice from the signed-orbit comparison that those layers rest on, so downstream rungs need not inherit Classical.choice through toInt.

This module sits at the first concrete numerical fact in that tower: zero below one.

proof idea

The module is a thin proof layer, not a definition dump. It specializes the imported ltQ relation to the canonical zero and unit ratio orbits. Cross-multiplication reduces the claim to a comparison of signed orbits that is already available from the choice-free signed order and the trichotomy/totality modules. Expect a short lemma zero_ltQ_one that unfolds ltQ, applies the cross-multiply definition, and discharges the resulting signed inequality by the integer/signed-orbit order facts already in scope.

why it matters in Recognition Science

In the Recognition foundation, every later comparison of phi-ladder rungs, mass ratios, and cost values presupposes a clean ordered field of rationals built without smuggling classical choice into the order. The fact $0<1$ is the seed inequality that orients the entire positive cone.

No downstream edges are recorded yet on this page, so the module is presently a leaf in the import graph. It still closes an obligatory base case for any parent that needs strict positivity of the unit, ordered-field axioms on RatioOrbit, or normalization of defects against a unit yardstick. It continues the choice-free program begun in SignedOrbitOrderChoiceFree and the Grow order stack (RatioOrbitLeReflTotal, RatioOrbitLtTrichotomy).

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (1)