MK0003

beta_valuation_prefix_last

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

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

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.

The carry relation contains actual quotient columns and carry bits, not the desired valuation. The theorem includes all finite lists and zero parts. It uses sequential binary-column carries; a separate simultaneous-grid or permutation-invariance theorem is not asserted.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ vb. ∀ vc. ∀ l. ∀ a. ∀ e. BetaValuationPrefix(p,b,c,vb,vc,S l) → BetaAt(b,c,l,a) → BetaAt(vb,vc,l,e) → BoundedPowerValuation(p,a,a,e)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaValuationPrefix(p,b,c,vb,vc,l) · 1BetaAt(b,c,i,x) · 4BoundedPowerValuation(p,n,b,e) · 2

Actual proof prerequisites

le_refl · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

All 49 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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: 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)Original native command in the exact edition
  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 defined 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 : ∃ 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))
  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