Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeIdentityIffTwoPrimeIdentityTarget_of_branch_uniformity

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

plain-language theorem explainer

If prime calibration forces branch-uniform identity orientation on native prime axes, then it also forces the identity-iff-two property: identity on any prime axis holds exactly when it holds on the orbit-2 axis. Native-cost uniqueness and universal-foundation certificates cite this reduction. The proof is a one-line unpacking that applies the character-level branch-uniform implication.

Claim. Assume that every ratio character $\chi$ that is prime-direction calibrated is branch-uniform on native prime axes (identity on one identity-oriented prime axis forces identity on all). Then every such calibrated $\chi$ satisfies the identity-iff-two law: $\chi$ is identity-oriented on an arbitrary native prime axis if and only if it is identity-oriented on the distinguished orbit-$2$ prime axis.

background

In the Primitive Recognition Calculus, ratio characters $\chi : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ encode orientation data along ratio orbits. Prime-direction calibration restricts how $\chi$ may act on native prime axes. Two calibration targets are compared here.

Branch uniformity says that once any identity-oriented native prime axis is fixed, every native prime axis sits on the identity branch. The identity-iff-two target is weaker in appearance: identity orientation on an arbitrary prime axis is equivalent to identity on the distinguished orbit-$2$ axis.

Upstream, the character-level lemma already shows that branch uniformity of a single $\chi$ implies the identity-iff-two property for that $\chi$. The present statement lifts that implication from characters to the corresponding global calibration targets (universal quantifiers over calibrated characters).

proof idea

Term-mode one-line wrapper. Unpack the identity-iff-two target by introducing a calibrated character $\chi$. Apply the hypothesis (branch-uniformity target) at $\chi$ to obtain branch uniformity of $\chi$. Feed that into PRCCharacterPrimeIdentityIffTwoPrimeIdentity_of_branch_uniform, which already proves the character-level identity-iff-two law from branch uniformity. No extra algebraic work.

why it matters

Closes one direction of the equivalence between the branch-uniformity target and the identity-iff-two target; the sibling converse completes the biconditional used to interchange those interfaces in native-cost uniqueness. Downstream, that equivalence feeds the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-field, and trace-logic certificates for the PRC foundation layer.

In the Recognition Science forcing picture this sits inside native-cost uniqueness for the J-cost side of the calculus (T5 J-uniqueness and the Recognition Composition Law live one layer up). It does not itself force $\phi$ or $D=3$; it only collapses two prime-axis orientation targets so later uniqueness arguments can quote either form.

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