PRCPrimeCalibrationForcesPrimeIdentityCommonTraceExtensionTarget
plain-language theorem explainer
Names the open target that every ratio-orbit character which is multiplicative and prime-direction calibrated must transport identity orientation through any finite common δ-trace extension of two prime axes. Cost-uniqueness and blocker-certificate work cite it as the sharper trace-transport obligation. The body is a pure Prop abbreviation packing three named hypotheses into one universal statement.
Claim. Every map $\chi$ on ratio orbits that is a ratio character (unit-preserving and multiplicative up to cross-equivalence) and whose generated cost matches canonical $J$-cost on every prime direction must respect common finite $\delta$-trace extension: whenever two prime-axis position traces embed in one finite trace $T$, identity orientation is transported under $\chi$ along that shared extension.
background
In the primitive recognition calculus, costs factor through ratio-orbit characters. A ratio orbit is an integer numerator over a nonzero distinction-orbit denominator. A ratio character $\chi$ is unit at the identity orbit and multiplicative up to cross-equivalence, so the construction stays quotient-native rather than forcing definitional equality.
Prime-direction calibration asks that the cost built from $\chi$ agree with the canonical $J$-cost on every prime orbit direction. The identity event sits at the $J$-cost minimum $x=1$. Native traces are built by recursion on distinction naturals via orbitPositionTrace, not by importing external $\mathbb{N}$ as object theory.
The common-trace-extension rule is the explicit transport law: if two prime-axis traces both extend into one finite $\delta$-trace $T$, identity orientation must transport under $\chi$. This definition packages that obligation as a single target Prop under character and calibration hypotheses.
proof idea
No proof: the declaration is a definitional Prop. It universally quantifies over maps $\chi$ on ratio orbits, assumes the ratio-character structure and prime-direction calibration, and concludes the common-trace-extension respect predicate. Downstream lemmas treat the name as a black-box hypothesis or unfold it with intro.
why it matters
This is the sharper trace-transport target in the native cost uniqueness program: prime calibration must force identity orientation through an explicitly witnessed common finite $\delta$-trace extension. It sits in the equivalence web with the canonical-add-trace target (iff and both directions of implication are proved) and is implied by the comparable-trace and trace-coherence targets.
The Pass-25 blocker certificate splits unfinished uniqueness mathematics into exact Lean targets; this name is one of those obligations. Closing it would advance the d'Alembert factorization route to uniqueness of the native cost, which feeds the broader forcing story around $J$-uniqueness (T5) and the recognition composition law. A refuted sibling already records that some stronger packings fail, so this formulation is the live cut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.