PRCDoubledTraceZeroCalibratedLinearRootTarget_proved
plain-language theorem explainer
Any doubled-trace map on ratio orbits that meets the native doubled-trace hypotheses and is zero-calibrated admits a working linear root candidate: the candidate is a ratio character (unit, multiplicative, reciprocal, normalized, nonzero-preserving) and recovers the doubled trace. Cost-uniqueness arguments in the primitive recognition calculus cite this step. The proof assembles prior respect, quadratic, and root-candidate lemmas into one constructor.
Claim. For every map $T$ from ratio orbits to ratio orbits: if $T$ satisfies the doubled-trace hypotheses and is zero-calibrated (vanishes on the unit orbit), then the linear root candidate built from $T$ works. Explicitly, that candidate is a ratio character (preserves the unit, is multiplicative and reciprocal, is normalized-invariant, and preserves nonzeroness) and its doubled trace recovers $T$.
background
In the primitive recognition calculus, cost data on positive ratios is packaged through ratio orbits and characters. A ratio character is a map on orbits that preserves the multiplicative unit, multiplies under orbit product, inverts under reciprocal, stays normalized under the native invariant, and never sends a nonzero orbit to zero. The native $J$-cost (the unique continuous solution of the recognition composition law, $J(x)=(x+x^{-1})/2-1$) is recovered from such characters via a doubled-trace construction: evaluate a character on an orbit and its reciprocal and combine.
The local target packages three layers. Doubled-trace hypotheses on a map $T$ encode the structural constraints needed before a root can be extracted (including d'Alembert-type identities already proved for native cost). Zero-calibration means $T$ vanishes on the unit orbit. The linear root candidate is the algebraic square-root extraction along the doubled trace; "works" means it is a genuine ratio character whose doubled trace equals $T$.
Upstream cost algebra supplies the multiplicative and reciprocal laws for $J$-automorphisms; orbit divisibility isolates the native unit as the one-step orbit. Those facts feed the root-candidate lemmas used here.
proof idea
Term-mode proof by introduction on $T$, the doubled-trace hypotheses, and zero-calibration. First obtain that $T$ respects the cross-equality relation from the hypotheses (PRCDoubledTraceRespectsCrossEq_proved). From respect, deduce that the linear root candidate is quadratic (traceRootCandidate_quadratic_of_trace_respect).
The goal is a pair. The first component is a ratio-character package for the root candidate: unit and multiplicativity from respect; reciprocity and nonzero-preservation from the quadratic law; normalized invariance again from respect. The second component is recovery of the doubled trace from the candidate, using zero-calibration together with the quadratic identity (traceRootCandidate_trace_of_quadratic). No new analytic work: pure assembly of prior root-candidate lemmas.
why it matters
Native cost uniqueness in PRC needs a bridge from abstract doubled-trace data back to a concrete ratio character. This theorem closes that bridge under zero-calibration: once $T$ is hypothesized and vanishes at the unit, the linear root is already a working character matching $T$.
The sole direct consumer is PRCDoubledTraceZeroCalibratedCoherentRootTarget_proved, which lifts the linear-root conclusion to the coherent-root target by a one-line reduction. That coherent step is the next gate toward identifying the native doubled-trace cost with the unique $J$-cost forced by the recognition composition law (forcing-chain T5: $J(x)=\cosh(\log x)-1$).
In framework terms this is ledger-side uniqueness infrastructure, not a spacetime or constants result. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only secures the algebraic root extraction that those later uniqueness arguments rely on when cost is presented as a doubled trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.