rationalTrace_nat_mono
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the rational doubled-trace display is monotone on the positive integers: if 1 ≤ m ≤ n then the trace at m is at most the trace at n. Cost and character-factorization arguments cite this to push integer comparisons through the real display. The proof applies the packed monotone hypothesis on natural orbits, casts to ℝ, and finishes by linear arithmetic on the unfolded display.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). For natural numbers $m,n$ with $1 \le m \le n$, the rational doubled-trace display of $F$ obeys $\mathrm{Tr}_F(m) \le \mathrm{Tr}_F(n)$.
background
This module builds a real character factorization of native cost on ratio orbits. The rational doubled trace rationalTrace F is the real display of the carrier-valued doubled trace evaluated on the ratio-orbit of a rational: it turns the symbolic cost into an honest function $\mathbb{Q}\to\mathbb{R}$.
Natural numbers embed as orbits via natOrbit n = ratioOrbitOfRat (n : ℚ), with natOrbit_toRat recovering the integer as a rational. The hypothesis pack SansAnchorHypotheses F is the anchor-free structural pack matching the PRC native-cost axioms without a fixed anchor: base-sans-two, sign-reversing, monotone on positive integer orbits, and zero-calibrated doubled trace.
Monotonicity of $F$ on positive integer orbits is the ingredient used here; the theorem lifts that orbit-level order to the real-valued rational trace on $\mathbb{N}_{\ge 1}$.
proof idea
From $1\le m\le n$ obtain $1\le n$ by le_trans. Apply the packed monotone field of SansAnchorHypotheses to the natural orbits of $m$ and $n$, supplying the positive-integer witnesses and the orbit comparison rewritten via natOrbit_toRat and exact_mod_cast on $m\le n$.
Rewrite the resulting orbit inequality as a comparison of .toRat values on $F$ at those orbits, then cast to $\mathbb{R}$. Unfold rationalTrace, natOrbit, traceDisplay, and the doubled-trace arithmetic (mul_toRat, add_toRat, constants), push_cast, and close with linarith.
why it matters
Integer monotonicity of the rational trace is the bridge from the structural monotone axiom to concrete comparisons used in character extraction. Downstream, nontrivialCharacterValue_nat_trace_mono lifts it to the nontrivial linear extraction (character value plus inverse) on naturals, and rationalTrace_nat_eq_two_of_two_eq_two uses the same monotone spine to show that a degenerate trace at two forces the trace to equal two at every positive integer.
In the Recognition cost story this supports uniqueness and factorization of the native cost (the J-cost lineage, T5/RCL) once the doubled trace is displayed on rationals: monotone integer samples pin the growth of the real character before the continuous or ladder-level statements. It is local scaffolding inside RealCharacterFactorization, not a forcing-chain landmark itself, but it is required for the nondegenerate character path that feeds cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.