RatioOrbit
plain-language theorem explainer
A rational orbit is an integer numerator (signed orbit difference) over a nonzero finite distinction count. It is the native display type for rational values in the primitive recognition calculus. Cost and gauge-orbit classification cite it as the domain of native cost functionals. The declaration is a plain structure with a nonzero-denominator side condition; no proof content.
Claim. A rational orbit is a triple $(n,d,h)$ where $n$ is a signed orbit (difference of two finite distinction counts), $d$ is a finite distinction count, and $h$ asserts $d \neq 0$. It is the native display of a rational $n/d$ built only from repeated distinction.
background
In the primitive recognition calculus, quantities are built from repeated distinction rather than from bare naturals or integers. DistinctionNat (K2.12) is the base-neutral finite orbit of that process: an inductive zero/successor type standing in for a count of distinctions. SignedOrbit (K4.6) packages two such counts as a formal difference pos - neg, giving a signed integer display without importing $\mathbb{Z}$ as primitive.
This module (IntegerRational) lifts those ingredients to rationals. A rational orbit is exactly an integer numerator over a nonzero orbit denominator. The nonzero side condition is stated at the type level so every inhabitant is a well-formed rational display. Downstream cost work treats these displays as the domain of native cost maps and of the rational trace used to classify gauges.
proof idea
No proof. The declaration is a structure with three fields: a signed-orbit numerator, a distinction-count denominator, and a proof that the denominator is not zero. Downstream code projects the fields and uses the side condition when converting to rationals or when forming products and sums of displays.
why it matters
Rational orbits are the carrier type for the gauge-orbit cost classification. Parent results in GaugeOrbitClassification quantify over them: cost_display relates native cost to the rational trace on a display; cost_at_zero, cost_at_neg, and cost_at_pos pin the cost on zero, negative, and positive displays; degenerate_is_signGauge and charges_at_two_iff_not_signGauge identify the degenerate branch with the sign cost and characterize nondegeneracy without exponents.
In the Recognition framework this sits under the foundation layer that feeds J-cost uniqueness (T5) and the Recognition Composition Law. The structure itself does not force $J$ or $\phi$; it supplies the rational domain on which those cost identities are later stated and compared to the sign gauge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.