Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.RatioOrbitDenseMediant

show as:
view Lean formalization →

Defines the mediant of two ratio-orbits and proves it lies strictly between them under the cross-multiplication order. Anyone building density or approximation arguments on the primitive ratio lattice would cite this. The argument reduces order comparisons to signed-orbit arithmetic already developed choice-free upstream.

claimFor positive ratio-orbits $p=(a:b)$ and $q=(c:d)$, the mediant is $m=(a+c:b+d)$. Under the cross-multiplication order $\lt_Q$, one has $p\lt_Q q$ if and only if the corresponding natural comparison holds after display, and then $p\lt_Q m\lt_Q q$.

background

In the Primitive Recognition Calculus, rationals are not taken from Mathlib as a finished field. They appear as ratio-orbits: pairs of a signed numerator orbit and a positive denominator orbit, ordered by cross-multiplication. Upstream, leQ says $p\le_Q q$ exactly when the signed product $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is at most $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$ after casting dens via SignedOrbit.ofOrbit.

That order was rebuilt choice-free in the signed-orbit foundation so that reflexivity, totality, and trichotomy do not inherit classical choice from Mathlib integers. This module sits on those order modules plus the integer/rational display layer, and introduces the classical mediant construction inside that native order.

The mediant is the elementary interpolant used in Farey sequences and Stern-Brocot trees: from two adjacent fractions it produces a strictly intermediate one, which is the combinatorial engine for density of the ratio lattice.

proof idea

Three sibling pieces structure the file. First, mediant is the definition $(a:b)\oplus(c:d)=(a+c:b+d)$ on ratio-orbits. Second, ltQ_iff_toNat bridges the abstract $\lt_Q$ relation to a comparison after the natural/integer display, so inequalities can be checked in ordinary arithmetic. Third, ltQ_mediant applies that bridge: assuming $p\lt_Q q$, the two cross-multiplication inequalities for $p$ vs mediant and mediant vs $q$ expand into sums of positive denominator terms and fall out of the upstream trichotomy and order lemmas. No analytic limits; pure ordered-semiring algebra on orbits.

why it matters in Recognition Science

Density of ratio-orbits under the recognition order is a prerequisite for any continuum limit or approximation statement inside the Grow layer of Primitive Recognition Calculus. The mediant supplies an explicit, constructive witness that between any two comparable ratios sits another, without leaving the choice-free signed-orbit substrate.

No downstream edges are recorded yet on this page, so the module is presently a leaf that packages the mediant lemma for later density, continued-fraction, or ladder-approximation arguments. In the broader RS foundation it supports building continuous structure from discrete recognition steps rather than importing $\mathbb{R}$ as primitive. It does not itself touch the forcing chain T5-T8 or the J-cost; it is infrastructure under the rational skeleton those later steps presuppose.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (3)