Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_iff_trace_coherence

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
domain
Foundation
line
9718 · github
papers citing
none yet

plain-language theorem explainer

Prime-calibration branch-uniformity and prime-calibration trace-coherence are equivalent targets: each holds for all ratio characters exactly when the other does. Anyone tracking the remaining native-cost uniqueness blockers cites this to collapse the two formulations. The proof is a two-constructor Iff built from the already-proved one-way implications.

Claim. The following are equivalent: (i) every ratio character that is prime-direction calibrated is identity-branch uniform on native prime axes; (ii) every such character is identity-trace coherent across prime axes. In other words, the branch-uniformity target forced by prime calibration is logically equivalent to the trace-coherence target forced by prime calibration.

background

In the Primitive Recognition Calculus, a ratio character $\chi$ is a map on ratio orbits that encodes how cost or orientation is assigned along multiplicative structure. Prime-direction calibration means $\chi$ has been fixed so that native prime axes point in a preferred (identity) direction. Two residual targets remain for uniqueness arguments.

The branch-uniformity target asks that, once any identity-oriented native prime axis is present, every native prime axis sits on the identity branch. The trace-coherence target asks the weaker-looking structural demand that identity orientation propagate along the already-proved connectivity of the prime-axis trace graph.

Both targets are quantified over the same class: ratio characters that are prime-direction calibrated. Upstream one-way theorems already convert branch uniformity into trace coherence and conversely, by applying the corresponding character-level lemmas on each $\chi$.

proof idea

Term-mode Iff constructor. The forward arrow is the existing theorem that branch uniformity implies trace coherence (apply the character-level coherence-from-uniformity lemma under the calibrated hypotheses). The reverse arrow is the existing theorem that trace coherence implies branch uniformity (apply the character-level uniformity-from-coherence lemma the same way). No new quantification or case split is introduced.

why it matters

Native-cost uniqueness in PRC still has open calibration blockers. This equivalence lets the development treat branch uniformity and trace coherence as a single residual obligation: refute or discharge one and the other follows. Downstream, the trace-coherence target is refuted by transporting a branch-uniformity refutation across this Iff, and the same link is recorded in the native-cost uniqueness blocker certificate and the conditional universal-foundation certificate. In the broader Recognition chain this sits inside the foundation layer that feeds J-uniqueness and the forcing steps toward $\phi$ and the eight-tick structure, by clearing which prime-axis orientation statements are still free.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.