BD0014

binary_modular_exponent_coded_execution_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

For every arbitrary natural exponent and guarded modulus, construct canonical beta-coded digits, their full genuine square-and-multiply history, and its proved modular-power result.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall n a m. (exists ff_modulus_gap_binary_bd_modulus. ff_modulus_gap_binary_bd_modulus + S 1 = m) -> exists l b c r. ((((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_total_run_canonical_length ff_lower_bl_bd_total_run_canonical_length ff_upper_bl_bd_total_run_canonical_length. (((l) = S ff_exponent_bl_bd_total_run_canonical_length) /\ ((exists ff_positive_bl_bd_total_run_canonical_length. ff_positive_bl_bd_total_run_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_total_run_canonical_length_lower pa_c_bl_bd_total_run_canonical_length_lower. ((forall pa_i_bl_bd_total_run_canonical_length_lower_repeat. (exists pa_lt_bl_bd_total_run_canonical_length_lower_repeat_bound. pa_lt_bl_bd_total_run_canonical_length_lower_repeat_bound + S pa_i_bl_bd_total_run_canonical_length_lower_repeat = ff_exponent_bl_bd_total_run_canonical_length) -> (((exists pa_h_bl_bd_total_run_canonical_length_lower_repeat_decoded. pa_h_bl_bd_total_run_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_run_canonical_length_lower_repeat)) * pa_c_bl_bd_total_run_canonical_length_lower)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_repeat_decoded. pa_b_bl_bd_total_run_canonical_length_lower = pa_q_bl_bd_total_run_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_total_run_canonical_length_lower_repeat)) * pa_c_bl_bd_total_run_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_total_run_canonical_length_lower_product pa_v_bl_bd_total_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_start. pa_h_bl_bd_total_run_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_start. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_terminal. pa_h_bl_bd_total_run_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_total_run_canonical_length) = S ((S (ff_exponent_bl_bd_total_run_canonical_length)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_terminal. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_total_run_canonical_length)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (ff_lower_bl_bd_total_run_canonical_length))) /\ forall pa_i_bl_bd_total_run_canonical_length_lower_product. (exists pa_lt_bl_bd_total_run_canonical_length_lower_product_bound. pa_lt_bl_bd_total_run_canonical_length_lower_product_bound + S pa_i_bl_bd_total_run_canonical_length_lower_product = ff_exponent_bl_bd_total_run_canonical_length) -> exists pa_p_bl_bd_total_run_canonical_length_lower_product pa_r_bl_bd_total_run_canonical_length_lower_product pa_s_bl_bd_total_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_factor. pa_h_bl_bd_total_run_canonical_length_lower_product_factor + S (pa_p_bl_bd_total_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_c_bl_bd_total_run_canonical_length_lower)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_factor. pa_b_bl_bd_total_run_canonical_length_lower = pa_q_bl_bd_total_run_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_c_bl_bd_total_run_canonical_length_lower) + (pa_p_bl_bd_total_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_partial. pa_h_bl_bd_total_run_canonical_length_lower_product_partial + S (pa_r_bl_bd_total_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_partial. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (pa_r_bl_bd_total_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_successor. pa_h_bl_bd_total_run_canonical_length_lower_product_successor + S (pa_s_bl_bd_total_run_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_successor. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (pa_s_bl_bd_total_run_canonical_length_lower_product))) /\ pa_s_bl_bd_total_run_canonical_length_lower_product = pa_r_bl_bd_total_run_canonical_length_lower_product * pa_p_bl_bd_total_run_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_total_run_canonical_length_upper pa_c_bl_bd_total_run_canonical_length_upper. ((forall pa_i_bl_bd_total_run_canonical_length_upper_repeat. (exists pa_lt_bl_bd_total_run_canonical_length_upper_repeat_bound. pa_lt_bl_bd_total_run_canonical_length_upper_repeat_bound + S pa_i_bl_bd_total_run_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_total_run_canonical_length_upper_repeat_decoded. pa_h_bl_bd_total_run_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_run_canonical_length_upper_repeat)) * pa_c_bl_bd_total_run_canonical_length_upper)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_repeat_decoded. pa_b_bl_bd_total_run_canonical_length_upper = pa_q_bl_bd_total_run_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_total_run_canonical_length_upper_repeat)) * pa_c_bl_bd_total_run_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_total_run_canonical_length_upper_product pa_v_bl_bd_total_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_start. pa_h_bl_bd_total_run_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_start. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_terminal. pa_h_bl_bd_total_run_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_total_run_canonical_length) = S ((S (l)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_terminal. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (ff_upper_bl_bd_total_run_canonical_length))) /\ forall pa_i_bl_bd_total_run_canonical_length_upper_product. (exists pa_lt_bl_bd_total_run_canonical_length_upper_product_bound. pa_lt_bl_bd_total_run_canonical_length_upper_product_bound + S pa_i_bl_bd_total_run_canonical_length_upper_product = l) -> exists pa_p_bl_bd_total_run_canonical_length_upper_product pa_r_bl_bd_total_run_canonical_length_upper_product pa_s_bl_bd_total_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_factor. pa_h_bl_bd_total_run_canonical_length_upper_product_factor + S (pa_p_bl_bd_total_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_c_bl_bd_total_run_canonical_length_upper)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_factor. pa_b_bl_bd_total_run_canonical_length_upper = pa_q_bl_bd_total_run_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_c_bl_bd_total_run_canonical_length_upper) + (pa_p_bl_bd_total_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_partial. pa_h_bl_bd_total_run_canonical_length_upper_product_partial + S (pa_r_bl_bd_total_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_partial. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (pa_r_bl_bd_total_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_successor. pa_h_bl_bd_total_run_canonical_length_upper_product_successor + S (pa_s_bl_bd_total_run_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_successor. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (pa_s_bl_bd_total_run_canonical_length_upper_product))) /\ pa_s_bl_bd_total_run_canonical_length_upper_product = pa_r_bl_bd_total_run_canonical_length_upper_product * pa_p_bl_bd_total_run_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_total_run_canonical_length. ff_lower_gap_bl_bd_total_run_canonical_length + (ff_lower_bl_bd_total_run_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_total_run_canonical_length. ff_upper_gap_bl_bd_total_run_canonical_length + S (n) = (ff_upper_bl_bd_total_run_canonical_length))))))))) /\ (((forall ff_index_be_bd_total_run_canonical_code_digits ff_digit_be_bd_total_run_canonical_code_digits. (exists ff_lt_be_bd_total_run_canonical_code_digits_bound. ff_lt_be_bd_total_run_canonical_code_digits_bound + S ff_index_be_bd_total_run_canonical_code_digits = l) -> (((exists ff_h_be_bd_total_run_canonical_code_digits_digit. ff_h_be_bd_total_run_canonical_code_digits_digit + S (ff_digit_be_bd_total_run_canonical_code_digits) = S ((S (ff_index_be_bd_total_run_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_total_run_canonical_code_digits_digit. b = ff_q_be_bd_total_run_canonical_code_digits_digit * S ((S (ff_index_be_bd_total_run_canonical_code_digits)) * c) + (ff_digit_be_bd_total_run_canonical_code_digits))) -> (ff_digit_be_bd_total_run_canonical_code_digits = 0 \/ ff_digit_be_bd_total_run_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_total_run_canonical_code_horner ff_v_ph_bd_total_run_canonical_code_horner. ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_start. fs_h_ph_bd_total_run_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_start. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_total_run_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_terminal. fs_h_ph_bd_total_run_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_terminal. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_total_run_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_total_run_canonical_code_horner_body_steps. (exists ph_bound_bd_total_run_canonical_code_horner_body_steps. ph_bound_bd_total_run_canonical_code_horner_body_steps + S ff_i_ph_bd_total_run_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps ff_previous_ph_bd_total_run_canonical_code_horner_body_steps ff_current_ph_bd_total_run_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_total_run_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_total_run_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_steps_before. fs_h_ph_bd_total_run_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_total_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_steps_before. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner) + (ff_previous_ph_bd_total_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_steps_after. fs_h_ph_bd_total_run_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_total_run_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_steps_after. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner) + (ff_current_ph_bd_total_run_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_total_run_canonical_code_horner_body_steps = ff_previous_ph_bd_total_run_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps)))))))))) /\ ((exists ff_trace_code_be_bd_total_run_execution ff_trace_scale_be_bd_total_run_execution. ((((((exists ff_h_be_bd_total_run_execution_trace_start. ff_h_be_bd_total_run_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_trace_start. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_total_run_execution) + (1))) /\ forall ff_index_be_bd_total_run_execution_trace. (exists ff_lt_be_bd_total_run_execution_trace_bound. ff_lt_be_bd_total_run_execution_trace_bound + S ff_index_be_bd_total_run_execution_trace = l) -> exists ff_digit_be_bd_total_run_execution_trace ff_previous_be_bd_total_run_execution_trace ff_current_be_bd_total_run_execution_trace. ((((exists ff_h_be_bd_total_run_execution_trace_source. ff_h_be_bd_total_run_execution_trace_source + S (ff_digit_be_bd_total_run_execution_trace) = S ((S (ff_index_be_bd_total_run_execution_trace)) * c)) /\ exists ff_q_be_bd_total_run_execution_trace_source. b = ff_q_be_bd_total_run_execution_trace_source * S ((S (ff_index_be_bd_total_run_execution_trace)) * c) + (ff_digit_be_bd_total_run_execution_trace))) /\ ((((exists ff_h_be_bd_total_run_execution_trace_before. ff_h_be_bd_total_run_execution_trace_before + S (ff_previous_be_bd_total_run_execution_trace) = S ((S (ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_trace_before. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_trace_before * S ((S (ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution) + (ff_previous_be_bd_total_run_execution_trace))) /\ ((((exists ff_h_be_bd_total_run_execution_trace_after. ff_h_be_bd_total_run_execution_trace_after + S (ff_current_be_bd_total_run_execution_trace) = S ((S (S ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_trace_after. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_trace_after * S ((S (S ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution) + (ff_current_be_bd_total_run_execution_trace))) /\ ((((ff_digit_be_bd_total_run_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_total_run_execution_trace_transition_square. ff_gap_binary_be_bd_total_run_execution_trace_transition_square + S (ff_current_be_bd_total_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_total_run_execution_trace_transition_square_congruence ff_right_binary_be_bd_total_run_execution_trace_transition_square_congruence. (ff_previous_be_bd_total_run_execution_trace * ff_previous_be_bd_total_run_execution_trace) + m * ff_left_binary_be_bd_total_run_execution_trace_transition_square_congruence = (ff_current_be_bd_total_run_execution_trace) + m * ff_right_binary_be_bd_total_run_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_total_run_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_total_run_execution_trace_transition_multiply. ff_gap_binary_be_bd_total_run_execution_trace_transition_multiply + S (ff_current_be_bd_total_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_total_run_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_total_run_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_total_run_execution_trace * ff_previous_be_bd_total_run_execution_trace) * a) + m * ff_left_binary_be_bd_total_run_execution_trace_transition_multiply_congruence = (ff_current_be_bd_total_run_execution_trace) + m * ff_right_binary_be_bd_total_run_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_total_run_execution_terminal. ff_h_be_bd_total_run_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_terminal. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_terminal * S ((S (l)) * ff_trace_scale_be_bd_total_run_execution) + (r))))) /\ (exists ff_power_binary_bd_total_run_power. ((exists ff_b_binary_bd_total_run_power_value ff_c_binary_bd_total_run_power_value. ((forall ff_i_binary_bd_total_run_power_value_repeat. (exists ff_lt_binary_bd_total_run_power_value_repeat_bound. ff_lt_binary_bd_total_run_power_value_repeat_bound + S ff_i_binary_bd_total_run_power_value_repeat = n) -> (((exists ff_h_binary_bd_total_run_power_value_repeat_decoded. ff_h_binary_bd_total_run_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_bd_total_run_power_value_repeat)) * ff_c_binary_bd_total_run_power_value)) /\ exists ff_q_binary_bd_total_run_power_value_repeat_decoded. ff_b_binary_bd_total_run_power_value = ff_q_binary_bd_total_run_power_value_repeat_decoded * S ((S (ff_i_binary_bd_total_run_power_value_repeat)) * ff_c_binary_bd_total_run_power_value) + (a)))) /\ (exists ff_u_binary_bd_total_run_power_value_product ff_v_binary_bd_total_run_power_value_product. ((((exists ff_h_binary_bd_total_run_power_value_product_start. ff_h_binary_bd_total_run_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_bd_total_run_power_value_product)) /\ exists ff_q_binary_bd_total_run_power_value_product_start. ff_u_binary_bd_total_run_power_value_product = ff_q_binary_bd_total_run_power_value_product_start * S ((S (0)) * ff_v_binary_bd_total_run_power_value_product) + (1))) /\ ((((exists ff_h_binary_bd_total_run_power_value_product_terminal. ff_h_binary_bd_total_run_power_value_product_terminal + S (ff_power_binary_bd_total_run_power) = S ((S (n)) * ff_v_binary_bd_total_run_power_value_product)) /\ exists ff_q_binary_bd_total_run_power_value_product_terminal. ff_u_binary_bd_total_run_power_value_product = ff_q_binary_bd_total_run_power_value_product_terminal * S ((S (n)) * ff_v_binary_bd_total_run_power_value_product) + (ff_power_binary_bd_total_run_power))) /\ forall ff_i_binary_bd_total_run_power_value_product. (exists ff_lt_binary_bd_total_run_power_value_product_bound. ff_lt_binary_bd_total_run_power_value_product_bound + S ff_i_binary_bd_total_run_power_value_product = n) -> exists ff_p_binary_bd_total_run_power_value_product ff_r_binary_bd_total_run_power_value_product ff_s_binary_bd_total_run_power_value_product. ((((exists ff_h_binary_bd_total_run_power_value_product_factor. ff_h_binary_bd_total_run_power_value_product_factor + S (ff_p_binary_bd_total_run_power_value_product) = S ((S (ff_i_binary_bd_total_run_power_value_product)) * ff_c_binary_bd_total_run_power_value)) /\ exists ff_q_binary_bd_total_run_power_value_product_factor. ff_b_binary_bd_total_run_power_value = ff_q_binary_bd_total_run_power_value_product_factor * S ((S (ff_i_binary_bd_total_run_power_value_product)) * ff_c_binary_bd_total_run_power_value) + (ff_p_binary_bd_total_run_power_value_product))) /\ ((((exists ff_h_binary_bd_total_run_power_value_product_partial. ff_h_binary_bd_total_run_power_value_product_partial + S (ff_r_binary_bd_total_run_power_value_product) = S ((S (ff_i_binary_bd_total_run_power_value_product)) * ff_v_binary_bd_total_run_power_value_product)) /\ exists ff_q_binary_bd_total_run_power_value_product_partial. ff_u_binary_bd_total_run_power_value_product = ff_q_binary_bd_total_run_power_value_product_partial * S ((S (ff_i_binary_bd_total_run_power_value_product)) * ff_v_binary_bd_total_run_power_value_product) + (ff_r_binary_bd_total_run_power_value_product))) /\ ((((exists ff_h_binary_bd_total_run_power_value_product_successor. ff_h_binary_bd_total_run_power_value_product_successor + S (ff_s_binary_bd_total_run_power_value_product) = S ((S (S ff_i_binary_bd_total_run_power_value_product)) * ff_v_binary_bd_total_run_power_value_product)) /\ exists ff_q_binary_bd_total_run_power_value_product_successor. ff_u_binary_bd_total_run_power_value_product = ff_q_binary_bd_total_run_power_value_product_successor * S ((S (S ff_i_binary_bd_total_run_power_value_product)) * ff_v_binary_bd_total_run_power_value_product) + (ff_s_binary_bd_total_run_power_value_product))) /\ ff_s_binary_bd_total_run_power_value_product = ff_r_binary_bd_total_run_power_value_product * ff_p_binary_bd_total_run_power_value_product)))))))) /\ (((exists ff_gap_binary_bd_total_run_power_residue. ff_gap_binary_bd_total_run_power_residue + S (r) = m) /\ (exists ff_left_binary_bd_total_run_power_residue_congruence ff_right_binary_bd_total_run_power_residue_congruence. (ff_power_binary_bd_total_run_power) + m * ff_left_binary_bd_total_run_power_residue_congruence = (r) + m * ff_right_binary_bd_total_run_power_residue_congruence))))))))

Constructive proof overview

Generated structural guide

For every arbitrary natural exponent and guarded modulus, construct canonical beta-coded digits, their full genuine square-and-multiply history, and its proved modular-power result.

The unchanged tactic script uses 3 declared prerequisites and contains 43 exact native proof lines.

Alpha v34 checked-use · first admitted v23 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

BD000A binary_exponent_digit_prefix_exists binary_modular_execution_exists Alpha theorem; checked-use authorized BD0013 binary_modular_exponent_coded_execution_power_correct

Direct dependents

BD0016 binary_modular_exponent_coded_execution_exists_unique BD0018 binary_modular_execution_logarithmic_bound

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

43 script commands · 14 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
binary exponent digit prefix existsbinary modular exponent coded execution power correct

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro m
  4. L4
    intro hmodulus
02Establish hcanonicalL5–7

Establish this local claim before using it. It is not an additional assumption.

  1. L5
    have hcanonical : ∃ l. ∃ b. ∃ c. BinaryCanonicalExponentDigitCode(n,l,b,c)Definitions: BinaryCanonicalExponentDigitCode
  2. L6
    specialize binary_exponent_digit_prefix_exists n
  3. L7
    exact binary_exponent_digit_prefix_exists
03Separate the logical casesL8–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L8
    cases hcanonical
  2. L9
    cases hcanonical_witness
  3. L10
    cases hcanonical_witness_witness
04Establish hdigitsL11–11

Establish this local claim before using it. It is not an additional assumption.

  1. L11
    have hdigits : BinaryDigitPrefix(x1,x2,x)Definitions: BinaryDigitPrefix
05Separate the logical casesL12–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hcanonical_witness_witness_witness
  2. L13
    cases hcanonical_witness_witness_witness_right
06Use earlier factsL14–14

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L14
    exact hcanonical_witness_witness_witness_right_left
07Establish hexecutionL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary modular execution exists.

  1. L15
    have hexecution : ∃ r. BinaryModularExecution(x1,x2,a,m,x,r)Definitions: BinaryModularExecution
  2. L16
    specialize binary_modular_execution_exists x1
  3. L17
    specialize binary_modular_execution_exists x2
  4. L18
    specialize binary_modular_execution_exists a
  5. L19
    specialize binary_modular_execution_exists m
  6. L20
    specialize binary_modular_execution_exists x
  7. L21
    apply binary_modular_execution_exists
  8. L22
    exact hmodulus
  9. L23
    exact hdigits
08Separate the logical casesL24–24

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L24
    cases hexecution
09Construct an explicit witnessL25–28

Supply the displayed value, then prove that it has the required property.

  1. L25
    exists x
  2. L26
    exists x1
  3. L27
    exists x2
  4. L28
    exists x3
10Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    split
11Use earlier factsL30–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L30
    exact hcanonical_witness_witness_witness
12Separate the logical casesL31–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    split
13Use earlier factsL32–41

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    exact hexecution_witness
  2. L33
    specialize binary_modular_exponent_coded_execution_power_correct n
  3. L34
    specialize binary_modular_exponent_coded_execution_power_correct a
  4. L35
    specialize binary_modular_exponent_coded_execution_power_correct m
  5. L36
    specialize binary_modular_exponent_coded_execution_power_correct x
  6. L37
    specialize binary_modular_exponent_coded_execution_power_correct x1
  7. L38
    specialize binary_modular_exponent_coded_execution_power_correct x2
  8. L39
    specialize binary_modular_exponent_coded_execution_power_correct x3
  9. L40
    apply binary_modular_exponent_coded_execution_power_correct
  10. L41
    exact hmodulus
14Use earlier factsL42–43

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L42
    exact hcanonical_witness_witness_witness
  2. L43
    exact hexecution_witness

Library-wide reading audit

Original exact command ledger · 43 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro m
  4. 0004intro hmodulus
  5. 0005have hcanonical : exists l b c. ((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_total_run_canonical_length ff_lower_bl_bd_total_run_canonical_length ff_upper_bl_bd_total_run_canonical_length. (((l) = S ff_exponent_bl_bd_total_run_canonical_length) /\ ((exists ff_positive_bl_bd_total_run_canonical_length. ff_positive_bl_bd_total_run_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_total_run_canonical_length_lower pa_c_bl_bd_total_run_canonical_length_lower. ((forall pa_i_bl_bd_total_run_canonical_length_lower_repeat. (exists pa_lt_bl_bd_total_run_canonical_length_lower_repeat_bound. pa_lt_bl_bd_total_run_canonical_length_lower_repeat_bound + S pa_i_bl_bd_total_run_canonical_length_lower_repeat = ff_exponent_bl_bd_total_run_canonical_length) -> (((exists pa_h_bl_bd_total_run_canonical_length_lower_repeat_decoded. pa_h_bl_bd_total_run_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_run_canonical_length_lower_repeat)) * pa_c_bl_bd_total_run_canonical_length_lower)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_repeat_decoded. pa_b_bl_bd_total_run_canonical_length_lower = pa_q_bl_bd_total_run_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_total_run_canonical_length_lower_repeat)) * pa_c_bl_bd_total_run_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_total_run_canonical_length_lower_product pa_v_bl_bd_total_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_start. pa_h_bl_bd_total_run_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_start. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_terminal. pa_h_bl_bd_total_run_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_total_run_canonical_length) = S ((S (ff_exponent_bl_bd_total_run_canonical_length)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_terminal. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_total_run_canonical_length)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (ff_lower_bl_bd_total_run_canonical_length))) /\ forall pa_i_bl_bd_total_run_canonical_length_lower_product. (exists pa_lt_bl_bd_total_run_canonical_length_lower_product_bound. pa_lt_bl_bd_total_run_canonical_length_lower_product_bound + S pa_i_bl_bd_total_run_canonical_length_lower_product = ff_exponent_bl_bd_total_run_canonical_length) -> exists pa_p_bl_bd_total_run_canonical_length_lower_product pa_r_bl_bd_total_run_canonical_length_lower_product pa_s_bl_bd_total_run_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_factor. pa_h_bl_bd_total_run_canonical_length_lower_product_factor + S (pa_p_bl_bd_total_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_c_bl_bd_total_run_canonical_length_lower)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_factor. pa_b_bl_bd_total_run_canonical_length_lower = pa_q_bl_bd_total_run_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_c_bl_bd_total_run_canonical_length_lower) + (pa_p_bl_bd_total_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_partial. pa_h_bl_bd_total_run_canonical_length_lower_product_partial + S (pa_r_bl_bd_total_run_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_partial. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (pa_r_bl_bd_total_run_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_lower_product_successor. pa_h_bl_bd_total_run_canonical_length_lower_product_successor + S (pa_s_bl_bd_total_run_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_lower_product_successor. pa_u_bl_bd_total_run_canonical_length_lower_product = pa_q_bl_bd_total_run_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_total_run_canonical_length_lower_product)) * pa_v_bl_bd_total_run_canonical_length_lower_product) + (pa_s_bl_bd_total_run_canonical_length_lower_product))) /\ pa_s_bl_bd_total_run_canonical_length_lower_product = pa_r_bl_bd_total_run_canonical_length_lower_product * pa_p_bl_bd_total_run_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_total_run_canonical_length_upper pa_c_bl_bd_total_run_canonical_length_upper. ((forall pa_i_bl_bd_total_run_canonical_length_upper_repeat. (exists pa_lt_bl_bd_total_run_canonical_length_upper_repeat_bound. pa_lt_bl_bd_total_run_canonical_length_upper_repeat_bound + S pa_i_bl_bd_total_run_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_total_run_canonical_length_upper_repeat_decoded. pa_h_bl_bd_total_run_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_run_canonical_length_upper_repeat)) * pa_c_bl_bd_total_run_canonical_length_upper)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_repeat_decoded. pa_b_bl_bd_total_run_canonical_length_upper = pa_q_bl_bd_total_run_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_total_run_canonical_length_upper_repeat)) * pa_c_bl_bd_total_run_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_total_run_canonical_length_upper_product pa_v_bl_bd_total_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_start. pa_h_bl_bd_total_run_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_start. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_terminal. pa_h_bl_bd_total_run_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_total_run_canonical_length) = S ((S (l)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_terminal. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (ff_upper_bl_bd_total_run_canonical_length))) /\ forall pa_i_bl_bd_total_run_canonical_length_upper_product. (exists pa_lt_bl_bd_total_run_canonical_length_upper_product_bound. pa_lt_bl_bd_total_run_canonical_length_upper_product_bound + S pa_i_bl_bd_total_run_canonical_length_upper_product = l) -> exists pa_p_bl_bd_total_run_canonical_length_upper_product pa_r_bl_bd_total_run_canonical_length_upper_product pa_s_bl_bd_total_run_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_factor. pa_h_bl_bd_total_run_canonical_length_upper_product_factor + S (pa_p_bl_bd_total_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_c_bl_bd_total_run_canonical_length_upper)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_factor. pa_b_bl_bd_total_run_canonical_length_upper = pa_q_bl_bd_total_run_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_c_bl_bd_total_run_canonical_length_upper) + (pa_p_bl_bd_total_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_partial. pa_h_bl_bd_total_run_canonical_length_upper_product_partial + S (pa_r_bl_bd_total_run_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_partial. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (pa_r_bl_bd_total_run_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_run_canonical_length_upper_product_successor. pa_h_bl_bd_total_run_canonical_length_upper_product_successor + S (pa_s_bl_bd_total_run_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_run_canonical_length_upper_product_successor. pa_u_bl_bd_total_run_canonical_length_upper_product = pa_q_bl_bd_total_run_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_total_run_canonical_length_upper_product)) * pa_v_bl_bd_total_run_canonical_length_upper_product) + (pa_s_bl_bd_total_run_canonical_length_upper_product))) /\ pa_s_bl_bd_total_run_canonical_length_upper_product = pa_r_bl_bd_total_run_canonical_length_upper_product * pa_p_bl_bd_total_run_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_total_run_canonical_length. ff_lower_gap_bl_bd_total_run_canonical_length + (ff_lower_bl_bd_total_run_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_total_run_canonical_length. ff_upper_gap_bl_bd_total_run_canonical_length + S (n) = (ff_upper_bl_bd_total_run_canonical_length))))))))) /\ (((forall ff_index_be_bd_total_run_canonical_code_digits ff_digit_be_bd_total_run_canonical_code_digits. (exists ff_lt_be_bd_total_run_canonical_code_digits_bound. ff_lt_be_bd_total_run_canonical_code_digits_bound + S ff_index_be_bd_total_run_canonical_code_digits = l) -> (((exists ff_h_be_bd_total_run_canonical_code_digits_digit. ff_h_be_bd_total_run_canonical_code_digits_digit + S (ff_digit_be_bd_total_run_canonical_code_digits) = S ((S (ff_index_be_bd_total_run_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_total_run_canonical_code_digits_digit. b = ff_q_be_bd_total_run_canonical_code_digits_digit * S ((S (ff_index_be_bd_total_run_canonical_code_digits)) * c) + (ff_digit_be_bd_total_run_canonical_code_digits))) -> (ff_digit_be_bd_total_run_canonical_code_digits = 0 \/ ff_digit_be_bd_total_run_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_total_run_canonical_code_horner ff_v_ph_bd_total_run_canonical_code_horner. ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_start. fs_h_ph_bd_total_run_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_start. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_total_run_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_terminal. fs_h_ph_bd_total_run_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_terminal. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_total_run_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_total_run_canonical_code_horner_body_steps. (exists ph_bound_bd_total_run_canonical_code_horner_body_steps. ph_bound_bd_total_run_canonical_code_horner_body_steps + S ff_i_ph_bd_total_run_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps ff_previous_ph_bd_total_run_canonical_code_horner_body_steps ff_current_ph_bd_total_run_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_total_run_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_total_run_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_steps_before. fs_h_ph_bd_total_run_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_total_run_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_steps_before. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner) + (ff_previous_ph_bd_total_run_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_run_canonical_code_horner_body_steps_after. fs_h_ph_bd_total_run_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_total_run_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner)) /\ exists fs_q_ph_bd_total_run_canonical_code_horner_body_steps_after. ff_u_ph_bd_total_run_canonical_code_horner = fs_q_ph_bd_total_run_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_total_run_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_run_canonical_code_horner) + (ff_current_ph_bd_total_run_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_total_run_canonical_code_horner_body_steps = ff_previous_ph_bd_total_run_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_total_run_canonical_code_horner_body_steps))))))))))
  6. 0006specialize binary_exponent_digit_prefix_exists n
  7. 0007exact binary_exponent_digit_prefix_exists
  8. 0008cases hcanonical
  9. 0009cases hcanonical_witness
  10. 0010cases hcanonical_witness_witness
  11. 0011have hdigits : (forall ff_index_be_bd_total_run_digits ff_digit_be_bd_total_run_digits. (exists ff_lt_be_bd_total_run_digits_bound. ff_lt_be_bd_total_run_digits_bound + S ff_index_be_bd_total_run_digits = x) -> (((exists ff_h_be_bd_total_run_digits_digit. ff_h_be_bd_total_run_digits_digit + S (ff_digit_be_bd_total_run_digits) = S ((S (ff_index_be_bd_total_run_digits)) * x2)) /\ exists ff_q_be_bd_total_run_digits_digit. x1 = ff_q_be_bd_total_run_digits_digit * S ((S (ff_index_be_bd_total_run_digits)) * x2) + (ff_digit_be_bd_total_run_digits))) -> (ff_digit_be_bd_total_run_digits = 0 \/ ff_digit_be_bd_total_run_digits = 1))
  12. 0012cases hcanonical_witness_witness_witness
  13. 0013cases hcanonical_witness_witness_witness_right
  14. 0014exact hcanonical_witness_witness_witness_right_left
  15. 0015have hexecution : exists r. (exists ff_trace_code_be_bd_total_run_execution ff_trace_scale_be_bd_total_run_execution. ((((((exists ff_h_be_bd_total_run_execution_trace_start. ff_h_be_bd_total_run_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_trace_start. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_trace_start * S ((S (0)) * ff_trace_scale_be_bd_total_run_execution) + (1))) /\ forall ff_index_be_bd_total_run_execution_trace. (exists ff_lt_be_bd_total_run_execution_trace_bound. ff_lt_be_bd_total_run_execution_trace_bound + S ff_index_be_bd_total_run_execution_trace = x) -> exists ff_digit_be_bd_total_run_execution_trace ff_previous_be_bd_total_run_execution_trace ff_current_be_bd_total_run_execution_trace. ((((exists ff_h_be_bd_total_run_execution_trace_source. ff_h_be_bd_total_run_execution_trace_source + S (ff_digit_be_bd_total_run_execution_trace) = S ((S (ff_index_be_bd_total_run_execution_trace)) * x2)) /\ exists ff_q_be_bd_total_run_execution_trace_source. x1 = ff_q_be_bd_total_run_execution_trace_source * S ((S (ff_index_be_bd_total_run_execution_trace)) * x2) + (ff_digit_be_bd_total_run_execution_trace))) /\ ((((exists ff_h_be_bd_total_run_execution_trace_before. ff_h_be_bd_total_run_execution_trace_before + S (ff_previous_be_bd_total_run_execution_trace) = S ((S (ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_trace_before. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_trace_before * S ((S (ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution) + (ff_previous_be_bd_total_run_execution_trace))) /\ ((((exists ff_h_be_bd_total_run_execution_trace_after. ff_h_be_bd_total_run_execution_trace_after + S (ff_current_be_bd_total_run_execution_trace) = S ((S (S ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_trace_after. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_trace_after * S ((S (S ff_index_be_bd_total_run_execution_trace)) * ff_trace_scale_be_bd_total_run_execution) + (ff_current_be_bd_total_run_execution_trace))) /\ ((((ff_digit_be_bd_total_run_execution_trace = 0) /\ (((exists ff_gap_binary_be_bd_total_run_execution_trace_transition_square. ff_gap_binary_be_bd_total_run_execution_trace_transition_square + S (ff_current_be_bd_total_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_total_run_execution_trace_transition_square_congruence ff_right_binary_be_bd_total_run_execution_trace_transition_square_congruence. (ff_previous_be_bd_total_run_execution_trace * ff_previous_be_bd_total_run_execution_trace) + m * ff_left_binary_be_bd_total_run_execution_trace_transition_square_congruence = (ff_current_be_bd_total_run_execution_trace) + m * ff_right_binary_be_bd_total_run_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_bd_total_run_execution_trace = 1) /\ (((exists ff_gap_binary_be_bd_total_run_execution_trace_transition_multiply. ff_gap_binary_be_bd_total_run_execution_trace_transition_multiply + S (ff_current_be_bd_total_run_execution_trace) = m) /\ (exists ff_left_binary_be_bd_total_run_execution_trace_transition_multiply_congruence ff_right_binary_be_bd_total_run_execution_trace_transition_multiply_congruence. ((ff_previous_be_bd_total_run_execution_trace * ff_previous_be_bd_total_run_execution_trace) * a) + m * ff_left_binary_be_bd_total_run_execution_trace_transition_multiply_congruence = (ff_current_be_bd_total_run_execution_trace) + m * ff_right_binary_be_bd_total_run_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_bd_total_run_execution_terminal. ff_h_be_bd_total_run_execution_terminal + S (r) = S ((S (x)) * ff_trace_scale_be_bd_total_run_execution)) /\ exists ff_q_be_bd_total_run_execution_terminal. ff_trace_code_be_bd_total_run_execution = ff_q_be_bd_total_run_execution_terminal * S ((S (x)) * ff_trace_scale_be_bd_total_run_execution) + (r)))))
  16. 0016specialize binary_modular_execution_exists x1
  17. 0017specialize binary_modular_execution_exists x2
  18. 0018specialize binary_modular_execution_exists a
  19. 0019specialize binary_modular_execution_exists m
  20. 0020specialize binary_modular_execution_exists x
  21. 0021apply binary_modular_execution_exists
  22. 0022exact hmodulus
  23. 0023exact hdigits
  24. 0024cases hexecution
  25. 0025exists x
  26. 0026exists x1
  27. 0027exists x2
  28. 0028exists x3
  29. 0029split
  30. 0030exact hcanonical_witness_witness_witness
  31. 0031split
  32. 0032exact hexecution_witness
  33. 0033specialize binary_modular_exponent_coded_execution_power_correct n
  34. 0034specialize binary_modular_exponent_coded_execution_power_correct a
  35. 0035specialize binary_modular_exponent_coded_execution_power_correct m
  36. 0036specialize binary_modular_exponent_coded_execution_power_correct x
  37. 0037specialize binary_modular_exponent_coded_execution_power_correct x1
  38. 0038specialize binary_modular_exponent_coded_execution_power_correct x2
  39. 0039specialize binary_modular_exponent_coded_execution_power_correct x3
  40. 0040apply binary_modular_exponent_coded_execution_power_correct
  41. 0041exact hmodulus
  42. 0042exact hcanonical_witness_witness_witness
  43. 0043exact hexecution_witness

Separate complete second-wave branches: Full T13 proof · Alpha v27.