PRCPrimeCalibrationForcesPrimeIdentityTraceTransportTarget
plain-language theorem explainer
Packages the smaller trace-transport obligation: any ratio character calibrated on native prime directions must keep identity orientation invariant along prime-axis δ-trace connections. Cited by anyone closing native cost uniqueness or relating transport, coherence, and canonical-add-trace targets. Pure Prop definition; no proof beyond the quantified implication.
Claim. For every map $\chi$ from ratio orbits to ratio orbits, if $\chi$ is a ratio character and is calibrated on every native prime direction (its generated cost matches canonical $J$-cost on each prime orbit), then $\chi$ respects identity orientation along every finite $\delta$-trace connection between prime axes.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: integer numerator over a nonzero orbit denominator, compared by cross-equivalence rather than definitional equality. A ratio character $\chi$ is a candidate factor for the d'Alembert factorization of a native cost: it fixes the unit orbit and is multiplicative up to cross-equivalence.
Prime-direction calibration asks that the cost generated from $\chi$ agree with the canonical $J$-cost on every prime orbit. Separately, identity orientation (the character fixing a prime direction) is required to transport along the finite $\delta$-trace component that already connects any two prime axes; that connectivity is proved upstream.
This module isolates exact Lean targets for the remaining uniqueness gap. The present definition is the smaller transport form of the prime-calibration obligation.
proof idea
Definitional packaging only. The body is the universal implication $\forall,\chi,;\mathrm{RatioCharacter}(\chi)\to\mathrm{PrimeCalibrated}(\chi)\to\mathrm{RespectsTraceConnected}(\chi)$. No tactics, no lemmas applied; downstream theorems treat the name as a single Prop hypothesis and unfold or rewrite against equivalent targets.
why it matters
Native cost uniqueness is not closed; the Pass-25 blocker certificate splits the missing mathematics into named targets, and this is the smaller trace-transport one. Downstream, it is proved equivalent to the canonical-add-trace target and to the trace-coherence target (via mutual of_ constructors and iff theorems). Those equivalences let any one form discharge the others when building the uniqueness certificate.
In the broader Recognition chain this sits under J-uniqueness (T5) and the Recognition Composition Law: characters that match $J$ on primes and preserve identity along the prime-axis trace graph are the candidates that can force the native cost to be the unique d'Alembert factor. Closing this target would remove one blocker on uniqueness of the PRC native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.