rationalTrace_neg
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the rational doubled-trace display is an odd function of its rational argument: flipping the sign of x flips the sign of the displayed cost. Anyone building real characters or oddness lemmas for the PRC cost on Q will cite this. The proof applies the pack's sign-reversing axiom on ratio orbits, then reduces the display algebra with toRat lemmas and finishes by linear arithmetic.
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). Then for every rational $x\in\mathbb{Q}$, the rational doubled-trace display obeys $\mathrm{Tr}_F(-x)=-\mathrm{Tr}_F(x)$.
background
This module factors the real character of the primitive recognition cost through ratio orbits and their rational displays. A ratio orbit is the signed rational carrier used by the PRC integer-rational layer; toRat recovers the underlying rational, with addition and multiplication commuting with that forgetful map (add_toRat, mul_toRat, one_toRat).
SansAnchorHypotheses is the anchor-free pack matching the structural native-cost hypotheses: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Sign-reversing is the key structural input here: the native cost flips sign when its orbit argument is replaced by the opposite orbit.
rationalTrace F x is defined as the real display of the carrier-valued doubled trace on the ratio orbit of $x$. Concretely, traceDisplay casts (nativeCostDoubledTrace F q).toRat to $\mathbb{R}$. The theorem lifts orbit-level oddness to this honest function on rational displays.
proof idea
Instantiate the pack's sign_reversing field on the pair of orbits ratioOrbitOfRat x and ratioOrbitOfRat (-x), using that their toRat images are $x$ and $-x$. Unfold rationalTrace, traceDisplay, and the doubled-trace value into the underlying ratio-orbit arithmetic. Simplify with mul_toRat, add_toRat, ratioOrbitOfRat_toRat, two_toRat, and one_toRat, then norm_cast and close the resulting real equality by linarith against the sign-reversing identity.
why it matters
Oddness of the rational trace is the first algebraic character property needed once the doubled trace is displayed on $\mathbb{Q}$. In Recognition Science the native cost is built from the unique $J$-cost forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$), which is even in the multiplicative coordinate and yields an odd additive defect after the usual log change of variables. Establishing $\mathrm{Tr}_F(-x)=-\mathrm{Tr}_F(x)$ under the anchor-free pack keeps that parity intact at the rational-display layer used by real-character factorization.
No downstream users are wired yet in the graph (used_by is empty), so this is currently a leaf lemma inside Cost.RealCharacterFactorization, sitting beside the d'Alembert identities for the doubled trace and the real-ratio character constructors. It is the natural parity step before extending the character from $\mathbb{Q}$ toward the full real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.