PRCNativeCostCharacterFactorizationTarget_of_doubled_trace_zero_calibrated
plain-language theorem explainer
If every PRC-native cost forces its generated doubled trace to vanish on the zero orbit, then every admissible native RCL cost factors through a ratio character. Foundation workers closing the discrete d'Alembert uniqueness path for native costs cite this. The proof is a two-step term composition: lift the zero-orbit calibration hypothesis to a character-trace-lift target, then apply the factorization-from-trace-lift lemma.
Claim. Assume that for every map $F$ from ratio orbits to ratio orbits satisfying the native cost hypotheses, the doubled trace built from $F$ is zero-calibrated (vanishes on the zero orbit). Then for every such $F$ there exists a ratio character $\chi$ such that $F(q)$ is cross-equal to the cost reconstructed from $\chi$ at every orbit $q$.
background
In the Primitive Recognition Calculus, admissible native costs are maps $F$ on ratio orbits obeying the Recognition Composition Law (RCL) interface, quantified only over nonzero inputs. The first exact uniqueness blocker is character factorization: every such $F$ should arise as $\mathrm{costFromCharacter}(\chi)$ for some ratio character $\chi$. That is the discrete d'Alembert factorization step toward identifying the native cost with the classical $J$-cost $J(x)=(x+x^{-1})/2-1$.
A parallel construction builds a doubled trace from $F$. After the coherent-root theorem, the remaining zero-orbit obstruction is that native cost hypotheses must force this doubled trace to vanish at the zero orbit (zero-calibrated). The present target packages that obstruction as a single proposition, and the character-factorization target packages the desired factorization conclusion.
The module sits in the Foundation forcing chain that aims at T5 $J$-uniqueness. RCL only constrains nonzero ratios, so zero-orbit calibration is a separate, exact interface condition rather than a consequence of RCL alone.
proof idea
Pure term-mode composition of two already-proved bridges. First apply the lemma that turns the doubled-trace zero-calibration target into the character-trace-lift target (native cost hypotheses imply the doubled trace matches a character on the nonzero part and is calibrated at zero). Then feed that lift into the lemma that any cost admitting a character-trace lift factors through a ratio character in the cross-equality sense. No new algebra is done here; the declaration only chains the two reductions.
why it matters
Character factorization is documented as the first exact blocker on the PRC-native RCL uniqueness path: once every admissible native cost factors through a ratio character, the discrete d'Alembert analysis can force that character (and thus the cost) to the classical $J$ shape from T5. This theorem collapses that blocker to the single remaining zero-orbit calibration hypothesis on the doubled trace.
No downstream consumers are wired yet (used_by is empty), so the declaration is a leaf in the current graph: it records that factorization is no harder than zero-calibration. In the broader Recognition chain it sits under the Foundation push toward unique native cost, which feeds the forcing landmarks T5 (unique $J$), T6 ($\phi$ as self-similar fixed point), and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Closing the zero-calibration hypothesis would discharge this target and advance native-cost uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.