PRCPrimeCalibratedTwoAdicAxisTwistCharacter_iff_ratio_character_axis_twist
plain-language theorem explainer
Existence of a prime-calibrated two-adic axis-twist ratio character is equivalent to existence of any (uncalibrated) two-adic axis-twist ratio character. Cite this when collapsing the calibrated and uncalibrated branches of the character-rigidity fork, or when wiring the two-three composite local certificate. The proof is a pure Iff packaging of the two already-proved directed implications.
Claim. There exists a map $\chi$ on ratio orbits that is a ratio character, is prime-direction calibrated, and exhibits two-adic axis twist if and only if there exists a ratio character on ratio orbits that exhibits two-adic axis twist (with no separate prime-calibration hypothesis).
background
In the Primitive Recognition Calculus native-cost uniqueness development, a ratio character is a structure-preserving map $\chi$ on ratio orbits. Two-adic axis twist is a branch condition on that character along the $2$-adic direction. Prime-direction calibration is an extra field that pins the character's behavior on prime axes.
The calibrated package asserts existence of a $\chi$ that is simultaneously a ratio character, prime-direction calibrated, and two-adic axis-twisted. The uncalibrated package drops the prime-calibration conjunct. The module records that Pass 115 makes prime calibration automatic once the twist branch is carried by a ratio character, so the calibrated object is the native valuation route to attacking the current character-rigidity branch, while the uncalibrated object is the lighter construction target.
The two directed lemmas already show each package implies the other; this declaration only names their equivalence.
proof idea
Term-mode Iff introduction. The forward direction applies the lemma that forgets the prime-calibration witness from a calibrated two-adic axis-twist character, retaining the ratio character and the twist branch. The reverse direction applies the lemma that, from any two-adic axis-twist ratio character, rebuilds the calibrated package by filling the prime-calibration field automatically. No new algebra is done here.
why it matters
This equivalence is the bridge that lets the development treat calibrated and uncalibrated two-adic axis-twist characters as interchangeable. Downstream, the two-three composite local fork certificate stores it as the field equating calibrated two-adic axis twist with the ratio-character axis-twist package. The orientation-failure character is then chained through this Iff (and its symmetric) to the calibrated package. The universal-foundation conditional certificate sits further up the same dependency cone.
In framework terms this is foundation-layer bookkeeping for the character-rigidity fork inside native cost uniqueness, not a forcing-chain (T0–T8) step. It clears the path to either construct a countermodel character or close the rigidity branch without carrying redundant calibration hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.