theorem
proved
PRCCharacterPrimeDirectionCalibrated_of_two_adic_axis_twist
show as:
PRCCharacterPrimeDirectionCalibrated_of_two_adic_axis_twist