Pith. sign in
theorem

PRCTwoThreeCompositeLocalOrientationFailureCharacter_absurd_of_prime_identity_branch_uniformity

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

plain-language theorem explainer

Under the prime-calibration branch-uniformity target, no ratio character can witness a 2·3 composite-local orientation failure. Anyone closing the native-cost uniqueness or universal-foundation certificate cites this. The proof is a two-step composition: the failure witness reduces to a two-adic axis-twist character, which is already absurd under the same uniformity hypothesis.

Claim. Assume that every prime-direction-calibrated ratio character is identity-branch-uniform on native prime axes. Then there is no ratio character $\chi$ that is a two-adic axis twist and fails two-three composite-local orientation (i.e., the constructive $2\cdot 3$ composite-local failure surface is empty).

background

In the Primitive Recognition Calculus, ratio characters $\chi$ act on ratio orbits and encode branch choices (identity vs reciprocal) along prime axes. A character is prime-direction-calibrated when native primes sit on distinguished directions; identity-branch-uniformity then demands that every identity-oriented native prime axis forces all native prime axes onto the identity branch.

The two-three composite-local orientation failure is the constructive countermodel surface: existence of a ratio character that is a two-adic axis twist yet fails local orientation on the composite direction $2\cdot 3$. The module treats this witness as equivalent (via reduction) to the reduced two-adic ratio-character obstruction used in native-cost uniqueness.

Upstream, the branch-uniformity target is the trace-free Prop that prime calibration forces identity-branch uniformity. A sibling theorem already shows that same target kills every two-adic axis-twist ratio character; another sibling extracts the two-adic twist from any two-three local-orientation failure witness.

proof idea

Term-mode composition, no case split. Assume a two-three composite-local orientation failure witness $h_{\mathrm{fail}}$. Apply the reduction lemma that any such witness yields a two-adic axis-twist ratio character (by dropping the local-orientation negation and retaining the character and twist data). Feed that derived twist into the upstream absurdity theorem: under the same prime-identity branch-uniformity hypothesis, no two-adic axis-twist ratio character exists. Contradiction, so the failure surface is empty.

why it matters

This closes one constructive countermodel surface on the path to native-cost uniqueness: the $2\cdot 3$ composite-local failure cannot occur once prime calibration enforces identity-branch uniformity. Downstream it is consumed by prc_universal_foundation_conditional_certificate, which packages kernel, real-complete ordered field, and trace-logic certificates into the conditional universal-foundation bundle.

In the broader Recognition forcing chain, native-cost uniqueness feeds the J-cost story (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Ruling out mixed-branch twists on small composites is part of forcing a unique cost functional before $\varphi$ and the eight-tick structure are installed. The result is conditional on the uniformity target Prop, not an unconditional uniqueness theorem by itself.

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