MK0003

beta_valuation_prefix_last

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

Each actual last table entry has the exact canonical valuation of its actual decoded factor.

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 p b c vb vc l a e. (forall mkm_index_last_source. (exists mkm_lt_last_source_bound. mkm_lt_last_source_bound + S (mkm_index_last_source) = (S l)) -> (exists mkm_value_last_source_point mkm_exponent_last_source_point. (((exists fs_h_mkm_last_source_point_source. fs_h_mkm_last_source_point_source + S (mkm_value_last_source_point) = S ((S (mkm_index_last_source)) * c)) /\ exists fs_q_mkm_last_source_point_source. b = fs_q_mkm_last_source_point_source * S ((S (mkm_index_last_source)) * c) + (mkm_value_last_source_point))) /\ ((((exists fs_h_mkm_last_source_point_decoded. fs_h_mkm_last_source_point_decoded + S (mkm_exponent_last_source_point) = S ((S (mkm_index_last_source)) * vc)) /\ exists fs_q_mkm_last_source_point_decoded. vb = fs_q_mkm_last_source_point_decoded * S ((S (mkm_index_last_source)) * vc) + (mkm_exponent_last_source_point))) /\ (((exists bpv_gap_mkm_last_source_point_valuation_exponent_bound. bpv_gap_mkm_last_source_point_valuation_exponent_bound + mkm_exponent_last_source_point = (mkm_value_last_source_point)) /\ (exists bpv_result_mkm_last_source_point_valuation_selected. ((exists ff_b_mkm_last_source_point_valuation_selected_power ff_c_mkm_last_source_point_valuation_selected_power. ((forall ff_i_mkm_last_source_point_valuation_selected_power_repeat. (exists ff_lt_mkm_last_source_point_valuation_selected_power_repeat_bound. ff_lt_mkm_last_source_point_valuation_selected_power_repeat_bound + S ff_i_mkm_last_source_point_valuation_selected_power_repeat = mkm_exponent_last_source_point) -> (((exists ff_h_mkm_last_source_point_valuation_selected_power_repeat_decoded. ff_h_mkm_last_source_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_last_source_point_valuation_selected_power_repeat)) * ff_c_mkm_last_source_point_valuation_selected_power)) /\ exists ff_q_mkm_last_source_point_valuation_selected_power_repeat_decoded. ff_b_mkm_last_source_point_valuation_selected_power = ff_q_mkm_last_source_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_last_source_point_valuation_selected_power_repeat)) * ff_c_mkm_last_source_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_last_source_point_valuation_selected_power_product ff_v_mkm_last_source_point_valuation_selected_power_product. ((((exists ff_h_mkm_last_source_point_valuation_selected_power_product_start. ff_h_mkm_last_source_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_last_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_selected_power_product_start. ff_u_mkm_last_source_point_valuation_selected_power_product = ff_q_mkm_last_source_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_last_source_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_last_source_point_valuation_selected_power_product_terminal. ff_h_mkm_last_source_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_last_source_point_valuation_selected) = S ((S (mkm_exponent_last_source_point)) * ff_v_mkm_last_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_selected_power_product_terminal. ff_u_mkm_last_source_point_valuation_selected_power_product = ff_q_mkm_last_source_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_last_source_point)) * ff_v_mkm_last_source_point_valuation_selected_power_product) + (bpv_result_mkm_last_source_point_valuation_selected))) /\ forall ff_i_mkm_last_source_point_valuation_selected_power_product. (exists ff_lt_mkm_last_source_point_valuation_selected_power_product_bound. ff_lt_mkm_last_source_point_valuation_selected_power_product_bound + S ff_i_mkm_last_source_point_valuation_selected_power_product = mkm_exponent_last_source_point) -> exists ff_p_mkm_last_source_point_valuation_selected_power_product ff_r_mkm_last_source_point_valuation_selected_power_product ff_s_mkm_last_source_point_valuation_selected_power_product. ((((exists ff_h_mkm_last_source_point_valuation_selected_power_product_factor. ff_h_mkm_last_source_point_valuation_selected_power_product_factor + S (ff_p_mkm_last_source_point_valuation_selected_power_product) = S ((S (ff_i_mkm_last_source_point_valuation_selected_power_product)) * ff_c_mkm_last_source_point_valuation_selected_power)) /\ exists ff_q_mkm_last_source_point_valuation_selected_power_product_factor. ff_b_mkm_last_source_point_valuation_selected_power = ff_q_mkm_last_source_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_last_source_point_valuation_selected_power_product)) * ff_c_mkm_last_source_point_valuation_selected_power) + (ff_p_mkm_last_source_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_last_source_point_valuation_selected_power_product_partial. ff_h_mkm_last_source_point_valuation_selected_power_product_partial + S (ff_r_mkm_last_source_point_valuation_selected_power_product) = S ((S (ff_i_mkm_last_source_point_valuation_selected_power_product)) * ff_v_mkm_last_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_selected_power_product_partial. ff_u_mkm_last_source_point_valuation_selected_power_product = ff_q_mkm_last_source_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_last_source_point_valuation_selected_power_product)) * ff_v_mkm_last_source_point_valuation_selected_power_product) + (ff_r_mkm_last_source_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_last_source_point_valuation_selected_power_product_successor. ff_h_mkm_last_source_point_valuation_selected_power_product_successor + S (ff_s_mkm_last_source_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_last_source_point_valuation_selected_power_product)) * ff_v_mkm_last_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_selected_power_product_successor. ff_u_mkm_last_source_point_valuation_selected_power_product = ff_q_mkm_last_source_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_last_source_point_valuation_selected_power_product)) * ff_v_mkm_last_source_point_valuation_selected_power_product) + (ff_s_mkm_last_source_point_valuation_selected_power_product))) /\ ff_s_mkm_last_source_point_valuation_selected_power_product = ff_r_mkm_last_source_point_valuation_selected_power_product * ff_p_mkm_last_source_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_last_source_point_valuation_selected_divides. (mkm_value_last_source_point) = bpv_result_mkm_last_source_point_valuation_selected * bpv_factor_mkm_last_source_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_last_source_point_valuation. (exists bpv_gap_mkm_last_source_point_valuation_candidate_bound. bpv_gap_mkm_last_source_point_valuation_candidate_bound + bpv_candidate_mkm_last_source_point_valuation = (mkm_value_last_source_point)) -> (exists bpv_result_mkm_last_source_point_valuation_candidate. ((exists ff_b_mkm_last_source_point_valuation_candidate_power ff_c_mkm_last_source_point_valuation_candidate_power. ((forall ff_i_mkm_last_source_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_last_source_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_last_source_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_last_source_point_valuation_candidate_power_repeat = bpv_candidate_mkm_last_source_point_valuation) -> (((exists ff_h_mkm_last_source_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_last_source_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_last_source_point_valuation_candidate_power_repeat)) * ff_c_mkm_last_source_point_valuation_candidate_power)) /\ exists ff_q_mkm_last_source_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_last_source_point_valuation_candidate_power = ff_q_mkm_last_source_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_last_source_point_valuation_candidate_power_repeat)) * ff_c_mkm_last_source_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_last_source_point_valuation_candidate_power_product ff_v_mkm_last_source_point_valuation_candidate_power_product. ((((exists ff_h_mkm_last_source_point_valuation_candidate_power_product_start. ff_h_mkm_last_source_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_last_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_candidate_power_product_start. ff_u_mkm_last_source_point_valuation_candidate_power_product = ff_q_mkm_last_source_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_last_source_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_last_source_point_valuation_candidate_power_product_terminal. ff_h_mkm_last_source_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_last_source_point_valuation_candidate) = S ((S (bpv_candidate_mkm_last_source_point_valuation)) * ff_v_mkm_last_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_candidate_power_product_terminal. ff_u_mkm_last_source_point_valuation_candidate_power_product = ff_q_mkm_last_source_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_last_source_point_valuation)) * ff_v_mkm_last_source_point_valuation_candidate_power_product) + (bpv_result_mkm_last_source_point_valuation_candidate))) /\ forall ff_i_mkm_last_source_point_valuation_candidate_power_product. (exists ff_lt_mkm_last_source_point_valuation_candidate_power_product_bound. ff_lt_mkm_last_source_point_valuation_candidate_power_product_bound + S ff_i_mkm_last_source_point_valuation_candidate_power_product = bpv_candidate_mkm_last_source_point_valuation) -> exists ff_p_mkm_last_source_point_valuation_candidate_power_product ff_r_mkm_last_source_point_valuation_candidate_power_product ff_s_mkm_last_source_point_valuation_candidate_power_product. ((((exists ff_h_mkm_last_source_point_valuation_candidate_power_product_factor. ff_h_mkm_last_source_point_valuation_candidate_power_product_factor + S (ff_p_mkm_last_source_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_last_source_point_valuation_candidate_power_product)) * ff_c_mkm_last_source_point_valuation_candidate_power)) /\ exists ff_q_mkm_last_source_point_valuation_candidate_power_product_factor. ff_b_mkm_last_source_point_valuation_candidate_power = ff_q_mkm_last_source_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_last_source_point_valuation_candidate_power_product)) * ff_c_mkm_last_source_point_valuation_candidate_power) + (ff_p_mkm_last_source_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_last_source_point_valuation_candidate_power_product_partial. ff_h_mkm_last_source_point_valuation_candidate_power_product_partial + S (ff_r_mkm_last_source_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_last_source_point_valuation_candidate_power_product)) * ff_v_mkm_last_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_candidate_power_product_partial. ff_u_mkm_last_source_point_valuation_candidate_power_product = ff_q_mkm_last_source_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_last_source_point_valuation_candidate_power_product)) * ff_v_mkm_last_source_point_valuation_candidate_power_product) + (ff_r_mkm_last_source_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_last_source_point_valuation_candidate_power_product_successor. ff_h_mkm_last_source_point_valuation_candidate_power_product_successor + S (ff_s_mkm_last_source_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_last_source_point_valuation_candidate_power_product)) * ff_v_mkm_last_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_source_point_valuation_candidate_power_product_successor. ff_u_mkm_last_source_point_valuation_candidate_power_product = ff_q_mkm_last_source_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_last_source_point_valuation_candidate_power_product)) * ff_v_mkm_last_source_point_valuation_candidate_power_product) + (ff_s_mkm_last_source_point_valuation_candidate_power_product))) /\ ff_s_mkm_last_source_point_valuation_candidate_power_product = ff_r_mkm_last_source_point_valuation_candidate_power_product * ff_p_mkm_last_source_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_last_source_point_valuation_candidate_divides. (mkm_value_last_source_point) = bpv_result_mkm_last_source_point_valuation_candidate * bpv_factor_mkm_last_source_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_last_source_point_valuation_maximal. bpv_gap_mkm_last_source_point_valuation_maximal + bpv_candidate_mkm_last_source_point_valuation = mkm_exponent_last_source_point))))) -> (((exists fs_h_mkm_last_a. fs_h_mkm_last_a + S (a) = S ((S (l)) * c)) /\ exists fs_q_mkm_last_a. b = fs_q_mkm_last_a * S ((S (l)) * c) + (a))) -> (((exists fs_h_mkm_last_e. fs_h_mkm_last_e + S (e) = S ((S (l)) * vc)) /\ exists fs_q_mkm_last_e. vb = fs_q_mkm_last_e * S ((S (l)) * vc) + (e))) -> (((exists bpv_gap_mkm_last_result_exponent_bound. bpv_gap_mkm_last_result_exponent_bound + e = (a)) /\ (exists bpv_result_mkm_last_result_selected. ((exists ff_b_mkm_last_result_selected_power ff_c_mkm_last_result_selected_power. ((forall ff_i_mkm_last_result_selected_power_repeat. (exists ff_lt_mkm_last_result_selected_power_repeat_bound. ff_lt_mkm_last_result_selected_power_repeat_bound + S ff_i_mkm_last_result_selected_power_repeat = e) -> (((exists ff_h_mkm_last_result_selected_power_repeat_decoded. ff_h_mkm_last_result_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_last_result_selected_power_repeat)) * ff_c_mkm_last_result_selected_power)) /\ exists ff_q_mkm_last_result_selected_power_repeat_decoded. ff_b_mkm_last_result_selected_power = ff_q_mkm_last_result_selected_power_repeat_decoded * S ((S (ff_i_mkm_last_result_selected_power_repeat)) * ff_c_mkm_last_result_selected_power) + (p)))) /\ (exists ff_u_mkm_last_result_selected_power_product ff_v_mkm_last_result_selected_power_product. ((((exists ff_h_mkm_last_result_selected_power_product_start. ff_h_mkm_last_result_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_last_result_selected_power_product)) /\ exists ff_q_mkm_last_result_selected_power_product_start. ff_u_mkm_last_result_selected_power_product = ff_q_mkm_last_result_selected_power_product_start * S ((S (0)) * ff_v_mkm_last_result_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_last_result_selected_power_product_terminal. ff_h_mkm_last_result_selected_power_product_terminal + S (bpv_result_mkm_last_result_selected) = S ((S (e)) * ff_v_mkm_last_result_selected_power_product)) /\ exists ff_q_mkm_last_result_selected_power_product_terminal. ff_u_mkm_last_result_selected_power_product = ff_q_mkm_last_result_selected_power_product_terminal * S ((S (e)) * ff_v_mkm_last_result_selected_power_product) + (bpv_result_mkm_last_result_selected))) /\ forall ff_i_mkm_last_result_selected_power_product. (exists ff_lt_mkm_last_result_selected_power_product_bound. ff_lt_mkm_last_result_selected_power_product_bound + S ff_i_mkm_last_result_selected_power_product = e) -> exists ff_p_mkm_last_result_selected_power_product ff_r_mkm_last_result_selected_power_product ff_s_mkm_last_result_selected_power_product. ((((exists ff_h_mkm_last_result_selected_power_product_factor. ff_h_mkm_last_result_selected_power_product_factor + S (ff_p_mkm_last_result_selected_power_product) = S ((S (ff_i_mkm_last_result_selected_power_product)) * ff_c_mkm_last_result_selected_power)) /\ exists ff_q_mkm_last_result_selected_power_product_factor. ff_b_mkm_last_result_selected_power = ff_q_mkm_last_result_selected_power_product_factor * S ((S (ff_i_mkm_last_result_selected_power_product)) * ff_c_mkm_last_result_selected_power) + (ff_p_mkm_last_result_selected_power_product))) /\ ((((exists ff_h_mkm_last_result_selected_power_product_partial. ff_h_mkm_last_result_selected_power_product_partial + S (ff_r_mkm_last_result_selected_power_product) = S ((S (ff_i_mkm_last_result_selected_power_product)) * ff_v_mkm_last_result_selected_power_product)) /\ exists ff_q_mkm_last_result_selected_power_product_partial. ff_u_mkm_last_result_selected_power_product = ff_q_mkm_last_result_selected_power_product_partial * S ((S (ff_i_mkm_last_result_selected_power_product)) * ff_v_mkm_last_result_selected_power_product) + (ff_r_mkm_last_result_selected_power_product))) /\ ((((exists ff_h_mkm_last_result_selected_power_product_successor. ff_h_mkm_last_result_selected_power_product_successor + S (ff_s_mkm_last_result_selected_power_product) = S ((S (S ff_i_mkm_last_result_selected_power_product)) * ff_v_mkm_last_result_selected_power_product)) /\ exists ff_q_mkm_last_result_selected_power_product_successor. ff_u_mkm_last_result_selected_power_product = ff_q_mkm_last_result_selected_power_product_successor * S ((S (S ff_i_mkm_last_result_selected_power_product)) * ff_v_mkm_last_result_selected_power_product) + (ff_s_mkm_last_result_selected_power_product))) /\ ff_s_mkm_last_result_selected_power_product = ff_r_mkm_last_result_selected_power_product * ff_p_mkm_last_result_selected_power_product)))))))) /\ (exists bpv_factor_mkm_last_result_selected_divides. (a) = bpv_result_mkm_last_result_selected * bpv_factor_mkm_last_result_selected_divides)))) /\ forall bpv_candidate_mkm_last_result. (exists bpv_gap_mkm_last_result_candidate_bound. bpv_gap_mkm_last_result_candidate_bound + bpv_candidate_mkm_last_result = (a)) -> (exists bpv_result_mkm_last_result_candidate. ((exists ff_b_mkm_last_result_candidate_power ff_c_mkm_last_result_candidate_power. ((forall ff_i_mkm_last_result_candidate_power_repeat. (exists ff_lt_mkm_last_result_candidate_power_repeat_bound. ff_lt_mkm_last_result_candidate_power_repeat_bound + S ff_i_mkm_last_result_candidate_power_repeat = bpv_candidate_mkm_last_result) -> (((exists ff_h_mkm_last_result_candidate_power_repeat_decoded. ff_h_mkm_last_result_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_last_result_candidate_power_repeat)) * ff_c_mkm_last_result_candidate_power)) /\ exists ff_q_mkm_last_result_candidate_power_repeat_decoded. ff_b_mkm_last_result_candidate_power = ff_q_mkm_last_result_candidate_power_repeat_decoded * S ((S (ff_i_mkm_last_result_candidate_power_repeat)) * ff_c_mkm_last_result_candidate_power) + (p)))) /\ (exists ff_u_mkm_last_result_candidate_power_product ff_v_mkm_last_result_candidate_power_product. ((((exists ff_h_mkm_last_result_candidate_power_product_start. ff_h_mkm_last_result_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_last_result_candidate_power_product)) /\ exists ff_q_mkm_last_result_candidate_power_product_start. ff_u_mkm_last_result_candidate_power_product = ff_q_mkm_last_result_candidate_power_product_start * S ((S (0)) * ff_v_mkm_last_result_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_last_result_candidate_power_product_terminal. ff_h_mkm_last_result_candidate_power_product_terminal + S (bpv_result_mkm_last_result_candidate) = S ((S (bpv_candidate_mkm_last_result)) * ff_v_mkm_last_result_candidate_power_product)) /\ exists ff_q_mkm_last_result_candidate_power_product_terminal. ff_u_mkm_last_result_candidate_power_product = ff_q_mkm_last_result_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_last_result)) * ff_v_mkm_last_result_candidate_power_product) + (bpv_result_mkm_last_result_candidate))) /\ forall ff_i_mkm_last_result_candidate_power_product. (exists ff_lt_mkm_last_result_candidate_power_product_bound. ff_lt_mkm_last_result_candidate_power_product_bound + S ff_i_mkm_last_result_candidate_power_product = bpv_candidate_mkm_last_result) -> exists ff_p_mkm_last_result_candidate_power_product ff_r_mkm_last_result_candidate_power_product ff_s_mkm_last_result_candidate_power_product. ((((exists ff_h_mkm_last_result_candidate_power_product_factor. ff_h_mkm_last_result_candidate_power_product_factor + S (ff_p_mkm_last_result_candidate_power_product) = S ((S (ff_i_mkm_last_result_candidate_power_product)) * ff_c_mkm_last_result_candidate_power)) /\ exists ff_q_mkm_last_result_candidate_power_product_factor. ff_b_mkm_last_result_candidate_power = ff_q_mkm_last_result_candidate_power_product_factor * S ((S (ff_i_mkm_last_result_candidate_power_product)) * ff_c_mkm_last_result_candidate_power) + (ff_p_mkm_last_result_candidate_power_product))) /\ ((((exists ff_h_mkm_last_result_candidate_power_product_partial. ff_h_mkm_last_result_candidate_power_product_partial + S (ff_r_mkm_last_result_candidate_power_product) = S ((S (ff_i_mkm_last_result_candidate_power_product)) * ff_v_mkm_last_result_candidate_power_product)) /\ exists ff_q_mkm_last_result_candidate_power_product_partial. ff_u_mkm_last_result_candidate_power_product = ff_q_mkm_last_result_candidate_power_product_partial * S ((S (ff_i_mkm_last_result_candidate_power_product)) * ff_v_mkm_last_result_candidate_power_product) + (ff_r_mkm_last_result_candidate_power_product))) /\ ((((exists ff_h_mkm_last_result_candidate_power_product_successor. ff_h_mkm_last_result_candidate_power_product_successor + S (ff_s_mkm_last_result_candidate_power_product) = S ((S (S ff_i_mkm_last_result_candidate_power_product)) * ff_v_mkm_last_result_candidate_power_product)) /\ exists ff_q_mkm_last_result_candidate_power_product_successor. ff_u_mkm_last_result_candidate_power_product = ff_q_mkm_last_result_candidate_power_product_successor * S ((S (S ff_i_mkm_last_result_candidate_power_product)) * ff_v_mkm_last_result_candidate_power_product) + (ff_s_mkm_last_result_candidate_power_product))) /\ ff_s_mkm_last_result_candidate_power_product = ff_r_mkm_last_result_candidate_power_product * ff_p_mkm_last_result_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_last_result_candidate_divides. (a) = bpv_result_mkm_last_result_candidate * bpv_factor_mkm_last_result_candidate_divides))) -> (exists bpv_gap_mkm_last_result_maximal. bpv_gap_mkm_last_result_maximal + bpv_candidate_mkm_last_result = e))

