Pith. sign in
theorem

PRCPrimeCalibrationForcesPrimeIdentityBranchUniformityTarget_of_identity_iff_two

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

plain-language theorem explainer

If prime calibration forces identity orientation on every native prime axis exactly when it forces identity on the distinguished orbit-2 axis, then it also forces full identity-branch uniformity across all native prime axes. Anyone assembling the PRC native-cost uniqueness chain or the universal-foundation certificate cites this implication. The proof is a one-line lift of the pointwise character lemma through the two targets' universal quantifiers.

Claim. Assume that for every ratio-orbit character $\chi$ that is prime-direction calibrated, identity orientation on any native prime axis is equivalent to identity orientation on the orbit-$2$ prime axis. Then, for every such $\chi$, identity orientation on any one native prime axis forces every native prime axis onto the identity branch.

background

In the Primitive Recognition Calculus, ratio characters $\chi$ map ratio orbits to ratio orbits and carry orientation data used to build the native cost. Prime-direction calibration constrains how $\chi$ may act on native prime axes. Two calibration targets are compared in this module.

The identity-iff-two target asks that, under prime calibration, $\chi$ is identity-oriented on an arbitrary native prime axis if and only if it is identity-oriented on the distinguished orbit-$2$ axis. The branch-uniformity target asks that identity orientation on any one native prime axis place all native prime axes on the identity branch.

A pointwise bridge is already proved: if a single character satisfies identity-iff-two, then it satisfies branch uniformity, by transporting identity through the equivalence with the orbit-$2$ axis. The present result lifts that bridge from characters to the two target propositions.

proof idea

Unpack the branch-uniformity target: introduce a character $\chi$ with the ratio-character and prime-calibration hypotheses. Apply the assumed identity-iff-two target at those data to obtain the pointwise identity-iff-two property for $\chi$. Pass that property to the upstream lemma that converts identity-iff-two into branch uniformity for one character. The resulting branch-uniformity statement is exactly the target conclusion.

why it matters

This is one direction of the equivalence between the two prime-calibration targets. Downstream, the biconditional packages both directions, so either formulation may be used interchangeably in the native-cost uniqueness development. The universal-foundation conditional certificate consumes this material when assembling the PRC foundation stack (kernel, real complete ordered field, and trace logic).

Within Recognition Science these calibration targets live in the foundation layer that forces the native cost structure tied to $J$-uniqueness (T5) and the Recognition Composition Law, before the later forcing steps (phi, eight-tick octave, $D=3$). Closing the equivalence removes a fork in the hypothesis interface for prime-axis orientation.

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