MK0001

beta_valuation_prefix_empty

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

Every empty decoded list has an empty bounded-valuation table.

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. forall mkm_index_empty. (exists mkm_lt_empty_bound. mkm_lt_empty_bound + S (mkm_index_empty) = (0)) -> (exists mkm_value_empty_point mkm_exponent_empty_point. (((exists fs_h_mkm_empty_point_source. fs_h_mkm_empty_point_source + S (mkm_value_empty_point) = S ((S (mkm_index_empty)) * c)) /\ exists fs_q_mkm_empty_point_source. b = fs_q_mkm_empty_point_source * S ((S (mkm_index_empty)) * c) + (mkm_value_empty_point))) /\ ((((exists fs_h_mkm_empty_point_decoded. fs_h_mkm_empty_point_decoded + S (mkm_exponent_empty_point) = S ((S (mkm_index_empty)) * vc)) /\ exists fs_q_mkm_empty_point_decoded. vb = fs_q_mkm_empty_point_decoded * S ((S (mkm_index_empty)) * vc) + (mkm_exponent_empty_point))) /\ (((exists bpv_gap_mkm_empty_point_valuation_exponent_bound. bpv_gap_mkm_empty_point_valuation_exponent_bound + mkm_exponent_empty_point = (mkm_value_empty_point)) /\ (exists bpv_result_mkm_empty_point_valuation_selected. ((exists ff_b_mkm_empty_point_valuation_selected_power ff_c_mkm_empty_point_valuation_selected_power. ((forall ff_i_mkm_empty_point_valuation_selected_power_repeat. (exists ff_lt_mkm_empty_point_valuation_selected_power_repeat_bound. ff_lt_mkm_empty_point_valuation_selected_power_repeat_bound + S ff_i_mkm_empty_point_valuation_selected_power_repeat = mkm_exponent_empty_point) -> (((exists ff_h_mkm_empty_point_valuation_selected_power_repeat_decoded. ff_h_mkm_empty_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_empty_point_valuation_selected_power_repeat)) * ff_c_mkm_empty_point_valuation_selected_power)) /\ exists ff_q_mkm_empty_point_valuation_selected_power_repeat_decoded. ff_b_mkm_empty_point_valuation_selected_power = ff_q_mkm_empty_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_empty_point_valuation_selected_power_repeat)) * ff_c_mkm_empty_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_empty_point_valuation_selected_power_product ff_v_mkm_empty_point_valuation_selected_power_product. ((((exists ff_h_mkm_empty_point_valuation_selected_power_product_start. ff_h_mkm_empty_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_empty_point_valuation_selected_power_product)) /\ exists ff_q_mkm_empty_point_valuation_selected_power_product_start. ff_u_mkm_empty_point_valuation_selected_power_product = ff_q_mkm_empty_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_empty_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_empty_point_valuation_selected_power_product_terminal. ff_h_mkm_empty_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_empty_point_valuation_selected) = S ((S (mkm_exponent_empty_point)) * ff_v_mkm_empty_point_valuation_selected_power_product)) /\ exists ff_q_mkm_empty_point_valuation_selected_power_product_terminal. ff_u_mkm_empty_point_valuation_selected_power_product = ff_q_mkm_empty_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_empty_point)) * ff_v_mkm_empty_point_valuation_selected_power_product) + (bpv_result_mkm_empty_point_valuation_selected))) /\ forall ff_i_mkm_empty_point_valuation_selected_power_product. (exists ff_lt_mkm_empty_point_valuation_selected_power_product_bound. ff_lt_mkm_empty_point_valuation_selected_power_product_bound + S ff_i_mkm_empty_point_valuation_selected_power_product = mkm_exponent_empty_point) -> exists ff_p_mkm_empty_point_valuation_selected_power_product ff_r_mkm_empty_point_valuation_selected_power_product ff_s_mkm_empty_point_valuation_selected_power_product. ((((exists ff_h_mkm_empty_point_valuation_selected_power_product_factor. ff_h_mkm_empty_point_valuation_selected_power_product_factor + S (ff_p_mkm_empty_point_valuation_selected_power_product) = S ((S (ff_i_mkm_empty_point_valuation_selected_power_product)) * ff_c_mkm_empty_point_valuation_selected_power)) /\ exists ff_q_mkm_empty_point_valuation_selected_power_product_factor. ff_b_mkm_empty_point_valuation_selected_power = ff_q_mkm_empty_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_empty_point_valuation_selected_power_product)) * ff_c_mkm_empty_point_valuation_selected_power) + (ff_p_mkm_empty_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_empty_point_valuation_selected_power_product_partial. ff_h_mkm_empty_point_valuation_selected_power_product_partial + S (ff_r_mkm_empty_point_valuation_selected_power_product) = S ((S (ff_i_mkm_empty_point_valuation_selected_power_product)) * ff_v_mkm_empty_point_valuation_selected_power_product)) /\ exists ff_q_mkm_empty_point_valuation_selected_power_product_partial. ff_u_mkm_empty_point_valuation_selected_power_product = ff_q_mkm_empty_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_empty_point_valuation_selected_power_product)) * ff_v_mkm_empty_point_valuation_selected_power_product) + (ff_r_mkm_empty_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_empty_point_valuation_selected_power_product_successor. ff_h_mkm_empty_point_valuation_selected_power_product_successor + S (ff_s_mkm_empty_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_empty_point_valuation_selected_power_product)) * ff_v_mkm_empty_point_valuation_selected_power_product)) /\ exists ff_q_mkm_empty_point_valuation_selected_power_product_successor. ff_u_mkm_empty_point_valuation_selected_power_product = ff_q_mkm_empty_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_empty_point_valuation_selected_power_product)) * ff_v_mkm_empty_point_valuation_selected_power_product) + (ff_s_mkm_empty_point_valuation_selected_power_product))) /\ ff_s_mkm_empty_point_valuation_selected_power_product = ff_r_mkm_empty_point_valuation_selected_power_product * ff_p_mkm_empty_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_empty_point_valuation_selected_divides. (mkm_value_empty_point) = bpv_result_mkm_empty_point_valuation_selected * bpv_factor_mkm_empty_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_empty_point_valuation. (exists bpv_gap_mkm_empty_point_valuation_candidate_bound. bpv_gap_mkm_empty_point_valuation_candidate_bound + bpv_candidate_mkm_empty_point_valuation = (mkm_value_empty_point)) -> (exists bpv_result_mkm_empty_point_valuation_candidate. ((exists ff_b_mkm_empty_point_valuation_candidate_power ff_c_mkm_empty_point_valuation_candidate_power. ((forall ff_i_mkm_empty_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_empty_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_empty_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_empty_point_valuation_candidate_power_repeat = bpv_candidate_mkm_empty_point_valuation) -> (((exists ff_h_mkm_empty_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_empty_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_empty_point_valuation_candidate_power_repeat)) * ff_c_mkm_empty_point_valuation_candidate_power)) /\ exists ff_q_mkm_empty_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_empty_point_valuation_candidate_power = ff_q_mkm_empty_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_empty_point_valuation_candidate_power_repeat)) * ff_c_mkm_empty_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_empty_point_valuation_candidate_power_product ff_v_mkm_empty_point_valuation_candidate_power_product. ((((exists ff_h_mkm_empty_point_valuation_candidate_power_product_start. ff_h_mkm_empty_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_empty_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_empty_point_valuation_candidate_power_product_start. ff_u_mkm_empty_point_valuation_candidate_power_product = ff_q_mkm_empty_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_empty_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_empty_point_valuation_candidate_power_product_terminal. ff_h_mkm_empty_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_empty_point_valuation_candidate) = S ((S (bpv_candidate_mkm_empty_point_valuation)) * ff_v_mkm_empty_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_empty_point_valuation_candidate_power_product_terminal. ff_u_mkm_empty_point_valuation_candidate_power_product = ff_q_mkm_empty_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_empty_point_valuation)) * ff_v_mkm_empty_point_valuation_candidate_power_product) + (bpv_result_mkm_empty_point_valuation_candidate))) /\ forall ff_i_mkm_empty_point_valuation_candidate_power_product. (exists ff_lt_mkm_empty_point_valuation_candidate_power_product_bound. ff_lt_mkm_empty_point_valuation_candidate_power_product_bound + S ff_i_mkm_empty_point_valuation_candidate_power_product = bpv_candidate_mkm_empty_point_valuation) -> exists ff_p_mkm_empty_point_valuation_candidate_power_product ff_r_mkm_empty_point_valuation_candidate_power_product ff_s_mkm_empty_point_valuation_candidate_power_product. ((((exists ff_h_mkm_empty_point_valuation_candidate_power_product_factor. ff_h_mkm_empty_point_valuation_candidate_power_product_factor + S (ff_p_mkm_empty_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_empty_point_valuation_candidate_power_product)) * ff_c_mkm_empty_point_valuation_candidate_power)) /\ exists ff_q_mkm_empty_point_valuation_candidate_power_product_factor. ff_b_mkm_empty_point_valuation_candidate_power = ff_q_mkm_empty_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_empty_point_valuation_candidate_power_product)) * ff_c_mkm_empty_point_valuation_candidate_power) + (ff_p_mkm_empty_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_empty_point_valuation_candidate_power_product_partial. ff_h_mkm_empty_point_valuation_candidate_power_product_partial + S (ff_r_mkm_empty_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_empty_point_valuation_candidate_power_product)) * ff_v_mkm_empty_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_empty_point_valuation_candidate_power_product_partial. ff_u_mkm_empty_point_valuation_candidate_power_product = ff_q_mkm_empty_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_empty_point_valuation_candidate_power_product)) * ff_v_mkm_empty_point_valuation_candidate_power_product) + (ff_r_mkm_empty_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_empty_point_valuation_candidate_power_product_successor. ff_h_mkm_empty_point_valuation_candidate_power_product_successor + S (ff_s_mkm_empty_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_empty_point_valuation_candidate_power_product)) * ff_v_mkm_empty_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_empty_point_valuation_candidate_power_product_successor. ff_u_mkm_empty_point_valuation_candidate_power_product = ff_q_mkm_empty_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_empty_point_valuation_candidate_power_product)) * ff_v_mkm_empty_point_valuation_candidate_power_product) + (ff_s_mkm_empty_point_valuation_candidate_power_product))) /\ ff_s_mkm_empty_point_valuation_candidate_power_product = ff_r_mkm_empty_point_valuation_candidate_power_product * ff_p_mkm_empty_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_empty_point_valuation_candidate_divides. (mkm_value_empty_point) = bpv_result_mkm_empty_point_valuation_candidate * bpv_factor_mkm_empty_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_empty_point_valuation_maximal. bpv_gap_mkm_empty_point_valuation_maximal + bpv_candidate_mkm_empty_point_valuation = mkm_exponent_empty_point))))

Constructive proof overview

Generated structural guide

Every empty decoded list has an empty bounded-valuation table.

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

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

Proof neighborhood

Direct dependencies

lt_not_le Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorized

Direct dependents

MK0005 beta_valuation_prefix_exists

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

14 script commands · 3 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–7

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 i
  7. L7
    intro hi
02Separate the logical casesL8–8

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

  1. L8
    exfalso
03Use earlier factsL9–14

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

  1. L9
    specialize lt_not_le i
  2. L10
    specialize lt_not_le 0
  3. L11
    apply lt_not_le
  4. L12
    exact hi
  5. L13
    specialize zero_le i
  6. L14
    apply zero_le

Library-wide reading audit

Original exact command ledger · 14 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro vb
  5. 0005intro vc
  6. 0006intro i
  7. 0007intro hi
  8. 0008exfalso
  9. 0009specialize lt_not_le i
  10. 0010specialize lt_not_le 0
  11. 0011apply lt_not_le
  12. 0012exact hi
  13. 0013specialize zero_le i
  14. 0014apply zero_le