TS003A

all_bad_prime_even_valuation_value_eq_transport

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

The universally quantified bad-prime even-valuation invariant transports constructively along equality of natural values.

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 a b. a = b -> (forall ftsp_bad_prime_transport_source ftsp_bad_exponent_transport_source. ((~(ftsp_bad_prime_transport_source = 1) /\ forall frm_prime_left_ftsp_transport_source_prime frm_prime_right_ftsp_transport_source_prime. ftsp_bad_prime_transport_source = frm_prime_left_ftsp_transport_source_prime * frm_prime_right_ftsp_transport_source_prime -> frm_prime_left_ftsp_transport_source_prime = 1 \/ frm_prime_right_ftsp_transport_source_prime = 1)) -> (exists ftsc_four_three_ftsp_transport_source_three. (ftsp_bad_prime_transport_source) = 4 * ftsc_four_three_ftsp_transport_source_three + 3) -> (((exists bpv_gap_ftsp_transport_source_valuation_exponent_bound. bpv_gap_ftsp_transport_source_valuation_exponent_bound + ftsp_bad_exponent_transport_source = (a)) /\ (exists bpv_result_ftsp_transport_source_valuation_selected. ((exists ff_b_ftsp_transport_source_valuation_selected_power ff_c_ftsp_transport_source_valuation_selected_power. ((forall ff_i_ftsp_transport_source_valuation_selected_power_repeat. (exists ff_lt_ftsp_transport_source_valuation_selected_power_repeat_bound. ff_lt_ftsp_transport_source_valuation_selected_power_repeat_bound + S ff_i_ftsp_transport_source_valuation_selected_power_repeat = ftsp_bad_exponent_transport_source) -> (((exists ff_h_ftsp_transport_source_valuation_selected_power_repeat_decoded. ff_h_ftsp_transport_source_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_transport_source) = S ((S (ff_i_ftsp_transport_source_valuation_selected_power_repeat)) * ff_c_ftsp_transport_source_valuation_selected_power)) /\ exists ff_q_ftsp_transport_source_valuation_selected_power_repeat_decoded. ff_b_ftsp_transport_source_valuation_selected_power = ff_q_ftsp_transport_source_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_transport_source_valuation_selected_power_repeat)) * ff_c_ftsp_transport_source_valuation_selected_power) + (ftsp_bad_prime_transport_source)))) /\ (exists ff_u_ftsp_transport_source_valuation_selected_power_product ff_v_ftsp_transport_source_valuation_selected_power_product. ((((exists ff_h_ftsp_transport_source_valuation_selected_power_product_start. ff_h_ftsp_transport_source_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_transport_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_selected_power_product_start. ff_u_ftsp_transport_source_valuation_selected_power_product = ff_q_ftsp_transport_source_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_transport_source_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_transport_source_valuation_selected_power_product_terminal. ff_h_ftsp_transport_source_valuation_selected_power_product_terminal + S (bpv_result_ftsp_transport_source_valuation_selected) = S ((S (ftsp_bad_exponent_transport_source)) * ff_v_ftsp_transport_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_selected_power_product_terminal. ff_u_ftsp_transport_source_valuation_selected_power_product = ff_q_ftsp_transport_source_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_transport_source)) * ff_v_ftsp_transport_source_valuation_selected_power_product) + (bpv_result_ftsp_transport_source_valuation_selected))) /\ forall ff_i_ftsp_transport_source_valuation_selected_power_product. (exists ff_lt_ftsp_transport_source_valuation_selected_power_product_bound. ff_lt_ftsp_transport_source_valuation_selected_power_product_bound + S ff_i_ftsp_transport_source_valuation_selected_power_product = ftsp_bad_exponent_transport_source) -> exists ff_p_ftsp_transport_source_valuation_selected_power_product ff_r_ftsp_transport_source_valuation_selected_power_product ff_s_ftsp_transport_source_valuation_selected_power_product. ((((exists ff_h_ftsp_transport_source_valuation_selected_power_product_factor. ff_h_ftsp_transport_source_valuation_selected_power_product_factor + S (ff_p_ftsp_transport_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_transport_source_valuation_selected_power_product)) * ff_c_ftsp_transport_source_valuation_selected_power)) /\ exists ff_q_ftsp_transport_source_valuation_selected_power_product_factor. ff_b_ftsp_transport_source_valuation_selected_power = ff_q_ftsp_transport_source_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_transport_source_valuation_selected_power_product)) * ff_c_ftsp_transport_source_valuation_selected_power) + (ff_p_ftsp_transport_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_transport_source_valuation_selected_power_product_partial. ff_h_ftsp_transport_source_valuation_selected_power_product_partial + S (ff_r_ftsp_transport_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_transport_source_valuation_selected_power_product)) * ff_v_ftsp_transport_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_selected_power_product_partial. ff_u_ftsp_transport_source_valuation_selected_power_product = ff_q_ftsp_transport_source_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_transport_source_valuation_selected_power_product)) * ff_v_ftsp_transport_source_valuation_selected_power_product) + (ff_r_ftsp_transport_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_transport_source_valuation_selected_power_product_successor. ff_h_ftsp_transport_source_valuation_selected_power_product_successor + S (ff_s_ftsp_transport_source_valuation_selected_power_product) = S ((S (S ff_i_ftsp_transport_source_valuation_selected_power_product)) * ff_v_ftsp_transport_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_selected_power_product_successor. ff_u_ftsp_transport_source_valuation_selected_power_product = ff_q_ftsp_transport_source_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_transport_source_valuation_selected_power_product)) * ff_v_ftsp_transport_source_valuation_selected_power_product) + (ff_s_ftsp_transport_source_valuation_selected_power_product))) /\ ff_s_ftsp_transport_source_valuation_selected_power_product = ff_r_ftsp_transport_source_valuation_selected_power_product * ff_p_ftsp_transport_source_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_transport_source_valuation_selected_divides. (a) = bpv_result_ftsp_transport_source_valuation_selected * bpv_factor_ftsp_transport_source_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_transport_source_valuation. (exists bpv_gap_ftsp_transport_source_valuation_candidate_bound. bpv_gap_ftsp_transport_source_valuation_candidate_bound + bpv_candidate_ftsp_transport_source_valuation = (a)) -> (exists bpv_result_ftsp_transport_source_valuation_candidate. ((exists ff_b_ftsp_transport_source_valuation_candidate_power ff_c_ftsp_transport_source_valuation_candidate_power. ((forall ff_i_ftsp_transport_source_valuation_candidate_power_repeat. (exists ff_lt_ftsp_transport_source_valuation_candidate_power_repeat_bound. ff_lt_ftsp_transport_source_valuation_candidate_power_repeat_bound + S ff_i_ftsp_transport_source_valuation_candidate_power_repeat = bpv_candidate_ftsp_transport_source_valuation) -> (((exists ff_h_ftsp_transport_source_valuation_candidate_power_repeat_decoded. ff_h_ftsp_transport_source_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_transport_source) = S ((S (ff_i_ftsp_transport_source_valuation_candidate_power_repeat)) * ff_c_ftsp_transport_source_valuation_candidate_power)) /\ exists ff_q_ftsp_transport_source_valuation_candidate_power_repeat_decoded. ff_b_ftsp_transport_source_valuation_candidate_power = ff_q_ftsp_transport_source_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_transport_source_valuation_candidate_power_repeat)) * ff_c_ftsp_transport_source_valuation_candidate_power) + (ftsp_bad_prime_transport_source)))) /\ (exists ff_u_ftsp_transport_source_valuation_candidate_power_product ff_v_ftsp_transport_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_transport_source_valuation_candidate_power_product_start. ff_h_ftsp_transport_source_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_transport_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_candidate_power_product_start. ff_u_ftsp_transport_source_valuation_candidate_power_product = ff_q_ftsp_transport_source_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_transport_source_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_transport_source_valuation_candidate_power_product_terminal. ff_h_ftsp_transport_source_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_transport_source_valuation_candidate) = S ((S (bpv_candidate_ftsp_transport_source_valuation)) * ff_v_ftsp_transport_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_candidate_power_product_terminal. ff_u_ftsp_transport_source_valuation_candidate_power_product = ff_q_ftsp_transport_source_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_transport_source_valuation)) * ff_v_ftsp_transport_source_valuation_candidate_power_product) + (bpv_result_ftsp_transport_source_valuation_candidate))) /\ forall ff_i_ftsp_transport_source_valuation_candidate_power_product. (exists ff_lt_ftsp_transport_source_valuation_candidate_power_product_bound. ff_lt_ftsp_transport_source_valuation_candidate_power_product_bound + S ff_i_ftsp_transport_source_valuation_candidate_power_product = bpv_candidate_ftsp_transport_source_valuation) -> exists ff_p_ftsp_transport_source_valuation_candidate_power_product ff_r_ftsp_transport_source_valuation_candidate_power_product ff_s_ftsp_transport_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_transport_source_valuation_candidate_power_product_factor. ff_h_ftsp_transport_source_valuation_candidate_power_product_factor + S (ff_p_ftsp_transport_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_transport_source_valuation_candidate_power_product)) * ff_c_ftsp_transport_source_valuation_candidate_power)) /\ exists ff_q_ftsp_transport_source_valuation_candidate_power_product_factor. ff_b_ftsp_transport_source_valuation_candidate_power = ff_q_ftsp_transport_source_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_transport_source_valuation_candidate_power_product)) * ff_c_ftsp_transport_source_valuation_candidate_power) + (ff_p_ftsp_transport_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_transport_source_valuation_candidate_power_product_partial. ff_h_ftsp_transport_source_valuation_candidate_power_product_partial + S (ff_r_ftsp_transport_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_transport_source_valuation_candidate_power_product)) * ff_v_ftsp_transport_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_candidate_power_product_partial. ff_u_ftsp_transport_source_valuation_candidate_power_product = ff_q_ftsp_transport_source_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_transport_source_valuation_candidate_power_product)) * ff_v_ftsp_transport_source_valuation_candidate_power_product) + (ff_r_ftsp_transport_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_transport_source_valuation_candidate_power_product_successor. ff_h_ftsp_transport_source_valuation_candidate_power_product_successor + S (ff_s_ftsp_transport_source_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_transport_source_valuation_candidate_power_product)) * ff_v_ftsp_transport_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_source_valuation_candidate_power_product_successor. ff_u_ftsp_transport_source_valuation_candidate_power_product = ff_q_ftsp_transport_source_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_transport_source_valuation_candidate_power_product)) * ff_v_ftsp_transport_source_valuation_candidate_power_product) + (ff_s_ftsp_transport_source_valuation_candidate_power_product))) /\ ff_s_ftsp_transport_source_valuation_candidate_power_product = ff_r_ftsp_transport_source_valuation_candidate_power_product * ff_p_ftsp_transport_source_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_transport_source_valuation_candidate_divides. (a) = bpv_result_ftsp_transport_source_valuation_candidate * bpv_factor_ftsp_transport_source_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_transport_source_valuation_maximal. bpv_gap_ftsp_transport_source_valuation_maximal + bpv_candidate_ftsp_transport_source_valuation = ftsp_bad_exponent_transport_source)) -> exists ftsp_bad_half_transport_source. ftsp_bad_exponent_transport_source = ftsp_bad_half_transport_source + ftsp_bad_half_transport_source) -> (forall ftsp_bad_prime_transport_target ftsp_bad_exponent_transport_target. ((~(ftsp_bad_prime_transport_target = 1) /\ forall frm_prime_left_ftsp_transport_target_prime frm_prime_right_ftsp_transport_target_prime. ftsp_bad_prime_transport_target = frm_prime_left_ftsp_transport_target_prime * frm_prime_right_ftsp_transport_target_prime -> frm_prime_left_ftsp_transport_target_prime = 1 \/ frm_prime_right_ftsp_transport_target_prime = 1)) -> (exists ftsc_four_three_ftsp_transport_target_three. (ftsp_bad_prime_transport_target) = 4 * ftsc_four_three_ftsp_transport_target_three + 3) -> (((exists bpv_gap_ftsp_transport_target_valuation_exponent_bound. bpv_gap_ftsp_transport_target_valuation_exponent_bound + ftsp_bad_exponent_transport_target = (b)) /\ (exists bpv_result_ftsp_transport_target_valuation_selected. ((exists ff_b_ftsp_transport_target_valuation_selected_power ff_c_ftsp_transport_target_valuation_selected_power. ((forall ff_i_ftsp_transport_target_valuation_selected_power_repeat. (exists ff_lt_ftsp_transport_target_valuation_selected_power_repeat_bound. ff_lt_ftsp_transport_target_valuation_selected_power_repeat_bound + S ff_i_ftsp_transport_target_valuation_selected_power_repeat = ftsp_bad_exponent_transport_target) -> (((exists ff_h_ftsp_transport_target_valuation_selected_power_repeat_decoded. ff_h_ftsp_transport_target_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_transport_target) = S ((S (ff_i_ftsp_transport_target_valuation_selected_power_repeat)) * ff_c_ftsp_transport_target_valuation_selected_power)) /\ exists ff_q_ftsp_transport_target_valuation_selected_power_repeat_decoded. ff_b_ftsp_transport_target_valuation_selected_power = ff_q_ftsp_transport_target_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_transport_target_valuation_selected_power_repeat)) * ff_c_ftsp_transport_target_valuation_selected_power) + (ftsp_bad_prime_transport_target)))) /\ (exists ff_u_ftsp_transport_target_valuation_selected_power_product ff_v_ftsp_transport_target_valuation_selected_power_product. ((((exists ff_h_ftsp_transport_target_valuation_selected_power_product_start. ff_h_ftsp_transport_target_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_transport_target_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_selected_power_product_start. ff_u_ftsp_transport_target_valuation_selected_power_product = ff_q_ftsp_transport_target_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_transport_target_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_transport_target_valuation_selected_power_product_terminal. ff_h_ftsp_transport_target_valuation_selected_power_product_terminal + S (bpv_result_ftsp_transport_target_valuation_selected) = S ((S (ftsp_bad_exponent_transport_target)) * ff_v_ftsp_transport_target_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_selected_power_product_terminal. ff_u_ftsp_transport_target_valuation_selected_power_product = ff_q_ftsp_transport_target_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_transport_target)) * ff_v_ftsp_transport_target_valuation_selected_power_product) + (bpv_result_ftsp_transport_target_valuation_selected))) /\ forall ff_i_ftsp_transport_target_valuation_selected_power_product. (exists ff_lt_ftsp_transport_target_valuation_selected_power_product_bound. ff_lt_ftsp_transport_target_valuation_selected_power_product_bound + S ff_i_ftsp_transport_target_valuation_selected_power_product = ftsp_bad_exponent_transport_target) -> exists ff_p_ftsp_transport_target_valuation_selected_power_product ff_r_ftsp_transport_target_valuation_selected_power_product ff_s_ftsp_transport_target_valuation_selected_power_product. ((((exists ff_h_ftsp_transport_target_valuation_selected_power_product_factor. ff_h_ftsp_transport_target_valuation_selected_power_product_factor + S (ff_p_ftsp_transport_target_valuation_selected_power_product) = S ((S (ff_i_ftsp_transport_target_valuation_selected_power_product)) * ff_c_ftsp_transport_target_valuation_selected_power)) /\ exists ff_q_ftsp_transport_target_valuation_selected_power_product_factor. ff_b_ftsp_transport_target_valuation_selected_power = ff_q_ftsp_transport_target_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_transport_target_valuation_selected_power_product)) * ff_c_ftsp_transport_target_valuation_selected_power) + (ff_p_ftsp_transport_target_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_transport_target_valuation_selected_power_product_partial. ff_h_ftsp_transport_target_valuation_selected_power_product_partial + S (ff_r_ftsp_transport_target_valuation_selected_power_product) = S ((S (ff_i_ftsp_transport_target_valuation_selected_power_product)) * ff_v_ftsp_transport_target_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_selected_power_product_partial. ff_u_ftsp_transport_target_valuation_selected_power_product = ff_q_ftsp_transport_target_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_transport_target_valuation_selected_power_product)) * ff_v_ftsp_transport_target_valuation_selected_power_product) + (ff_r_ftsp_transport_target_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_transport_target_valuation_selected_power_product_successor. ff_h_ftsp_transport_target_valuation_selected_power_product_successor + S (ff_s_ftsp_transport_target_valuation_selected_power_product) = S ((S (S ff_i_ftsp_transport_target_valuation_selected_power_product)) * ff_v_ftsp_transport_target_valuation_selected_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_selected_power_product_successor. ff_u_ftsp_transport_target_valuation_selected_power_product = ff_q_ftsp_transport_target_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_transport_target_valuation_selected_power_product)) * ff_v_ftsp_transport_target_valuation_selected_power_product) + (ff_s_ftsp_transport_target_valuation_selected_power_product))) /\ ff_s_ftsp_transport_target_valuation_selected_power_product = ff_r_ftsp_transport_target_valuation_selected_power_product * ff_p_ftsp_transport_target_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_transport_target_valuation_selected_divides. (b) = bpv_result_ftsp_transport_target_valuation_selected * bpv_factor_ftsp_transport_target_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_transport_target_valuation. (exists bpv_gap_ftsp_transport_target_valuation_candidate_bound. bpv_gap_ftsp_transport_target_valuation_candidate_bound + bpv_candidate_ftsp_transport_target_valuation = (b)) -> (exists bpv_result_ftsp_transport_target_valuation_candidate. ((exists ff_b_ftsp_transport_target_valuation_candidate_power ff_c_ftsp_transport_target_valuation_candidate_power. ((forall ff_i_ftsp_transport_target_valuation_candidate_power_repeat. (exists ff_lt_ftsp_transport_target_valuation_candidate_power_repeat_bound. ff_lt_ftsp_transport_target_valuation_candidate_power_repeat_bound + S ff_i_ftsp_transport_target_valuation_candidate_power_repeat = bpv_candidate_ftsp_transport_target_valuation) -> (((exists ff_h_ftsp_transport_target_valuation_candidate_power_repeat_decoded. ff_h_ftsp_transport_target_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_transport_target) = S ((S (ff_i_ftsp_transport_target_valuation_candidate_power_repeat)) * ff_c_ftsp_transport_target_valuation_candidate_power)) /\ exists ff_q_ftsp_transport_target_valuation_candidate_power_repeat_decoded. ff_b_ftsp_transport_target_valuation_candidate_power = ff_q_ftsp_transport_target_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_transport_target_valuation_candidate_power_repeat)) * ff_c_ftsp_transport_target_valuation_candidate_power) + (ftsp_bad_prime_transport_target)))) /\ (exists ff_u_ftsp_transport_target_valuation_candidate_power_product ff_v_ftsp_transport_target_valuation_candidate_power_product. ((((exists ff_h_ftsp_transport_target_valuation_candidate_power_product_start. ff_h_ftsp_transport_target_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_transport_target_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_candidate_power_product_start. ff_u_ftsp_transport_target_valuation_candidate_power_product = ff_q_ftsp_transport_target_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_transport_target_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_transport_target_valuation_candidate_power_product_terminal. ff_h_ftsp_transport_target_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_transport_target_valuation_candidate) = S ((S (bpv_candidate_ftsp_transport_target_valuation)) * ff_v_ftsp_transport_target_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_candidate_power_product_terminal. ff_u_ftsp_transport_target_valuation_candidate_power_product = ff_q_ftsp_transport_target_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_transport_target_valuation)) * ff_v_ftsp_transport_target_valuation_candidate_power_product) + (bpv_result_ftsp_transport_target_valuation_candidate))) /\ forall ff_i_ftsp_transport_target_valuation_candidate_power_product. (exists ff_lt_ftsp_transport_target_valuation_candidate_power_product_bound. ff_lt_ftsp_transport_target_valuation_candidate_power_product_bound + S ff_i_ftsp_transport_target_valuation_candidate_power_product = bpv_candidate_ftsp_transport_target_valuation) -> exists ff_p_ftsp_transport_target_valuation_candidate_power_product ff_r_ftsp_transport_target_valuation_candidate_power_product ff_s_ftsp_transport_target_valuation_candidate_power_product. ((((exists ff_h_ftsp_transport_target_valuation_candidate_power_product_factor. ff_h_ftsp_transport_target_valuation_candidate_power_product_factor + S (ff_p_ftsp_transport_target_valuation_candidate_power_product) = S ((S (ff_i_ftsp_transport_target_valuation_candidate_power_product)) * ff_c_ftsp_transport_target_valuation_candidate_power)) /\ exists ff_q_ftsp_transport_target_valuation_candidate_power_product_factor. ff_b_ftsp_transport_target_valuation_candidate_power = ff_q_ftsp_transport_target_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_transport_target_valuation_candidate_power_product)) * ff_c_ftsp_transport_target_valuation_candidate_power) + (ff_p_ftsp_transport_target_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_transport_target_valuation_candidate_power_product_partial. ff_h_ftsp_transport_target_valuation_candidate_power_product_partial + S (ff_r_ftsp_transport_target_valuation_candidate_power_product) = S ((S (ff_i_ftsp_transport_target_valuation_candidate_power_product)) * ff_v_ftsp_transport_target_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_candidate_power_product_partial. ff_u_ftsp_transport_target_valuation_candidate_power_product = ff_q_ftsp_transport_target_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_transport_target_valuation_candidate_power_product)) * ff_v_ftsp_transport_target_valuation_candidate_power_product) + (ff_r_ftsp_transport_target_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_transport_target_valuation_candidate_power_product_successor. ff_h_ftsp_transport_target_valuation_candidate_power_product_successor + S (ff_s_ftsp_transport_target_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_transport_target_valuation_candidate_power_product)) * ff_v_ftsp_transport_target_valuation_candidate_power_product)) /\ exists ff_q_ftsp_transport_target_valuation_candidate_power_product_successor. ff_u_ftsp_transport_target_valuation_candidate_power_product = ff_q_ftsp_transport_target_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_transport_target_valuation_candidate_power_product)) * ff_v_ftsp_transport_target_valuation_candidate_power_product) + (ff_s_ftsp_transport_target_valuation_candidate_power_product))) /\ ff_s_ftsp_transport_target_valuation_candidate_power_product = ff_r_ftsp_transport_target_valuation_candidate_power_product * ff_p_ftsp_transport_target_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_transport_target_valuation_candidate_divides. (b) = bpv_result_ftsp_transport_target_valuation_candidate * bpv_factor_ftsp_transport_target_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_transport_target_valuation_maximal. bpv_gap_ftsp_transport_target_valuation_maximal + bpv_candidate_ftsp_transport_target_valuation = ftsp_bad_exponent_transport_target)) -> exists ftsp_bad_half_transport_target. ftsp_bad_exponent_transport_target = ftsp_bad_half_transport_target + ftsp_bad_half_transport_target)