Constructive proof overview

Generated structural guide

Each actual last table entry has the exact canonical valuation of its actual decoded factor.

The unchanged tactic script uses 2 declared prerequisites and contains 49 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_refl Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

MK0006 beta_prime_product_valuation_eq_sum

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

49 script commands · 8 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.

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

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro vb
  5. L5
    intro vc
  6. L6
    intro l
  7. L7
    intro a
  8. L8
    intro e
  9. L9
    intro h
  10. L10
    intro ha
02Fix variables and assumptionsL11–11

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

  1. L11
    intro he
03Establish hpointL12–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h.

  1. L12
    have hpoint : ∃ mkm_value_last_point. ∃ mkm_exponent_last_point. BetaAt(b,c,l,mkm_value_last_point) ∧ (BetaAt(vb,vc,l,mkm_exponent_last_point) ∧ BoundedPowerValuation(p,mkm_value_last_point,mkm_value_last_point,mkm_exponent_last_point))Definitions: BetaAtBoundedPowerValuation
  2. L13
    specialize h l
  3. L14
    apply h
  4. L15
    specialize le_refl (S l)
  5. L16
    apply le_refl
04Separate the logical casesL17–20

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

  1. L17
    cases hpoint
  2. L18
    cases hpoint_witness
  3. L19
    cases hpoint_witness_witness
  4. L20
    cases hpoint_witness_witness_right
