Pith. sign in
theorem

PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_no_calibrated_two_adic_axis_twist

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

plain-language theorem explainer

Absence of a prime-calibrated two-adic axis-twist character forces absence of any 2·3 composite-local orientation failure character. Native-cost uniqueness and character-rigidity arguments cite this to discharge the constructive countermodel surface. The proof is a short contrappositive: the failure witness already builds a calibrated twist, so denying the latter denies the former.

Claim. If there does not exist a map $\chi$ on ratio orbits that is a ratio character, prime-direction calibrated, and a two-adic axis twist, then there does not exist a map $\chi$ that is a ratio character and a two-adic axis twist yet fails the $2\cdot 3$ composite-local orientation condition.

background

In the Primitive Recognition Calculus, cost uniqueness is attacked through characters on ratio orbits: maps $\chi$ that preserve the multiplicative structure used to read native cost. A two-adic axis twist is a character that flips the orbit of $2$ onto the reciprocal branch. Prime-direction calibration strengthens that model so the twist is aligned with a native prime direction.

The $2\cdot 3$ composite-local orientation failure is the constructive countermodel surface: a ratio character that twists the two-adic axis and yet fails orientation on the composite direction $2\cdot 3$. Its doc-comment calls it "equivalent to the reduced two-adic ratio-character target." The calibrated twist object is the native-valuation route that would refute the current character-rigidity branch if it could be built.

Upstream, any such failure character already yields a prime-calibrated two-adic axis-twist character, by stripping the orientation failure down to a calibrated twist model.

proof idea

Assume a $2\cdot 3$ composite-local orientation failure character. Apply the upstream implication that every such failure character produces a prime-calibrated two-adic axis-twist character. That contradicts the hypothesis that no calibrated twist exists. Discharge by exact on the negated hypothesis. Pure contrappositive packaging; no new algebraic work.

why it matters

Closes the failure-character side of the two-adic axis-twist target under the no-calibrated-twist hypothesis. The immediate parent turns that absurdity into the positive orientation target for two-adic axis twists. That target feeds the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic certificates for the PRC foundation layer.

In the broader Recognition forcing picture this sits inside native cost uniqueness for the character calculus that underwrites J-cost rigidity (T5) and the self-similar fixed point $\phi$ (T6). It does not itself force $\phi$ or the eight-tick octave; it removes one constructive escape hatch on the two-adic mixed branch so the rigidity story can proceed.

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