MK0005

beta_valuation_prefix_exists

Every finite decoded list has a genuinely constructed finite table of bounded power valuations.

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. ∀ l. ∃ vb. ∃ vc. BetaValuationPrefix(p,b,c,vb,vc,l)

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

Definition DAG

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

Actual proof prerequisites

beta_valuation_prefix_emptybeta_at_exists · checked external prerequisitepower_valuation_exists · checked external prerequisitebeta_valuation_prefix_extend
Original expanded first-order statement 
forall p b c l. exists vb vc. (forall mkm_index_exists_result. (exists mkm_lt_exists_result_bound. mkm_lt_exists_result_bound + S (mkm_index_exists_result) = (l)) -> (exists mkm_value_exists_result_point mkm_exponent_exists_result_point. (((exists fs_h_mkm_exists_result_point_source. fs_h_mkm_exists_result_point_source + S (mkm_value_exists_result_point) = S ((S (mkm_index_exists_result)) * c)) /\ exists fs_q_mkm_exists_result_point_source. b = fs_q_mkm_exists_result_point_source * S ((S (mkm_index_exists_result)) * c) + (mkm_value_exists_result_point))) /\ ((((exists fs_h_mkm_exists_result_point_decoded. fs_h_mkm_exists_result_point_decoded + S (mkm_exponent_exists_result_point) = S ((S (mkm_index_exists_result)) * vc)) /\ exists fs_q_mkm_exists_result_point_decoded. vb = fs_q_mkm_exists_result_point_decoded * S ((S (mkm_index_exists_result)) * vc) + (mkm_exponent_exists_result_point))) /\ (((exists bpv_gap_mkm_exists_result_point_valuation_exponent_bound. bpv_gap_mkm_exists_result_point_valuation_exponent_bound + mkm_exponent_exists_result_point = (mkm_value_exists_result_point)) /\ (exists bpv_result_mkm_exists_result_point_valuation_selected. ((exists ff_b_mkm_exists_result_point_valuation_selected_power ff_c_mkm_exists_result_point_valuation_selected_power. ((forall ff_i_mkm_exists_result_point_valuation_selected_power_repeat. (exists ff_lt_mkm_exists_result_point_valuation_selected_power_repeat_bound. ff_lt_mkm_exists_result_point_valuation_selected_power_repeat_bound + S ff_i_mkm_exists_result_point_valuation_selected_power_repeat = mkm_exponent_exists_result_point) -> (((exists ff_h_mkm_exists_result_point_valuation_selected_power_repeat_decoded. ff_h_mkm_exists_result_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_repeat)) * ff_c_mkm_exists_result_point_valuation_selected_power)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_repeat_decoded. ff_b_mkm_exists_result_point_valuation_selected_power = ff_q_mkm_exists_result_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_repeat)) * ff_c_mkm_exists_result_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_exists_result_point_valuation_selected_power_product ff_v_mkm_exists_result_point_valuation_selected_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_start. ff_h_mkm_exists_result_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_start. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_terminal. ff_h_mkm_exists_result_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_exists_result_point_valuation_selected) = S ((S (mkm_exponent_exists_result_point)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_terminal. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_exists_result_point)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (bpv_result_mkm_exists_result_point_valuation_selected))) /\ forall ff_i_mkm_exists_result_point_valuation_selected_power_product. (exists ff_lt_mkm_exists_result_point_valuation_selected_power_product_bound. ff_lt_mkm_exists_result_point_valuation_selected_power_product_bound + S ff_i_mkm_exists_result_point_valuation_selected_power_product = mkm_exponent_exists_result_point) -> exists ff_p_mkm_exists_result_point_valuation_selected_power_product ff_r_mkm_exists_result_point_valuation_selected_power_product ff_s_mkm_exists_result_point_valuation_selected_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_factor. ff_h_mkm_exists_result_point_valuation_selected_power_product_factor + S (ff_p_mkm_exists_result_point_valuation_selected_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_c_mkm_exists_result_point_valuation_selected_power)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_factor. ff_b_mkm_exists_result_point_valuation_selected_power = ff_q_mkm_exists_result_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_c_mkm_exists_result_point_valuation_selected_power) + (ff_p_mkm_exists_result_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_partial. ff_h_mkm_exists_result_point_valuation_selected_power_product_partial + S (ff_r_mkm_exists_result_point_valuation_selected_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_partial. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (ff_r_mkm_exists_result_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_selected_power_product_successor. ff_h_mkm_exists_result_point_valuation_selected_power_product_successor + S (ff_s_mkm_exists_result_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_selected_power_product_successor. ff_u_mkm_exists_result_point_valuation_selected_power_product = ff_q_mkm_exists_result_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_exists_result_point_valuation_selected_power_product)) * ff_v_mkm_exists_result_point_valuation_selected_power_product) + (ff_s_mkm_exists_result_point_valuation_selected_power_product))) /\ ff_s_mkm_exists_result_point_valuation_selected_power_product = ff_r_mkm_exists_result_point_valuation_selected_power_product * ff_p_mkm_exists_result_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_exists_result_point_valuation_selected_divides. (mkm_value_exists_result_point) = bpv_result_mkm_exists_result_point_valuation_selected * bpv_factor_mkm_exists_result_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_exists_result_point_valuation. (exists bpv_gap_mkm_exists_result_point_valuation_candidate_bound. bpv_gap_mkm_exists_result_point_valuation_candidate_bound + bpv_candidate_mkm_exists_result_point_valuation = (mkm_value_exists_result_point)) -> (exists bpv_result_mkm_exists_result_point_valuation_candidate. ((exists ff_b_mkm_exists_result_point_valuation_candidate_power ff_c_mkm_exists_result_point_valuation_candidate_power. ((forall ff_i_mkm_exists_result_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_exists_result_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_exists_result_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_exists_result_point_valuation_candidate_power_repeat = bpv_candidate_mkm_exists_result_point_valuation) -> (((exists ff_h_mkm_exists_result_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_exists_result_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_repeat)) * ff_c_mkm_exists_result_point_valuation_candidate_power)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_exists_result_point_valuation_candidate_power = ff_q_mkm_exists_result_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_repeat)) * ff_c_mkm_exists_result_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_exists_result_point_valuation_candidate_power_product ff_v_mkm_exists_result_point_valuation_candidate_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_start. ff_h_mkm_exists_result_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_start. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_terminal. ff_h_mkm_exists_result_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_exists_result_point_valuation_candidate) = S ((S (bpv_candidate_mkm_exists_result_point_valuation)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_terminal. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_exists_result_point_valuation)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (bpv_result_mkm_exists_result_point_valuation_candidate))) /\ forall ff_i_mkm_exists_result_point_valuation_candidate_power_product. (exists ff_lt_mkm_exists_result_point_valuation_candidate_power_product_bound. ff_lt_mkm_exists_result_point_valuation_candidate_power_product_bound + S ff_i_mkm_exists_result_point_valuation_candidate_power_product = bpv_candidate_mkm_exists_result_point_valuation) -> exists ff_p_mkm_exists_result_point_valuation_candidate_power_product ff_r_mkm_exists_result_point_valuation_candidate_power_product ff_s_mkm_exists_result_point_valuation_candidate_power_product. ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_factor. ff_h_mkm_exists_result_point_valuation_candidate_power_product_factor + S (ff_p_mkm_exists_result_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_c_mkm_exists_result_point_valuation_candidate_power)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_factor. ff_b_mkm_exists_result_point_valuation_candidate_power = ff_q_mkm_exists_result_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_c_mkm_exists_result_point_valuation_candidate_power) + (ff_p_mkm_exists_result_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_partial. ff_h_mkm_exists_result_point_valuation_candidate_power_product_partial + S (ff_r_mkm_exists_result_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_partial. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (ff_r_mkm_exists_result_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_exists_result_point_valuation_candidate_power_product_successor. ff_h_mkm_exists_result_point_valuation_candidate_power_product_successor + S (ff_s_mkm_exists_result_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_exists_result_point_valuation_candidate_power_product_successor. ff_u_mkm_exists_result_point_valuation_candidate_power_product = ff_q_mkm_exists_result_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_exists_result_point_valuation_candidate_power_product)) * ff_v_mkm_exists_result_point_valuation_candidate_power_product) + (ff_s_mkm_exists_result_point_valuation_candidate_power_product))) /\ ff_s_mkm_exists_result_point_valuation_candidate_power_product = ff_r_mkm_exists_result_point_valuation_candidate_power_product * ff_p_mkm_exists_result_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_exists_result_point_valuation_candidate_divides. (mkm_value_exists_result_point) = bpv_result_mkm_exists_result_point_valuation_candidate * bpv_factor_mkm_exists_result_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_exists_result_point_valuation_maximal. bpv_gap_mkm_exists_result_point_valuation_maximal + bpv_candidate_mkm_exists_result_point_valuation = mkm_exponent_exists_result_point)))))

