le_of_trace_le
plain-language theorem explainer
On [1, ∞), the map v ↦ v + v⁻¹ is strictly increasing, so a ≤ b whenever the traces satisfy a + a⁻¹ ≤ b + b⁻¹. Classification of gauge-orbit costs cites it to convert ledger monotonicity on costs into monotonicity of the extracted character on positive integers. The proof is a short contradiction via an algebraic identity for the trace difference.
Claim. For real numbers $a,b \ge 1$, if $a + a^{-1} \le b + b^{-1}$, then $a \le b$. Equivalently, $v \mapsto v + v^{-1}$ is strictly increasing on $[1,\infty)$.
background
In the gauge-orbit cost module, principal values of ratio orbits are read through the real trace $v \mapsto v + v^{-1}$. That expression is the unnormalized form of the Recognition Science J-cost $J(x) = (x + x^{-1})/2 - 1$ (T5 uniqueness), so inequalities on traces are inequalities on costs up to affine rescaling.
The local setting classifies multiplicative characters on ratio orbits under ledger hypotheses (SansAnchorHypotheses). Monotonicity is stated on costs; to feed Erdős-type uniqueness for completely multiplicative monotone maps on $\mathbb{N}$, one must recover ordinary order on the positive principal values themselves.
Upstream cost definitions (observer forcing, multiplicative recognizer, rung coarsening) all route through J-cost or a derived comparator cost. This lemma is the elementary real-analysis bridge that turns those cost inequalities into value inequalities on $[1,\infty)$.
proof idea
Proof by contradiction. Assume $a > b$ with $a,b \ge 1$. Positivity $a,b > 0$ is immediate from $1 \le a,b$. The key algebraic identity
$(a + a^{-1}) - (b + b^{-1}) = (a-b)(ab-1)/(ab)$
is obtained by field_simp and ring. Both factors $a-b$ and $ab-1$ are strictly positive ($ab \ge a \cdot 1 \ge 1$, and strict because $b \ge 1$ and $a > b$), and the denominator $ab > 0$, so the right-hand side is positive. Rewriting yields a strictly positive trace difference, contradicting the hypothesis. Finish with linarith.
why it matters
This is the monotonicity transfer step inside Cost.GaugeOrbitClassification. Downstream, natChar_monotoneMultiplicative quotes it explicitly: complete multiplicativity comes from character extraction, while monotonicity is the ledger's, read through this lemma, so the restricted character meets the hypotheses of Erdős's theorem on monotone completely multiplicative functions.
It also supports degenerate_is_signGauge, which identifies the flat (trace-two-at-two) anchor with the pure sign cost. Together these close the dichotomy between the degenerate sign gauge and the nontrivial signed-power characters on ratio orbits.
Framework-wise, the trace is the raw form of the T5 J-cost. Converting cost order into value order is what lets the Recognition Composition Law and ledger monotonicity force the discrete character classification used later for mass-ladder and gauge structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.