zeroFlatNativeCost_doubled_trace_zero
plain-language theorem explainer
At the zero ratio orbit, the doubled d'Alembert trace of the zero-flat native cost equals the doubled-trace value of zero itself. Anyone ruling out zero-calibration for this cost cites the identity. The proof is a two-rewrite wrapper: unfold the doubled-trace carrier, then apply the fact that the zero-flat cost vanishes at zero.
Claim. Let $F$ be the zero-flat native cost on ratio orbits (canonical off zero, flattened to $0$ at the zero orbit). Then the doubled d'Alembert trace $T_F(q)=2(F(q)+1)$ satisfies $T_F(0)=2(0+1)$, i.e. $T_F$ at the zero orbit equals the doubled-trace value attached to the zero orbit.
background
In the Primitive Recognition Calculus, costs act on ratio orbits: integer-numerator displays over nonzero orbit denominators. The doubled d'Alembert trace of a cost $F$ is $T_F(q)=2(F(q)+1)$; for a character-generated cost this recovers $\chi(q)+\chi(q)^{-1}$.
The zero-flat native cost is the canonical native cost on every nonzero orbit, forced to $0$ at the zero orbit (and also at the unit orbit). It still meets the native cost interface because the Recognition Composition Law only quantifies over nonzero inputs. A prior lemma records that this cost evaluates to the zero orbit at the zero orbit.
The local module develops uniqueness and calibration constraints for native costs via their doubled traces, including d'Alembert-type functional equations and zero-calibration predicates.
proof idea
One-line rewrite wrapper. Unfold nativeCostDoubledTrace to expose doubledTraceValue (F q) at $q=0$, then rewrite with the lemma that the zero-flat cost at the zero orbit is the zero orbit. The two sides become identical.
why it matters
Feeds the immediate parent that the doubled trace of the zero-flat native cost is not zero-calibrated: after this identity, evaluating $2(0+1)$ at the zero orbit yields a nonzero rational, so the calibration predicate fails.
That negative result is part of the native-cost uniqueness campaign in PRC: among candidates satisfying the RCL-style interface, only the genuine $J$-cost (T5 uniqueness: $J(x)=(x+x^{-1})/2-1$) can carry a properly calibrated doubled trace. Flattening at zero is a natural counter-model that still obeys the nonzero RCL quantifiers, so one must pin down calibration at zero separately. This lemma is the algebraic hinge that turns the flattening definition into a concrete calibration failure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.