character_trace_rigid
plain-language theorem explainer
On a calibration point, the d'Alembert trace of a ratio character collapses to the identity trace: χ(p)+χ(p)⁻¹ is cross-equivalent to p+p⁻¹. Anyone deriving PRC cost uniqueness from character data cites this local rigidity step. The proof is a short rational-display calculation: calibration gives χ(p)~p, and add/recip commute with the toRat display.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $\chi$ is calibrated at an orbit $p$ (i.e. $\chi(p)$ is cross-equivalent to $p$), then the d'Alembert traces agree on that point: $\chi(p)+\chi(p)^{-1}$ is cross-equivalent to $p+p^{-1}$.
background
In the Primitive Recognition Calculus continuum layer, multiplicative structure lives on ratio orbits. A PRC ratio character is a multiplicative map $\chi$ on those orbits. Cross-equivalence identifies orbits that share the same positive-rational display (via toRat).
Calibration at $p$ means $\chi$ acts as the identity character on that orbit direction: $\chi(p)\sim p$. The module records that calibration at two is the single-point datum the PRC cost hypotheses actually carry.
The d'Alembert (Chebyshev) trace $x+x^{-1}$ is the natural invariant of a multiplicative character and the algebraic skeleton of the RS cost: T5 forces $J(x)=(x+x^{-1})/2-1$. Matching traces at a calibration point is the first rigidity step from character data toward that unique $J$.
proof idea
Unfold the calibration hypothesis to crossEq (χ p) p. Rewrite both hypothesis and goal through the iff that turns cross-equivalence into equality of rational displays. Expand the rational displays of sum and reciprocal on both sides (add_toRat, recip_toRat). The calibration equality then makes the two traces identical as rationals. The ambient PRCRatioCharacter package is in the signature for context but is not used in the rewrite chain; the argument is pure display algebra from calibration.
why it matters
Local character-trace rigidity inside CharacterRigidityForcing. Calibrated characters cannot twist the d'Alembert trace at the calibration point. Immediate siblings push the same idea further: costFromCharacter_rigid forces the character-generated cost to equal the canonical PRC $J$-cost on the orbit at that point, and doubledTrace_character_rigid is the parallel doubled-trace form.
In the RS forcing chain, T5 uniqueness of $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the cost landmark compatible with the Recognition Composition Law. Trace rigidity is how that uniqueness descends from abstract multiplicative character data to continuum PRC cost. No recorded downstream consumers yet; the lemma is infrastructure for cost-from-character uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.