Constructive proof overview

Generated structural guide

The universally quantified bad-prime even-valuation invariant transports constructively along equality of natural values.

The unchanged tactic script uses 1 declared prerequisite and contains 24 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

power_valuation_value_eq_transport Alpha theorem; checked-use authorized

Direct dependents

TS003C all_bad_prime_even_two_square_sufficiency_bounded

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

24 script commands · 3 reading checkpoints · 1 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.

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–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hequal
  4. L4
    intro hsource
  5. L5
    intro p
  6. L6
    intro e
  7. L7
    intro hprime
  8. L8
    intro hthree
  9. L9
    intro htarget
02Establish hvaluationL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation value eq transport.

  1. L10
    have hvaluation : BoundedPowerValuation(p,a,a,e)Definitions: BoundedPowerValuation
  2. L11
    specialize power_valuation_value_eq_transport p
  3. L12
    specialize power_valuation_value_eq_transport b
  4. L13
    specialize power_valuation_value_eq_transport a
  5. L14
    specialize power_valuation_value_eq_transport e
  6. L15
    apply power_valuation_value_eq_transport
  7. L16
    symm
  8. L17
    exact hequal
  9. L18
    exact htarget
  10. L19
    specialize hsource p
03Use earlier factsL20–24

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

  1. L20
    specialize hsource e
  2. L21
    apply hsource
  3. L22
    exact hprime
  4. L23
    exact hthree
  5. L24
    exact hvaluation

