mediant
plain-language theorem explainer
Defines the mediant of two rational orbits: add numerators and denominators componentwise, recovering the classical (a+c)/(b+d). Anyone proving density of the ratio orbit order under successive refinement cites this constructor. The only nontrivial obligation is that the summed denominator stays nonzero, discharged by transporting both denominators to Nat and using omega.
Claim. For rational orbits $p=(n_p/d_p)$ and $q=(n_q/d_q)$ (signed-orbit numerators over nonzero distinction-orbit denominators), the mediant is the rational orbit $(n_p+n_q)/(d_p+d_q)$, with the sum of denominators proved nonzero.
background
In the primitive recognition calculus, rationals are not assumed as a base type. A RatioOrbit is a display of a signed orbit numerator over a nonzero DistinctionNat denominator (K4.7). DistinctionNat is the base-neutral finite orbit of repeated distinction (zero/succ). SignedOrbit packages a difference of two such orbits (intended meaning pos minus neg).
The mediant is the standard Farey/Stern–Brocot combination of two fractions. Here it is realized entirely inside the orbit arithmetic: numerators add via SignedOrbit.add, denominators via the monoid structure on DistinctionNat. Nonzeroness of denominators is tracked by a structure field den_ne_zero, so the constructor must re-establish it for the sum.
Upstream, den_toNat_ne_zero states that each denominator's verifier Nat is nonzero, and toNat_add (on distinction/logic Nats) recovers ordinary Nat addition under the iteration-count map. Those facts let the nonzeroness proof leave the orbit layer and finish in Nat.
proof idea
The definition sets num to the signed-orbit sum of the two numerators and den to the sum of the two denominators. The sole proof obligation is den_ne_zero for that sum.
Assume for contradiction the sum equals zero. Apply RatioOrbit.den_toNat_ne_zero to both inputs, so each den.toNat is a positive Nat. Transport the sum via DistinctionNat.toNat_add, obtaining 0 = p.den.toNat + q.den.toNat after rewriting the zero hypothesis. Then omega closes the contradiction on Nats.
why it matters
This is the constructive step that feeds density of the rational orbit order. The immediate parent is ltQ_mediant, which asserts that if $p < q$ in the ratio-orbit order then $p$ is strictly less than the mediant and the mediant is strictly less than $q$. That sandwich is the orbit-level analogue of the classical mediant property used in Farey sequences and Stern–Brocot trees.
In the Recognition foundation stack, ratio orbits sit above signed and distinction orbits as the first genuine rational layer (K4.7). Having a closed mediant operation inside that layer, without smuggling in Mathlib rationals, keeps the growth/order development choice-free and native to the forcing chain's arithmetic-from-logic path. It does not itself touch T5–T8 or the J-cost; it is infrastructure for later comparison and density arguments on displays of recognition ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.