nativeCostDoubledTrace_hypotheses_of_native_cost_hypotheses
plain-language theorem explainer
Native PRC cost hypotheses on a map F transfer to the doubled-trace package on T(q)=2(F(q)+1). Anyone building the character factorization F=J∘χ via a d'Alembert lift cites this bridge. The proof is a structure constructor: four fields push through doubled-trace congruence, and d'Alembert is the dedicated sibling lemma.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the native PRC cost package (reciprocity, normalization invariance, unit zero, two-calibration, and the native d'Alembert law). Then the doubled trace $T(q)=2\bigl(F(q)+1\bigr)$ satisfies the doubled-trace hypotheses: $T(q)\sim T(q^{-1})$, $T$ is invariant under ratio normalization, $T$ obeys the doubled-trace d'Alembert identity, $T(1)=2$, and the two-point calibration holds.
background
In the Primitive Recognition Calculus, costs live on ratio orbits (cross-multiplication classes of integer ratios). The native cost package on $F$ encodes the Recognition Composition Law at the orbit level: reciprocity under $q\mapsto q^{-1}$, invariance under distinction-normal form, vanishing at the unit orbit, a fixed calibration at the orbit of two, and a d'Alembert-type functional equation.
The doubled trace is the orbit-level avatar of $T=2(F+1)$. That shift is exactly the bridge from a J-style cost (with $J(1)=0$) to a Chebyshev/cosh-type character whose generated trace is $2\cosh$. Cross-equality of orbits is equivalent to equality of their rational displays (crossEq_iff_toRat_eq), so orbit identities can be checked after toRat.
This module isolates uniqueness of the native cost by lifting $F$ to a doubled-trace object and then recovering a character root. The present theorem is the pure hypothesis-transport step in that lift.
proof idea
Term-mode refine builds PRCDoubledTraceHypotheses fieldwise.
- Reciprocal and normalized-invariant: apply
doubledTraceValue_congrto the corresponding native fields ofhF. - d'Alembert: one-line call to the sibling
nativeCostDoubledTrace_dAlembert_of_native_hypotheses hF. - Unit trace: rewrite via
crossEq_iff_toRat_eq, unfoldnativeCostDoubledTrace/doubledTraceValue, inserthF.unit_zero, push throughmul_toRat/add_toRat/zero_toRat/one_toRat/two_toRat, finish withnorm_num(checks $2(0+1)=2$). - Two-trace:
doubledTraceValue_congronhF.two_calibrated.
why it matters
This is the gate from native cost axioms to the doubled-trace d'Alembert package used in character factorization. Downstream, PRCNativeCostCharacterTraceLiftTarget_of_doubled_trace_coherent_root and ..._of_doubled_trace_zero_calibrated both open with this transfer, then invoke a coherent-root or zero-calibrated target on $T$. The proved zero-calibrated lift PRCZeroCalibratedNativeCostCharacterTraceLiftTarget_proved does the same.
In framework terms this is the orbit-level form of the T5 J-uniqueness story: the hidden identity inside $F=J\circ\chi$ is that the generated trace of $\chi(q)$ equals $2(F(q)+1)$, which is exactly the doubled-trace object constructed here. Without hypothesis transport, the uniqueness chain cannot leave the native $F$-language and enter the character/root language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.