05Establish hvalueL21–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L21
    have hvalue : x = a
  2. L22
    specialize beta_at_unique b
  3. L23
    specialize beta_at_unique c
  4. L24
    specialize beta_at_unique l
  5. L25
    specialize beta_at_unique x
  6. L26
    specialize beta_at_unique a
  7. L27
    apply beta_at_unique
  8. L28
    exact hpoint_witness_witness_left
  9. L29
    exact ha
06Establish hexponentL30–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L30
    have hexponent : x1 = e
  2. L31
    specialize beta_at_unique vb
  3. L32
    specialize beta_at_unique vc
  4. L33
    specialize beta_at_unique l
  5. L34
    specialize beta_at_unique x1
  6. L35
    specialize beta_at_unique e
  7. L36
    apply beta_at_unique
  8. L37
    exact hpoint_witness_witness_right_left
  9. L38
    exact he
  10. L39
    rewrite hvalue at hpoint_witness_witness_right_right
07Calculate and transport equalitiesL40–48

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L40
    rewrite hvalue at hpoint_witness_witness_right_right
  2. L41
    rewrite hvalue at hpoint_witness_witness_right_right
  3. L42
    rewrite hvalue at hpoint_witness_witness_right_right
  4. L43
    rewrite hexponent at hpoint_witness_witness_right_right
  5. L44
    rewrite hexponent at hpoint_witness_witness_right_right
  6. L45
    rewrite hexponent at hpoint_witness_witness_right_right
  7. L46
    rewrite hexponent at hpoint_witness_witness_right_right
  8. L47
    rewrite hexponent at hpoint_witness_witness_right_right
  9. L48
    rewrite hexponent at hpoint_witness_witness_right_right
