doubledTrace_character_rigid
plain-language theorem explainer
On a calibration point, the doubled d'Alembert trace of the cost generated by a PRC ratio character matches the doubled trace of the canonical orbit cost. Continuum character-rigidity and cost-uniqueness arguments cite this packaging step. The proof is a one-line congruence wrapper around the already-proved cost-from-character rigidity lemma.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits, and let $p$ be a ratio orbit at which $\chi$ is calibrated (i.e. $\chi(p)$ is cross-equivalent to $p$). Then the doubled d'Alembert traces $2(F+1)$ of the cost generated by $\chi$ at $p$ and of the canonical PRC cost on the orbit of $p$ are cross-equivalent.
background
In the Primitive Recognition Calculus continuum layer, multiplicative characters act on ratio orbits. A PRC ratio character $\chi$ is such a multiplicative map. Calibration at an orbit direction $q$ means $\chi$ acts as the identity there: $\chi(q)$ is cross-equivalent to $q$. The module notes that calibration at two is the single-point datum the PRC cost hypotheses typically carry.
From a character one builds a generated cost and compares it to the canonical PRC J-cost on the ratio orbit. The doubled d'Alembert trace $2(F+1)$ is the natural display of that cost for rigidity statements; it is the doubled form of the unique J-cost fixed by the Recognition Composition Law. Upstream cost-uniqueness and functional-equation material pin that canonical shape; this lemma only transports an already-proved cost match into the doubled-trace display.
proof idea
One-line term proof. Apply congruence of the doubled-trace display to costFromCharacter_rigid at the same hypotheses (PRC character and calibration at $p$). That sibling forces the generated cost itself to be cross-equivalent to the canonical orbit cost; the doubled-trace values inherit the match by congruence, with no extra arithmetic.
why it matters
Sits in CharacterRigidityForcing under the PRC continuum stack. It lifts cost-level calibrated rigidity into the doubled d'Alembert trace language used for J-cost displays. The module headline (calibrated character-rigidity on a single prime direction) uses the same hypotheses to force the character to stay the identity on $p\cdot p$ and $p^{-1}$ (hence on the cyclic subgroup $p$ generates) and to force the generated cost to the canonical orbit cost. That is exactly the local rigidity calibrated multiplicativity supplies; the global all-primes step is deferred to separate target_* results.
Framework landmark: supports T5 J-uniqueness, since a calibrated character cannot drift the generated cost away from $J(x)=(x+x^{-1})/2-1$. No downstream consumers are wired yet, so this is presently a leaf packaging lemma in the continuum forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.