rationalTrace_pos_eq_two_of_two_eq_two
plain-language theorem explainer
If an anchor-free native cost map has doubled rational trace equal to 2 at the integer 2, then that trace equals 2 at every positive rational. Gauge-orbit and real-character arguments cite this to identify the degenerate (flat) cost with the pure sign gauge. The proof reduces a positive rational to a numerator/denominator pair, applies the rational d'Alembert identity, and feeds the three natural-number evaluations already known to be 2.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost package (base without fixing two, sign-reversing, monotone, zero-calibrated doubled trace). Write $T_F(x)$ for the doubled trace of $F$ evaluated on the rational display $x\in\mathbb{Q}$. If $T_F(2)=2$, then $T_F(x)=2$ for every rational $x>0$.
background
In the real-character factorization module, native costs act on ratio orbits. The doubled trace of such a map, pushed to rational displays, is the function rationalTrace: for $x\in\mathbb{Q}$ one forms the orbit of $x$ and reads the real trace display. The structure SansAnchorHypotheses packages the anchor-free axioms matching the PRC structural native-cost hypotheses without fixing the value at two: a base law, sign-reversal, monotonicity, and zero-calibration of the doubled trace.
Under those hypotheses the rational trace obeys a d'Alembert (cosine-type) identity $T_F(xy)+T_F(x/y)=T_F(x),T_F(y)$ for nonzero rationals $x,y$. A prior lemma already upgrades the single normalization $T_F(2)=2$ to $T_F(n)=2$ for every natural number $n\ge 1$, by a power-of-two squeeze that uses monotonicity and complete multiplicativity on naturals.
The present statement extends that natural-number rigidity to every positive rational, which is the display language used by gauge-orbit classification and by the assembled real character.
proof idea
Write a positive rational $x$ as $a/b$ with $a=x.\mathrm{num}.\mathrm{toNat}\ge 1$ and $b=x.\mathrm{den}\ge 1$, so $x=a/b$ in $\mathbb{Q}$. Apply the rational d'Alembert identity at this pair: $T_F(a\cdot b)+T_F(a/b)=T_F(a),T_F(b)$. The three natural arguments $a$, $b$, and $a\cdot b$ are each at least 1, so the natural-number rigidity lemma gives $T_F(a)=T_F(b)=T_F(ab)=2$. Substituting and using $a/b=x$ yields $2+T_F(x)=4$, hence $T_F(x)=2$ by linear arithmetic.
why it matters
This is the rational half of the degenerate-anchor dichotomy in Recognition cost theory. Downstream, degenerate_is_signGauge quotes it to prove that if the trace at two is two then the cost agrees with the pure sign gauge on every orbit: the trace is constantly two on positive displays, the cost vanishes there, and orientation reversal fills the negatives. Likewise vanishes_at_two_iff_flat uses it to turn "free at orbit two" into "free at every positive ratio," the slogan that charging nothing at one point charges nothing anywhere.
Inside the same module it feeds realCharacterCandidate_trace_of_pos, which reconstructs the doubled trace from a real character candidate on positive orbits. In the broader forcing picture this sits on the cost side of the J-uniqueness chain (T5): the only non-degenerate continuous solutions of the Recognition Composition Law are the hyperbolic J-costs; the degenerate branch is exactly the flat/sign character isolated here. No scaffolding remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.