PRCPrimeCalibrationForcesPrimeIdentityCanonicalAddTraceTarget
plain-language theorem explainer
The canonical-add-trace target packages the claim that every prime-calibrated ratio character must transport identity orientation through the concrete finite common extension given by the orbit-position trace of a sum of two primes. Native-cost uniqueness work cites it as one of the exact Prop targets into which the remaining gap is split. Downstream iff lemmas equate it with branch-uniformity, common-trace-extension, and trace-transport formulations. As a bare Prop definition it carries no proof content.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character (unit at one, multiplicative up to cross-equivalence) and is prime-direction calibrated (its induced cost agrees with canonical $J$-cost on every prime orbit), the identity orientation of $\chi$ respects the canonical add-trace: whenever prime axes $p$ and $r$ both extend into $\mathrm{orbitPositionTrace}(p+r)$, identity orientation transports through that finite common extension.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer-numerator display over a nonzero distinction-nat denominator. A ratio character $\chi$ is a candidate d'Alembert factor at that level: it fixes the unit orbit up to cross-equivalence and is multiplicative under orbit multiplication, again up to cross-equivalence rather than definitional equality, so the notion stays quotient-native.
Prime-direction calibration asks that the cost generated from $\chi$ agree, via cross-equivalence, with the canonical $J$-cost on every prime orbit. The identity event of ObserverForcing sits at the $J$-cost minimum $x=1$ and has zero cost; identity orientation is the character's action relative to that anchor.
The canonical-add-trace predicate sharpens earlier common-trace transport: instead of an arbitrary witness, it demands that identity orientation transport through the specific finite merger $\mathrm{orbitPositionTrace}(p+r)$ of two prime axes, whenever both axes extend into that sum. This module sits inside the native-cost uniqueness program that aims to force the unique $J$-cost of the Recognition Composition Law.
proof idea
Pure Prop packaging: the definition is the universal quantification over maps $\chi$ of the implication from ratio-character plus prime-direction calibration to the canonical-add-trace respect predicate. No tactics, no lemmas applied, no term construction beyond assembling those three named hypotheses into one target statement.
why it matters
This target is one of the exact Lean blockers recorded by the Pass-25 native-cost uniqueness certificate: uniqueness is not closed, but the missing mathematics is split into named Prop goals of which this is the canonical-add-trace form. Downstream, it is proved equivalent to the branch-uniformity target, the common-trace-extension target, and the trace-transport target, so any one of those formulations discharges the others. Those equivalences feed the certificate and the surrounding prime-identity forcing lemmas.
In the broader Recognition chain this sits under T5 $J$-uniqueness: forcing every admissible character that matches $J$ on primes to respect identity transport through finite $\delta$-orbit mergers is a step toward showing no exotic factorization of the native cost survives. Closing the target would remove one remaining degree of freedom in the character before the full uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.