proveit.physics.quantum.QPE._alpha_m_mod_as_geometric_sum proveit.physics.quantum.QPE._best_round_is_int proveit.physics.quantum.QPE._phase_from_best_with_delta_b proveit.physics.quantum.QPE._delta_b_is_real proveit.core_expr_types proveit.logic proveit.numbers proveit.physics.quantum.QPE._two_pow_t_is_nat_pos proveit.physics.quantum.QPE._delta_b_is_zero_or_non_int proveit.physics.quantum.QPE._alpha_are_complex proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval proveit.trigonometry