doubledTraceValue_congr
plain-language theorem explainer
Cross-equivalence of ratio orbits is preserved by the doubled-trace map a ↦ 2(a+1). Cost-uniqueness and character-rigidity arguments cite it whenever they transport the native d'Alembert trace across rational displays. The proof rewrites cross-equivalence to rational equality, unfolds the orbit arithmetic, and finishes by linear arithmetic.
Claim. If ratio orbits $a$ and $b$ are cross-equivalent (equivalently, $a$ and $b$ display the same rational), then the doubled traces $2(a+1)$ and $2(b+1)$ are likewise cross-equivalent.
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer numerator over a nonzero orbit denominator: the internal display of a rational built only from δ-orbit positions. Two such displays are related by crossEq when cross-multiplication balances as signed orbits; by K4.10 this is equivalent to equality of the verifier rationals toRat.
The doubled-trace value is the native map $a \mapsto 2(a+1)$ on ratio orbits. The module treats this as the RCL (Recognition Composition Law) equation after the change of unknown $T_F = 2(F+1)$, so congruence lemmas for the doubled trace are the bookkeeping step that lets cost and character statements pass between equivalent rational displays.
Upstream, crossEq_iff_toRat_eq identifies the internal relation with rational equality, and the *_toRat lemmas (add_toRat, mul_toRat, one_toRat, two_toRat) say that orbit arithmetic matches field arithmetic on the verifier.
proof idea
Tactic proof. Rewrite the hypothesis and goal with crossEq_iff_toRat_eq, so both sides become equalities of rationals. Unfold doubledTraceValue and simplify with the orbit-to-rational lemmas (mul_toRat, add_toRat, two_toRat, one_toRat), reducing the claim to an identity in $\mathbb{Q}$. Close with linarith.
why it matters
This is the congruence hinge for the native doubled-trace package in PRC cost uniqueness. Downstream, traceDisplay_eq_of_crossEq and traceDisplay_recip in RealCharacterFactorization apply it to show the real trace display is well-defined on cross-classes and reciprocal-invariant. In Continuum.CharacterRigidityForcing, doubledTrace_character_rigid uses it to rigidify $2(F+1)$ of a generated cost to the canonical doubled trace at a calibration point.
Inside the same module it feeds nativeCostDoubledTrace_hypotheses_of_native_cost_hypotheses and zeroSpikeDoubledTrace_hypotheses, which package reciprocal, normalization, and d'Alembert data for the doubled-trace form of native cost. Framework-wise it sits under the RCL after $T_F = 2(F+1)$, the algebraic skeleton behind T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.