zeroFlatNativeCost_no_character_trace
plain-language theorem explainer
There is no ratio-orbit character whose d'Alembert trace reproduces the zero-flat native cost. Anyone ruling out character-factorized native costs cites this. The proof evaluates the putative character at the zero and two orbits, forces both values to 1 by reciprocity and multiplicativity, then obtains 2 = 5/2 from the doubled-trace identity at two.
Claim. There do not exist a map $\chi$ from ratio orbits to ratio orbits that is a ratio character (unit-preserving, multiplicative, and reciprocal up to cross-equivalence) and whose doubled character trace matches the zero-flat native cost: for every orbit $q$, $\chi(q)+\chi(q)^{-1}$ is cross-equivalent to twice that cost plus two.
background
In the Primitive Recognition Calculus, costs live on ratio orbits rather than bare positives. Cross-equivalence is the internal rational relation: two orbits match when cross-multiplication of numerators and denominators balances as signed orbits, equivalently when their rational displays agree.
A ratio character $\chi$ is a quotient-native candidate for d'Alembert factorization of a PRC cost: it sends the unit orbit to itself, multiplies under orbit multiplication, and intertwines reciprocal, all up to cross-equivalence. The matching condition PRCCharacterTraceMatchesCost asks that the generated trace $\chi(q)+\chi(q)^{-1}$ equal the native doubled trace $2(F(q)+1)$ of the cost $F$.
The zero-flat native cost is the distinguished flat cost under study in this uniqueness module. The theorem says that cost admits no such character factorization.
proof idea
Assume a character $\chi$ whose trace matches the zero-flat cost. Set $a=(\chi,0)^{\mathbb{Q}}$ and $b=(\chi,2)^{\mathbb{Q}}$. Reciprocity at zero plus the trace identity at zero give $a=a^{-1}$ and $a+a^{-1}=2$, so $a=1$ by linear arithmetic.
Cross-equivalence respect (from the proved normalize-ratio canonical target) and multiplicativity at $(0,2)$ force $\chi(0\cdot 2)$ to display both as $a$ and as $a\cdot b$, hence $b=1$. The matching condition at the two-orbit, rewritten through the nonzero cross-equivalence of the zero-flat cost with the on-orbit cost, yields $b+b^{-1}=5/2$. Substituting $b=1$ produces $2=5/2$, contradiction.
why it matters
This is the concrete obstruction that discharges the character-trace lift target for native costs. The sole downstream consumer is PRCNativeCostCharacterTraceLiftTarget_refuted, which applies the present theorem at the zero-flat cost and its native hypotheses to refute existence of any native cost admitting a character-trace factorization.
In the Recognition forcing picture, native costs are meant to be unique up to the J-cost shape forced at T5 ($J(x)=(x+x^{-1})/2-1$). Ruling out a free character factor $\chi$ with $F=J\circ\chi$ keeps the cost rigid: the d'Alembert factorization cannot hide an extra multiplicative character on ratio orbits. That rigidity feeds the uniqueness thread of the primitive recognition calculus and, upstream of the global chain, protects the identification of the physical cost with the forced $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.