08Use earlier factsL49–49

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

  1. L49
    exact hpoint_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 49 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro vb
  5. 0005intro vc
  6. 0006intro l
  7. 0007intro a
  8. 0008intro e
  9. 0009intro h
  10. 0010intro ha
  11. 0011intro he
  12. 0012have hpoint : exists mkm_value_last_point mkm_exponent_last_point. (((exists fs_h_mkm_last_point_source. fs_h_mkm_last_point_source + S (mkm_value_last_point) = S ((S (l)) * c)) /\ exists fs_q_mkm_last_point_source. b = fs_q_mkm_last_point_source * S ((S (l)) * c) + (mkm_value_last_point))) /\ ((((exists fs_h_mkm_last_point_decoded. fs_h_mkm_last_point_decoded + S (mkm_exponent_last_point) = S ((S (l)) * vc)) /\ exists fs_q_mkm_last_point_decoded. vb = fs_q_mkm_last_point_decoded * S ((S (l)) * vc) + (mkm_exponent_last_point))) /\ (((exists bpv_gap_mkm_last_point_valuation_exponent_bound. bpv_gap_mkm_last_point_valuation_exponent_bound + mkm_exponent_last_point = (mkm_value_last_point)) /\ (exists bpv_result_mkm_last_point_valuation_selected. ((exists ff_b_mkm_last_point_valuation_selected_power ff_c_mkm_last_point_valuation_selected_power. ((forall ff_i_mkm_last_point_valuation_selected_power_repeat. (exists ff_lt_mkm_last_point_valuation_selected_power_repeat_bound. ff_lt_mkm_last_point_valuation_selected_power_repeat_bound + S ff_i_mkm_last_point_valuation_selected_power_repeat = mkm_exponent_last_point) -> (((exists ff_h_mkm_last_point_valuation_selected_power_repeat_decoded. ff_h_mkm_last_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_last_point_valuation_selected_power_repeat)) * ff_c_mkm_last_point_valuation_selected_power)) /\ exists ff_q_mkm_last_point_valuation_selected_power_repeat_decoded. ff_b_mkm_last_point_valuation_selected_power = ff_q_mkm_last_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_last_point_valuation_selected_power_repeat)) * ff_c_mkm_last_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_last_point_valuation_selected_power_product ff_v_mkm_last_point_valuation_selected_power_product. ((((exists ff_h_mkm_last_point_valuation_selected_power_product_start. ff_h_mkm_last_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_last_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_point_valuation_selected_power_product_start. ff_u_mkm_last_point_valuation_selected_power_product = ff_q_mkm_last_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_last_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_last_point_valuation_selected_power_product_terminal. ff_h_mkm_last_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_last_point_valuation_selected) = S ((S (mkm_exponent_last_point)) * ff_v_mkm_last_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_point_valuation_selected_power_product_terminal. ff_u_mkm_last_point_valuation_selected_power_product = ff_q_mkm_last_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_last_point)) * ff_v_mkm_last_point_valuation_selected_power_product) + (bpv_result_mkm_last_point_valuation_selected))) /\ forall ff_i_mkm_last_point_valuation_selected_power_product. (exists ff_lt_mkm_last_point_valuation_selected_power_product_bound. ff_lt_mkm_last_point_valuation_selected_power_product_bound + S ff_i_mkm_last_point_valuation_selected_power_product = mkm_exponent_last_point) -> exists ff_p_mkm_last_point_valuation_selected_power_product ff_r_mkm_last_point_valuation_selected_power_product ff_s_mkm_last_point_valuation_selected_power_product. ((((exists ff_h_mkm_last_point_valuation_selected_power_product_factor. ff_h_mkm_last_point_valuation_selected_power_product_factor + S (ff_p_mkm_last_point_valuation_selected_power_product) = S ((S (ff_i_mkm_last_point_valuation_selected_power_product)) * ff_c_mkm_last_point_valuation_selected_power)) /\ exists ff_q_mkm_last_point_valuation_selected_power_product_factor. ff_b_mkm_last_point_valuation_selected_power = ff_q_mkm_last_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_last_point_valuation_selected_power_product)) * ff_c_mkm_last_point_valuation_selected_power) + (ff_p_mkm_last_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_last_point_valuation_selected_power_product_partial. ff_h_mkm_last_point_valuation_selected_power_product_partial + S (ff_r_mkm_last_point_valuation_selected_power_product) = S ((S (ff_i_mkm_last_point_valuation_selected_power_product)) * ff_v_mkm_last_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_point_valuation_selected_power_product_partial. ff_u_mkm_last_point_valuation_selected_power_product = ff_q_mkm_last_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_last_point_valuation_selected_power_product)) * ff_v_mkm_last_point_valuation_selected_power_product) + (ff_r_mkm_last_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_last_point_valuation_selected_power_product_successor. ff_h_mkm_last_point_valuation_selected_power_product_successor + S (ff_s_mkm_last_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_last_point_valuation_selected_power_product)) * ff_v_mkm_last_point_valuation_selected_power_product)) /\ exists ff_q_mkm_last_point_valuation_selected_power_product_successor. ff_u_mkm_last_point_valuation_selected_power_product = ff_q_mkm_last_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_last_point_valuation_selected_power_product)) * ff_v_mkm_last_point_valuation_selected_power_product) + (ff_s_mkm_last_point_valuation_selected_power_product))) /\ ff_s_mkm_last_point_valuation_selected_power_product = ff_r_mkm_last_point_valuation_selected_power_product * ff_p_mkm_last_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_last_point_valuation_selected_divides. (mkm_value_last_point) = bpv_result_mkm_last_point_valuation_selected * bpv_factor_mkm_last_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_last_point_valuation. (exists bpv_gap_mkm_last_point_valuation_candidate_bound. bpv_gap_mkm_last_point_valuation_candidate_bound + bpv_candidate_mkm_last_point_valuation = (mkm_value_last_point)) -> (exists bpv_result_mkm_last_point_valuation_candidate. ((exists ff_b_mkm_last_point_valuation_candidate_power ff_c_mkm_last_point_valuation_candidate_power. ((forall ff_i_mkm_last_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_last_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_last_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_last_point_valuation_candidate_power_repeat = bpv_candidate_mkm_last_point_valuation) -> (((exists ff_h_mkm_last_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_last_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_last_point_valuation_candidate_power_repeat)) * ff_c_mkm_last_point_valuation_candidate_power)) /\ exists ff_q_mkm_last_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_last_point_valuation_candidate_power = ff_q_mkm_last_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_last_point_valuation_candidate_power_repeat)) * ff_c_mkm_last_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_last_point_valuation_candidate_power_product ff_v_mkm_last_point_valuation_candidate_power_product. ((((exists ff_h_mkm_last_point_valuation_candidate_power_product_start. ff_h_mkm_last_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_last_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_point_valuation_candidate_power_product_start. ff_u_mkm_last_point_valuation_candidate_power_product = ff_q_mkm_last_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_last_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_last_point_valuation_candidate_power_product_terminal. ff_h_mkm_last_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_last_point_valuation_candidate) = S ((S (bpv_candidate_mkm_last_point_valuation)) * ff_v_mkm_last_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_point_valuation_candidate_power_product_terminal. ff_u_mkm_last_point_valuation_candidate_power_product = ff_q_mkm_last_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_last_point_valuation)) * ff_v_mkm_last_point_valuation_candidate_power_product) + (bpv_result_mkm_last_point_valuation_candidate))) /\ forall ff_i_mkm_last_point_valuation_candidate_power_product. (exists ff_lt_mkm_last_point_valuation_candidate_power_product_bound. ff_lt_mkm_last_point_valuation_candidate_power_product_bound + S ff_i_mkm_last_point_valuation_candidate_power_product = bpv_candidate_mkm_last_point_valuation) -> exists ff_p_mkm_last_point_valuation_candidate_power_product ff_r_mkm_last_point_valuation_candidate_power_product ff_s_mkm_last_point_valuation_candidate_power_product. ((((exists ff_h_mkm_last_point_valuation_candidate_power_product_factor. ff_h_mkm_last_point_valuation_candidate_power_product_factor + S (ff_p_mkm_last_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_last_point_valuation_candidate_power_product)) * ff_c_mkm_last_point_valuation_candidate_power)) /\ exists ff_q_mkm_last_point_valuation_candidate_power_product_factor. ff_b_mkm_last_point_valuation_candidate_power = ff_q_mkm_last_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_last_point_valuation_candidate_power_product)) * ff_c_mkm_last_point_valuation_candidate_power) + (ff_p_mkm_last_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_last_point_valuation_candidate_power_product_partial. ff_h_mkm_last_point_valuation_candidate_power_product_partial + S (ff_r_mkm_last_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_last_point_valuation_candidate_power_product)) * ff_v_mkm_last_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_point_valuation_candidate_power_product_partial. ff_u_mkm_last_point_valuation_candidate_power_product = ff_q_mkm_last_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_last_point_valuation_candidate_power_product)) * ff_v_mkm_last_point_valuation_candidate_power_product) + (ff_r_mkm_last_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_last_point_valuation_candidate_power_product_successor. ff_h_mkm_last_point_valuation_candidate_power_product_successor + S (ff_s_mkm_last_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_last_point_valuation_candidate_power_product)) * ff_v_mkm_last_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_last_point_valuation_candidate_power_product_successor. ff_u_mkm_last_point_valuation_candidate_power_product = ff_q_mkm_last_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_last_point_valuation_candidate_power_product)) * ff_v_mkm_last_point_valuation_candidate_power_product) + (ff_s_mkm_last_point_valuation_candidate_power_product))) /\ ff_s_mkm_last_point_valuation_candidate_power_product = ff_r_mkm_last_point_valuation_candidate_power_product * ff_p_mkm_last_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_last_point_valuation_candidate_divides. (mkm_value_last_point) = bpv_result_mkm_last_point_valuation_candidate * bpv_factor_mkm_last_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_last_point_valuation_maximal. bpv_gap_mkm_last_point_valuation_maximal + bpv_candidate_mkm_last_point_valuation = mkm_exponent_last_point)))
  13. 0013specialize h l
  14. 0014apply h
  15. 0015specialize le_refl (S l)
  16. 0016apply le_refl
  17. 0017cases hpoint
  18. 0018cases hpoint_witness
  19. 0019cases hpoint_witness_witness
  20. 0020cases hpoint_witness_witness_right
  21. 0021have hvalue : x = a
  22. 0022specialize beta_at_unique b
  23. 0023specialize beta_at_unique c
  24. 0024specialize beta_at_unique l
  25. 0025specialize beta_at_unique x
  26. 0026specialize beta_at_unique a
  27. 0027apply beta_at_unique
  28. 0028exact hpoint_witness_witness_left
  29. 0029exact ha
  30. 0030have hexponent : x1 = e
  31. 0031specialize beta_at_unique vb
  32. 0032specialize beta_at_unique vc
  33. 0033specialize beta_at_unique l
  34. 0034specialize beta_at_unique x1
  35. 0035specialize beta_at_unique e
  36. 0036apply beta_at_unique
  37. 0037exact hpoint_witness_witness_right_left
  38. 0038exact he
  39. 0039rewrite hvalue at hpoint_witness_witness_right_right
  40. 0040rewrite hvalue at hpoint_witness_witness_right_right
  41. 0041rewrite hvalue at hpoint_witness_witness_right_right
  42. 0042rewrite hvalue at hpoint_witness_witness_right_right
  43. 0043rewrite hexponent at hpoint_witness_witness_right_right
  44. 0044rewrite hexponent at hpoint_witness_witness_right_right
  45. 0045rewrite hexponent at hpoint_witness_witness_right_right
  46. 0046rewrite hexponent at hpoint_witness_witness_right_right
  47. 0047rewrite hexponent at hpoint_witness_witness_right_right
  48. 0048rewrite hexponent at hpoint_witness_witness_right_right
  49. 0049exact hpoint_witness_witness_right_right