Pith. sign in
theorem

twoAdicAxisTwistCharacter_not_admissible

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

plain-language theorem explainer

The two-adic axis twist on ratio orbits is not an admissible ratio character. Anyone citing the repaired PRC admissible-character interface after the two-adic countermodel will use this exclusion. The proof is a one-line reduction: admissibility supplies prime-pair product cost consistency, which the twist already fails.

Claim. The two-adic axis twist character $\chi_{2}$ on ratio orbits is not admissible: it fails the repaired interface requiring ratio-character laws, prime calibration, and prime-pair product cost consistency.

background

In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters act on ratio orbits and feed a cost functional. After a two-adic countermodel, admissibility was repaired: a character $\chi$ is admissible only if it is a ratio character, is prime-calibrated, and satisfies prime-pair product cost consistency. That third field "preserves the two global orientations but excludes valuation twists."

The two-adic axis twist character is the ratio-orbit realization of the verifier two-adic branch twist: on each orbit it applies the corresponding rational two-adic twist and re-embeds. Upstream work already shows this map fails prime-pair product cost consistency, so it cannot sit in the repaired admissible class.

proof idea

One-line wrapper. Assume for contradiction that the two-adic axis twist is admissible. Project to the structure field prime_pair_product_cost, then apply the prior theorem that the twist is not prime-pair product cost consistent. Contradiction closes the claim.

why it matters

This seals the two-adic countermodel out of the repaired admissible-character interface used for native cost uniqueness. The parent interface requires ratio laws, prime calibration, and prime-pair product cost consistency precisely so valuation twists cannot masquerade as admissible characters while still matching the native cost. No downstream consumers are wired yet in the graph; the result is a local exclusion lemma that keeps the uniqueness pipeline free of the known two-adic branch twist. In the broader Recognition forcing picture it protects the uniqueness path toward the J-cost (T5) by blocking non-native characters before cost reconstruction.

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