Library-wide reading audit

Original exact command ledger · 24 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hequal
  4. 0004intro hsource
  5. 0005intro p
  6. 0006intro e
  7. 0007intro hprime
  8. 0008intro hthree
  9. 0009intro htarget
  10. 0010have hvaluation : (((exists bpv_gap_ftsp_transport_local_exponent_bound. bpv_gap_ftsp_transport_local_exponent_bound + e = a) /\ (exists bpv_result_ftsp_transport_local_selected. ((exists ff_b_ftsp_transport_local_selected_power ff_c_ftsp_transport_local_selected_power. ((forall ff_i_ftsp_transport_local_selected_power_repeat. (exists ff_lt_ftsp_transport_local_selected_power_repeat_bound. ff_lt_ftsp_transport_local_selected_power_repeat_bound + S ff_i_ftsp_transport_local_selected_power_repeat = e) -> (((exists ff_h_ftsp_transport_local_selected_power_repeat_decoded. ff_h_ftsp_transport_local_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_transport_local_selected_power_repeat)) * ff_c_ftsp_transport_local_selected_power)) /\ exists ff_q_ftsp_transport_local_selected_power_repeat_decoded. ff_b_ftsp_transport_local_selected_power = ff_q_ftsp_transport_local_selected_power_repeat_decoded * S ((S (ff_i_ftsp_transport_local_selected_power_repeat)) * ff_c_ftsp_transport_local_selected_power) + (p)))) /\ (exists ff_u_ftsp_transport_local_selected_power_product ff_v_ftsp_transport_local_selected_power_product. ((((exists ff_h_ftsp_transport_local_selected_power_product_start. ff_h_ftsp_transport_local_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_transport_local_selected_power_product)) /\ exists ff_q_ftsp_transport_local_selected_power_product_start. ff_u_ftsp_transport_local_selected_power_product = ff_q_ftsp_transport_local_selected_power_product_start * S ((S (0)) * ff_v_ftsp_transport_local_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_transport_local_selected_power_product_terminal. ff_h_ftsp_transport_local_selected_power_product_terminal + S (bpv_result_ftsp_transport_local_selected) = S ((S (e)) * ff_v_ftsp_transport_local_selected_power_product)) /\ exists ff_q_ftsp_transport_local_selected_power_product_terminal. ff_u_ftsp_transport_local_selected_power_product = ff_q_ftsp_transport_local_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_transport_local_selected_power_product) + (bpv_result_ftsp_transport_local_selected))) /\ forall ff_i_ftsp_transport_local_selected_power_product. (exists ff_lt_ftsp_transport_local_selected_power_product_bound. ff_lt_ftsp_transport_local_selected_power_product_bound + S ff_i_ftsp_transport_local_selected_power_product = e) -> exists ff_p_ftsp_transport_local_selected_power_product ff_r_ftsp_transport_local_selected_power_product ff_s_ftsp_transport_local_selected_power_product. ((((exists ff_h_ftsp_transport_local_selected_power_product_factor. ff_h_ftsp_transport_local_selected_power_product_factor + S (ff_p_ftsp_transport_local_selected_power_product) = S ((S (ff_i_ftsp_transport_local_selected_power_product)) * ff_c_ftsp_transport_local_selected_power)) /\ exists ff_q_ftsp_transport_local_selected_power_product_factor. ff_b_ftsp_transport_local_selected_power = ff_q_ftsp_transport_local_selected_power_product_factor * S ((S (ff_i_ftsp_transport_local_selected_power_product)) * ff_c_ftsp_transport_local_selected_power) + (ff_p_ftsp_transport_local_selected_power_product))) /\ ((((exists ff_h_ftsp_transport_local_selected_power_product_partial. ff_h_ftsp_transport_local_selected_power_product_partial + S (ff_r_ftsp_transport_local_selected_power_product) = S ((S (ff_i_ftsp_transport_local_selected_power_product)) * ff_v_ftsp_transport_local_selected_power_product)) /\ exists ff_q_ftsp_transport_local_selected_power_product_partial. ff_u_ftsp_transport_local_selected_power_product = ff_q_ftsp_transport_local_selected_power_product_partial * S ((S (ff_i_ftsp_transport_local_selected_power_product)) * ff_v_ftsp_transport_local_selected_power_product) + (ff_r_ftsp_transport_local_selected_power_product))) /\ ((((exists ff_h_ftsp_transport_local_selected_power_product_successor. ff_h_ftsp_transport_local_selected_power_product_successor + S (ff_s_ftsp_transport_local_selected_power_product) = S ((S (S ff_i_ftsp_transport_local_selected_power_product)) * ff_v_ftsp_transport_local_selected_power_product)) /\ exists ff_q_ftsp_transport_local_selected_power_product_successor. ff_u_ftsp_transport_local_selected_power_product = ff_q_ftsp_transport_local_selected_power_product_successor * S ((S (S ff_i_ftsp_transport_local_selected_power_product)) * ff_v_ftsp_transport_local_selected_power_product) + (ff_s_ftsp_transport_local_selected_power_product))) /\ ff_s_ftsp_transport_local_selected_power_product = ff_r_ftsp_transport_local_selected_power_product * ff_p_ftsp_transport_local_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_transport_local_selected_divides. a = bpv_result_ftsp_transport_local_selected * bpv_factor_ftsp_transport_local_selected_divides)))) /\ forall bpv_candidate_ftsp_transport_local. (exists bpv_gap_ftsp_transport_local_candidate_bound. bpv_gap_ftsp_transport_local_candidate_bound + bpv_candidate_ftsp_transport_local = a) -> (exists bpv_result_ftsp_transport_local_candidate. ((exists ff_b_ftsp_transport_local_candidate_power ff_c_ftsp_transport_local_candidate_power. ((forall ff_i_ftsp_transport_local_candidate_power_repeat. (exists ff_lt_ftsp_transport_local_candidate_power_repeat_bound. ff_lt_ftsp_transport_local_candidate_power_repeat_bound + S ff_i_ftsp_transport_local_candidate_power_repeat = bpv_candidate_ftsp_transport_local) -> (((exists ff_h_ftsp_transport_local_candidate_power_repeat_decoded. ff_h_ftsp_transport_local_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_transport_local_candidate_power_repeat)) * ff_c_ftsp_transport_local_candidate_power)) /\ exists ff_q_ftsp_transport_local_candidate_power_repeat_decoded. ff_b_ftsp_transport_local_candidate_power = ff_q_ftsp_transport_local_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_transport_local_candidate_power_repeat)) * ff_c_ftsp_transport_local_candidate_power) + (p)))) /\ (exists ff_u_ftsp_transport_local_candidate_power_product ff_v_ftsp_transport_local_candidate_power_product. ((((exists ff_h_ftsp_transport_local_candidate_power_product_start. ff_h_ftsp_transport_local_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_transport_local_candidate_power_product)) /\ exists ff_q_ftsp_transport_local_candidate_power_product_start. ff_u_ftsp_transport_local_candidate_power_product = ff_q_ftsp_transport_local_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_transport_local_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_transport_local_candidate_power_product_terminal. ff_h_ftsp_transport_local_candidate_power_product_terminal + S (bpv_result_ftsp_transport_local_candidate) = S ((S (bpv_candidate_ftsp_transport_local)) * ff_v_ftsp_transport_local_candidate_power_product)) /\ exists ff_q_ftsp_transport_local_candidate_power_product_terminal. ff_u_ftsp_transport_local_candidate_power_product = ff_q_ftsp_transport_local_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_transport_local)) * ff_v_ftsp_transport_local_candidate_power_product) + (bpv_result_ftsp_transport_local_candidate))) /\ forall ff_i_ftsp_transport_local_candidate_power_product. (exists ff_lt_ftsp_transport_local_candidate_power_product_bound. ff_lt_ftsp_transport_local_candidate_power_product_bound + S ff_i_ftsp_transport_local_candidate_power_product = bpv_candidate_ftsp_transport_local) -> exists ff_p_ftsp_transport_local_candidate_power_product ff_r_ftsp_transport_local_candidate_power_product ff_s_ftsp_transport_local_candidate_power_product. ((((exists ff_h_ftsp_transport_local_candidate_power_product_factor. ff_h_ftsp_transport_local_candidate_power_product_factor + S (ff_p_ftsp_transport_local_candidate_power_product) = S ((S (ff_i_ftsp_transport_local_candidate_power_product)) * ff_c_ftsp_transport_local_candidate_power)) /\ exists ff_q_ftsp_transport_local_candidate_power_product_factor. ff_b_ftsp_transport_local_candidate_power = ff_q_ftsp_transport_local_candidate_power_product_factor * S ((S (ff_i_ftsp_transport_local_candidate_power_product)) * ff_c_ftsp_transport_local_candidate_power) + (ff_p_ftsp_transport_local_candidate_power_product))) /\ ((((exists ff_h_ftsp_transport_local_candidate_power_product_partial. ff_h_ftsp_transport_local_candidate_power_product_partial + S (ff_r_ftsp_transport_local_candidate_power_product) = S ((S (ff_i_ftsp_transport_local_candidate_power_product)) * ff_v_ftsp_transport_local_candidate_power_product)) /\ exists ff_q_ftsp_transport_local_candidate_power_product_partial. ff_u_ftsp_transport_local_candidate_power_product = ff_q_ftsp_transport_local_candidate_power_product_partial * S ((S (ff_i_ftsp_transport_local_candidate_power_product)) * ff_v_ftsp_transport_local_candidate_power_product) + (ff_r_ftsp_transport_local_candidate_power_product))) /\ ((((exists ff_h_ftsp_transport_local_candidate_power_product_successor. ff_h_ftsp_transport_local_candidate_power_product_successor + S (ff_s_ftsp_transport_local_candidate_power_product) = S ((S (S ff_i_ftsp_transport_local_candidate_power_product)) * ff_v_ftsp_transport_local_candidate_power_product)) /\ exists ff_q_ftsp_transport_local_candidate_power_product_successor. ff_u_ftsp_transport_local_candidate_power_product = ff_q_ftsp_transport_local_candidate_power_product_successor * S ((S (S ff_i_ftsp_transport_local_candidate_power_product)) * ff_v_ftsp_transport_local_candidate_power_product) + (ff_s_ftsp_transport_local_candidate_power_product))) /\ ff_s_ftsp_transport_local_candidate_power_product = ff_r_ftsp_transport_local_candidate_power_product * ff_p_ftsp_transport_local_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_transport_local_candidate_divides. a = bpv_result_ftsp_transport_local_candidate * bpv_factor_ftsp_transport_local_candidate_divides))) -> (exists bpv_gap_ftsp_transport_local_maximal. bpv_gap_ftsp_transport_local_maximal + bpv_candidate_ftsp_transport_local = e))
  11. 0011specialize power_valuation_value_eq_transport p
  12. 0012specialize power_valuation_value_eq_transport b
  13. 0013specialize power_valuation_value_eq_transport a
  14. 0014specialize power_valuation_value_eq_transport e
  15. 0015apply power_valuation_value_eq_transport
  16. 0016symm
  17. 0017exact hequal
  18. 0018exact htarget
  19. 0019specialize hsource p
  20. 0020specialize hsource e
  21. 0021apply hsource
  22. 0022exact hprime
  23. 0023exact hthree
  24. 0024exact hvaluation