Complete tactic proof in conservative notation

All 39 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

39 script commands · 12 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.

Named ingredients (2)
beta valuation prefix emptybeta valuation prefix extend
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
02Induction on lL4–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
03Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 0
04Use earlier factsL7–12

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

  1. L7
    specialize beta_valuation_prefix_empty p
  2. L8
    specialize beta_valuation_prefix_empty b
  3. L9
    specialize beta_valuation_prefix_empty c
  4. L10
    specialize beta_valuation_prefix_empty 0
  5. L11
    specialize beta_valuation_prefix_empty 0
  6. L12
    apply beta_valuation_prefix_empty
05Establish hprefixL13–14

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

  1. L13
    have hprefix : ∃ vb. ∃ vc. BetaValuationPrefix(p,b,c,vb,vc,l)Definitions: BetaValuationPrefix(p,b,c,vb,vc,l)Original native command in the exact edition
  2. L14
    apply IH
06Separate the logical casesL15–16

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

  1. L15
    cases hprefix
  2. L16
    cases hprefix_witness
07Establish hvalueL17–21

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

  1. L17
    have hvalue : ∃ a. BetaAt(b,c,l,a)Definitions: BetaAt(b,c,l,a)Original native command in the exact edition
  2. L18
    specialize beta_at_exists b
  3. L19
    specialize beta_at_exists c
  4. L20
    specialize beta_at_exists l
  5. L21
    apply beta_at_exists
08Separate the logical casesL22–22

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

  1. L22
    cases hvalue
09Establish hvalL23–26

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

  1. L23
    have hval : ∃ e. BoundedPowerValuation(p,x2,x2,e)Definitions: BoundedPowerValuation(p,x2,x2,e)Original native command in the exact edition
  2. L24
    specialize power_valuation_exists p
  3. L25
    specialize power_valuation_exists x2
  4. L26
    apply power_valuation_exists
10Separate the logical casesL27–27

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

  1. L27
    cases hval
11Use earlier factsL28–37

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

  1. L28
    specialize beta_valuation_prefix_extend p
  2. L29
    specialize beta_valuation_prefix_extend b
  3. L30
    specialize beta_valuation_prefix_extend c
  4. L31
    specialize beta_valuation_prefix_extend x
  5. L32
    specialize beta_valuation_prefix_extend x1
  6. L33
    specialize beta_valuation_prefix_extend l
  7. L34
    specialize beta_valuation_prefix_extend x2
  8. L35
    specialize beta_valuation_prefix_extend x3
  9. L36
    apply beta_valuation_prefix_extend
  10. L37
    exact hprefix_witness_witness
12Use earlier factsL38–39

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

  1. L38
    exact hvalue_witness
  2. L39
    exact hval_witness

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004induction l
  5. 0005exists 0
  6. 0006exists 0
  7. 0007specialize beta_valuation_prefix_empty p
  8. 0008specialize beta_valuation_prefix_empty b
  9. 0009specialize beta_valuation_prefix_empty c
  10. 0010specialize beta_valuation_prefix_empty 0
  11. 0011specialize beta_valuation_prefix_empty 0
  12. 0012apply beta_valuation_prefix_empty
  13. 0013have hprefix : ∃ vb. ∃ vc. BetaValuationPrefix(p,b,c,vb,vc,l)
  14. 0014apply IH
  15. 0015cases hprefix
  16. 0016cases hprefix_witness
  17. 0017have hvalue : ∃ a. BetaAt(b,c,l,a)
  18. 0018specialize beta_at_exists b
  19. 0019specialize beta_at_exists c
  20. 0020specialize beta_at_exists l
  21. 0021apply beta_at_exists
  22. 0022cases hvalue
  23. 0023have hval : ∃ e. BoundedPowerValuation(p,x2,x2,e)
  24. 0024specialize power_valuation_exists p
  25. 0025specialize power_valuation_exists x2
  26. 0026apply power_valuation_exists
  27. 0027cases hval
  28. 0028specialize beta_valuation_prefix_extend p
  29. 0029specialize beta_valuation_prefix_extend b
  30. 0030specialize beta_valuation_prefix_extend c
  31. 0031specialize beta_valuation_prefix_extend x
  32. 0032specialize beta_valuation_prefix_extend x1
  33. 0033specialize beta_valuation_prefix_extend l
  34. 0034specialize beta_valuation_prefix_extend x2
  35. 0035specialize beta_valuation_prefix_extend x3
  36. 0036apply beta_valuation_prefix_extend
  37. 0037exact hprefix_witness_witness
  38. 0038exact hvalue_witness
  39. 0039exact hval_witness