BD0007

binary_digit_bounded_prefix_exists

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

Induction on the exact power exponent constructs a genuine length-l beta-coded binary representation of every natural strictly below 2^l.

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 l p n. (exists pa_b_bl_bd_bounded_power pa_c_bl_bd_bounded_power. ((forall pa_i_bl_bd_bounded_power_repeat. (exists pa_lt_bl_bd_bounded_power_repeat_bound. pa_lt_bl_bd_bounded_power_repeat_bound + S pa_i_bl_bd_bounded_power_repeat = l) -> (((exists pa_h_bl_bd_bounded_power_repeat_decoded. pa_h_bl_bd_bounded_power_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_bounded_power_repeat)) * pa_c_bl_bd_bounded_power)) /\ exists pa_q_bl_bd_bounded_power_repeat_decoded. pa_b_bl_bd_bounded_power = pa_q_bl_bd_bounded_power_repeat_decoded * S ((S (pa_i_bl_bd_bounded_power_repeat)) * pa_c_bl_bd_bounded_power) + (2)))) /\ (exists pa_u_bl_bd_bounded_power_product pa_v_bl_bd_bounded_power_product. ((((exists pa_h_bl_bd_bounded_power_product_start. pa_h_bl_bd_bounded_power_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_bounded_power_product)) /\ exists pa_q_bl_bd_bounded_power_product_start. pa_u_bl_bd_bounded_power_product = pa_q_bl_bd_bounded_power_product_start * S ((S (0)) * pa_v_bl_bd_bounded_power_product) + (1))) /\ ((((exists pa_h_bl_bd_bounded_power_product_terminal. pa_h_bl_bd_bounded_power_product_terminal + S (p) = S ((S (l)) * pa_v_bl_bd_bounded_power_product)) /\ exists pa_q_bl_bd_bounded_power_product_terminal. pa_u_bl_bd_bounded_power_product = pa_q_bl_bd_bounded_power_product_terminal * S ((S (l)) * pa_v_bl_bd_bounded_power_product) + (p))) /\ forall pa_i_bl_bd_bounded_power_product. (exists pa_lt_bl_bd_bounded_power_product_bound. pa_lt_bl_bd_bounded_power_product_bound + S pa_i_bl_bd_bounded_power_product = l) -> exists pa_p_bl_bd_bounded_power_product pa_r_bl_bd_bounded_power_product pa_s_bl_bd_bounded_power_product. ((((exists pa_h_bl_bd_bounded_power_product_factor. pa_h_bl_bd_bounded_power_product_factor + S (pa_p_bl_bd_bounded_power_product) = S ((S (pa_i_bl_bd_bounded_power_product)) * pa_c_bl_bd_bounded_power)) /\ exists pa_q_bl_bd_bounded_power_product_factor. pa_b_bl_bd_bounded_power = pa_q_bl_bd_bounded_power_product_factor * S ((S (pa_i_bl_bd_bounded_power_product)) * pa_c_bl_bd_bounded_power) + (pa_p_bl_bd_bounded_power_product))) /\ ((((exists pa_h_bl_bd_bounded_power_product_partial. pa_h_bl_bd_bounded_power_product_partial + S (pa_r_bl_bd_bounded_power_product) = S ((S (pa_i_bl_bd_bounded_power_product)) * pa_v_bl_bd_bounded_power_product)) /\ exists pa_q_bl_bd_bounded_power_product_partial. pa_u_bl_bd_bounded_power_product = pa_q_bl_bd_bounded_power_product_partial * S ((S (pa_i_bl_bd_bounded_power_product)) * pa_v_bl_bd_bounded_power_product) + (pa_r_bl_bd_bounded_power_product))) /\ ((((exists pa_h_bl_bd_bounded_power_product_successor. pa_h_bl_bd_bounded_power_product_successor + S (pa_s_bl_bd_bounded_power_product) = S ((S (S pa_i_bl_bd_bounded_power_product)) * pa_v_bl_bd_bounded_power_product)) /\ exists pa_q_bl_bd_bounded_power_product_successor. pa_u_bl_bd_bounded_power_product = pa_q_bl_bd_bounded_power_product_successor * S ((S (S pa_i_bl_bd_bounded_power_product)) * pa_v_bl_bd_bounded_power_product) + (pa_s_bl_bd_bounded_power_product))) /\ pa_s_bl_bd_bounded_power_product = pa_r_bl_bd_bounded_power_product * pa_p_bl_bd_bounded_power_product)))))))) -> (exists gap. gap + S n = p) -> exists b c. (((forall ff_index_be_bd_bounded_result_digits ff_digit_be_bd_bounded_result_digits. (exists ff_lt_be_bd_bounded_result_digits_bound. ff_lt_be_bd_bounded_result_digits_bound + S ff_index_be_bd_bounded_result_digits = l) -> (((exists ff_h_be_bd_bounded_result_digits_digit. ff_h_be_bd_bounded_result_digits_digit + S (ff_digit_be_bd_bounded_result_digits) = S ((S (ff_index_be_bd_bounded_result_digits)) * c)) /\ exists ff_q_be_bd_bounded_result_digits_digit. b = ff_q_be_bd_bounded_result_digits_digit * S ((S (ff_index_be_bd_bounded_result_digits)) * c) + (ff_digit_be_bd_bounded_result_digits))) -> (ff_digit_be_bd_bounded_result_digits = 0 \/ ff_digit_be_bd_bounded_result_digits = 1)) /\ (exists ff_u_ph_bd_bounded_result_horner ff_v_ph_bd_bounded_result_horner. ((((exists fs_h_ph_bd_bounded_result_horner_body_start. fs_h_ph_bd_bounded_result_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_bounded_result_horner)) /\ exists fs_q_ph_bd_bounded_result_horner_body_start. ff_u_ph_bd_bounded_result_horner = fs_q_ph_bd_bounded_result_horner_body_start * S ((S (0)) * ff_v_ph_bd_bounded_result_horner) + (0))) /\ ((((exists fs_h_ph_bd_bounded_result_horner_body_terminal. fs_h_ph_bd_bounded_result_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_bounded_result_horner)) /\ exists fs_q_ph_bd_bounded_result_horner_body_terminal. ff_u_ph_bd_bounded_result_horner = fs_q_ph_bd_bounded_result_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_bounded_result_horner) + (n))) /\ forall ff_i_ph_bd_bounded_result_horner_body_steps. (exists ph_bound_bd_bounded_result_horner_body_steps. ph_bound_bd_bounded_result_horner_body_steps + S ff_i_ph_bd_bounded_result_horner_body_steps = l) -> exists ff_coefficient_ph_bd_bounded_result_horner_body_steps ff_previous_ph_bd_bounded_result_horner_body_steps ff_current_ph_bd_bounded_result_horner_body_steps. ((((exists fs_h_ph_bd_bounded_result_horner_body_steps_coefficient. fs_h_ph_bd_bounded_result_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_bounded_result_horner_body_steps) = S ((S (ff_i_ph_bd_bounded_result_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_bounded_result_horner_body_steps_coefficient. b = fs_q_ph_bd_bounded_result_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_bounded_result_horner_body_steps)) * c) + (ff_coefficient_ph_bd_bounded_result_horner_body_steps))) /\ ((((exists fs_h_ph_bd_bounded_result_horner_body_steps_before. fs_h_ph_bd_bounded_result_horner_body_steps_before + S (ff_previous_ph_bd_bounded_result_horner_body_steps) = S ((S (ff_i_ph_bd_bounded_result_horner_body_steps)) * ff_v_ph_bd_bounded_result_horner)) /\ exists fs_q_ph_bd_bounded_result_horner_body_steps_before. ff_u_ph_bd_bounded_result_horner = fs_q_ph_bd_bounded_result_horner_body_steps_before * S ((S (ff_i_ph_bd_bounded_result_horner_body_steps)) * ff_v_ph_bd_bounded_result_horner) + (ff_previous_ph_bd_bounded_result_horner_body_steps))) /\ ((((exists fs_h_ph_bd_bounded_result_horner_body_steps_after. fs_h_ph_bd_bounded_result_horner_body_steps_after + S (ff_current_ph_bd_bounded_result_horner_body_steps) = S ((S (S ff_i_ph_bd_bounded_result_horner_body_steps)) * ff_v_ph_bd_bounded_result_horner)) /\ exists fs_q_ph_bd_bounded_result_horner_body_steps_after. ff_u_ph_bd_bounded_result_horner = fs_q_ph_bd_bounded_result_horner_body_steps_after * S ((S (S ff_i_ph_bd_bounded_result_horner_body_steps)) * ff_v_ph_bd_bounded_result_horner) + (ff_current_ph_bd_bounded_result_horner_body_steps))) /\ ff_current_ph_bd_bounded_result_horner_body_steps = ff_previous_ph_bd_bounded_result_horner_body_steps * 2 + ff_coefficient_ph_bd_bounded_result_horner_body_steps))))))))

Constructive proof overview

Generated structural guide

Induction on the exact power exponent constructs a genuine length-l beta-coded binary representation of every natural strictly below 2^l.

The unchanged tactic script uses 11 declared prerequisites and contains 97 exact native proof lines.

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

Proof neighborhood

Direct dependencies

binary_power_two_zero_value Alpha theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized le_zero Stable theorem; checked-use authorized beta_horner_eval_exists Alpha theorem; checked-use authorized beta_horner_eval_empty Alpha theorem; checked-use authorized binary_digit_prefix_empty Alpha theorem; checked-use authorized binary_power_two_exists Alpha theorem; checked-use authorized binary_power_two_successor_double Alpha theorem; checked-use authorized binary_length_digit_split_exists Alpha theorem; checked-use authorized BD0006 binary_digit_half_below_double BD0005 binary_digit_horner_append

Direct dependents

BD0009 binary_exponent_digit_prefix_at_length

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

97 script commands · 24 reading checkpoints · 11 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.

Named ingredients (2)
binary digit half below doublebinary digit horner append

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.

01Induction on lL1–5

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

  1. L1
    induction l
  2. L2
    intro p
  3. L3
    intro n
  4. L4
    intro hpower
  5. L5
    intro hbound
02Establish honeL6–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two zero value.

  1. L6
    have hone : p = 1
  2. L7
    specialize binary_power_two_zero_value p
  3. L8
    apply binary_power_two_zero_value
  4. L9
    exact hpower
  5. L10
    rewrite hone at hbound
03Establish hleL11–15

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

  1. L11
    have hle : exists gap. gap + n = 0
  2. L12
    specialize le_of_succ_le_succ n
  3. L13
    specialize le_of_succ_le_succ 0
  4. L14
    apply le_of_succ_le_succ
  5. L15
    exact hbound
04Establish hzeroL16–19

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

  1. L16
    have hzero : n = 0
  2. L17
    specialize le_zero n
  3. L18
    apply le_zero
  4. L19
    exact hle
05Establish hvalueL20–25

Establish this local claim before using it. It is not an additional assumption.

  1. L20
    have hvalue : ∃ value. Horner(0,0,2,0,value)Definitions: Horner
  2. L21
    specialize beta_horner_eval_exists 0
  3. L22
    specialize beta_horner_eval_exists 0
  4. L23
    specialize beta_horner_eval_exists 2
  5. L24
    specialize beta_horner_eval_exists 0
  6. L25
    exact beta_horner_eval_exists
06Separate the logical casesL26–26

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

  1. L26
    cases hvalue
07Establish hevalzeroL27–33

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

  1. L27
    have hevalzero : x = 0
  2. L28
    specialize beta_horner_eval_empty 0
  3. L29
    specialize beta_horner_eval_empty 0
  4. L30
    specialize beta_horner_eval_empty 2
  5. L31
    specialize beta_horner_eval_empty x
  6. L32
    apply beta_horner_eval_empty
  7. L33
    exact hvalue_witness
08Establish hequalL34–38

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have hequal : x = n
  2. L35
    trans 0
  3. L36
    exact hevalzero
  4. L37
    symm
  5. L38
    exact hzero
09Construct an explicit witnessL39–40

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

  1. L39
    exists 0
  2. L40
    exists 0
10Separate the logical casesL41–41

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

  1. L41
    split
11Use earlier factsL42–44

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

  1. L42
    specialize binary_digit_prefix_empty 0
  2. L43
    specialize binary_digit_prefix_empty 0
  3. L44
    exact binary_digit_prefix_empty
12Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite <- hequal
  2. L46
    rewrite <- hequal
13Use earlier factsL47–47

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

  1. L47
    exact hvalue_witness
14Fix variables and assumptionsL48–51

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

  1. L48
    intro p
  2. L49
    intro n
  3. L50
    intro hpower
  4. L51
    intro hbound
15Establish hpreviousL52–54

Establish this local claim before using it. It is not an additional assumption.

  1. L52
    have hprevious : ∃ value. PowTwo(l,value)Definitions: PowTwo
  2. L53
    specialize binary_power_two_exists l
  3. L54
    exact binary_power_two_exists
16Separate the logical casesL55–55

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

  1. L55
    cases hprevious
17Establish hdoubleL56–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two successor double.

  1. L56
    have hdouble : p = x + x
  2. L57
    specialize binary_power_two_successor_double l
  3. L58
    specialize binary_power_two_successor_double x
  4. L59
    specialize binary_power_two_successor_double p
  5. L60
    apply binary_power_two_successor_double
  6. L61
    exact hprevious_witness
  7. L62
    exact hpower
18Establish hsplitL63–65

Establish this local claim before using it. It is not an additional assumption.

  1. L63
    have hsplit : exists half digit. ((((digit = 0) \/ (digit = 1)) /\ n = (half + half) + digit))
  2. L64
    specialize binary_length_digit_split_exists n
  3. L65
    exact binary_length_digit_split_exists
19Separate the logical casesL66–67

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

  1. L66
    cases hsplit
  2. L67
    cases hsplit_witness
20Establish hhalfL68–76

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary digit half below double.

  1. L68
    have hhalf : exists gap. gap + S x1 = x
  2. L69
    specialize binary_digit_half_below_double n
  3. L70
    specialize binary_digit_half_below_double x1
  4. L71
    specialize binary_digit_half_below_double x2
  5. L72
    specialize binary_digit_half_below_double x
  6. L73
    apply binary_digit_half_below_double
  7. L74
    exact hsplit_witness_witness
  8. L75
    rewrite hdouble at hbound
  9. L76
    exact hbound
21Establish hprefixL77–82

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

  1. L77
    have hprefix : ∃ b. ∃ c. BinaryExponentDigitCode(x1,l,b,c)Definitions: BinaryExponentDigitCode
  2. L78
    specialize IH x
  3. L79
    specialize IH x1
  4. L80
    apply IH
  5. L81
    exact hprevious_witness
  6. L82
    exact hhalf
22Separate the logical casesL83–86

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

  1. L83
    cases hprefix
  2. L84
    cases hprefix_witness
  3. L85
    cases hprefix_witness_witness
  4. L86
    cases hsplit_witness_witness
23Use earlier factsL87–96

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

  1. L87
    specialize binary_digit_horner_append x3
  2. L88
    specialize binary_digit_horner_append x4
  3. L89
    specialize binary_digit_horner_append l
  4. L90
    specialize binary_digit_horner_append x1
  5. L91
    specialize binary_digit_horner_append x2
  6. L92
    specialize binary_digit_horner_append n
  7. L93
    apply binary_digit_horner_append
  8. L94
    exact hprefix_witness_witness_left
  9. L95
    exact hprefix_witness_witness_right
  10. L96
    exact hsplit_witness_witness_left
24Use earlier factsL97–97

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

  1. L97
    exact hsplit_witness_witness_right

Library-wide reading audit

Original exact command ledger · 97 lines
  1. 0001induction l
  2. 0002intro p
  3. 0003intro n
  4. 0004intro hpower
  5. 0005intro hbound
  6. 0006have hone : p = 1
  7. 0007specialize binary_power_two_zero_value p
  8. 0008apply binary_power_two_zero_value
  9. 0009exact hpower
  10. 0010rewrite hone at hbound
  11. 0011have hle : exists gap. gap + n = 0
  12. 0012specialize le_of_succ_le_succ n
  13. 0013specialize le_of_succ_le_succ 0
  14. 0014apply le_of_succ_le_succ
  15. 0015exact hbound
  16. 0016have hzero : n = 0
  17. 0017specialize le_zero n
  18. 0018apply le_zero
  19. 0019exact hle
  20. 0020have hvalue : exists value. (exists ff_u_ph_bd_empty_value ff_v_ph_bd_empty_value. ((((exists fs_h_ph_bd_empty_value_body_start. fs_h_ph_bd_empty_value_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_empty_value)) /\ exists fs_q_ph_bd_empty_value_body_start. ff_u_ph_bd_empty_value = fs_q_ph_bd_empty_value_body_start * S ((S (0)) * ff_v_ph_bd_empty_value) + (0))) /\ ((((exists fs_h_ph_bd_empty_value_body_terminal. fs_h_ph_bd_empty_value_body_terminal + S (value) = S ((S (0)) * ff_v_ph_bd_empty_value)) /\ exists fs_q_ph_bd_empty_value_body_terminal. ff_u_ph_bd_empty_value = fs_q_ph_bd_empty_value_body_terminal * S ((S (0)) * ff_v_ph_bd_empty_value) + (value))) /\ forall ff_i_ph_bd_empty_value_body_steps. (exists ph_bound_bd_empty_value_body_steps. ph_bound_bd_empty_value_body_steps + S ff_i_ph_bd_empty_value_body_steps = 0) -> exists ff_coefficient_ph_bd_empty_value_body_steps ff_previous_ph_bd_empty_value_body_steps ff_current_ph_bd_empty_value_body_steps. ((((exists fs_h_ph_bd_empty_value_body_steps_coefficient. fs_h_ph_bd_empty_value_body_steps_coefficient + S (ff_coefficient_ph_bd_empty_value_body_steps) = S ((S (ff_i_ph_bd_empty_value_body_steps)) * 0)) /\ exists fs_q_ph_bd_empty_value_body_steps_coefficient. 0 = fs_q_ph_bd_empty_value_body_steps_coefficient * S ((S (ff_i_ph_bd_empty_value_body_steps)) * 0) + (ff_coefficient_ph_bd_empty_value_body_steps))) /\ ((((exists fs_h_ph_bd_empty_value_body_steps_before. fs_h_ph_bd_empty_value_body_steps_before + S (ff_previous_ph_bd_empty_value_body_steps) = S ((S (ff_i_ph_bd_empty_value_body_steps)) * ff_v_ph_bd_empty_value)) /\ exists fs_q_ph_bd_empty_value_body_steps_before. ff_u_ph_bd_empty_value = fs_q_ph_bd_empty_value_body_steps_before * S ((S (ff_i_ph_bd_empty_value_body_steps)) * ff_v_ph_bd_empty_value) + (ff_previous_ph_bd_empty_value_body_steps))) /\ ((((exists fs_h_ph_bd_empty_value_body_steps_after. fs_h_ph_bd_empty_value_body_steps_after + S (ff_current_ph_bd_empty_value_body_steps) = S ((S (S ff_i_ph_bd_empty_value_body_steps)) * ff_v_ph_bd_empty_value)) /\ exists fs_q_ph_bd_empty_value_body_steps_after. ff_u_ph_bd_empty_value = fs_q_ph_bd_empty_value_body_steps_after * S ((S (S ff_i_ph_bd_empty_value_body_steps)) * ff_v_ph_bd_empty_value) + (ff_current_ph_bd_empty_value_body_steps))) /\ ff_current_ph_bd_empty_value_body_steps = ff_previous_ph_bd_empty_value_body_steps * 2 + ff_coefficient_ph_bd_empty_value_body_steps))))))
  21. 0021specialize beta_horner_eval_exists 0
  22. 0022specialize beta_horner_eval_exists 0
  23. 0023specialize beta_horner_eval_exists 2
  24. 0024specialize beta_horner_eval_exists 0
  25. 0025exact beta_horner_eval_exists
  26. 0026cases hvalue
  27. 0027have hevalzero : x = 0
  28. 0028specialize beta_horner_eval_empty 0
  29. 0029specialize beta_horner_eval_empty 0
  30. 0030specialize beta_horner_eval_empty 2
  31. 0031specialize beta_horner_eval_empty x
  32. 0032apply beta_horner_eval_empty
  33. 0033exact hvalue_witness
  34. 0034have hequal : x = n
  35. 0035trans 0
  36. 0036exact hevalzero
  37. 0037symm
  38. 0038exact hzero
  39. 0039exists 0
  40. 0040exists 0
  41. 0041split
  42. 0042specialize binary_digit_prefix_empty 0
  43. 0043specialize binary_digit_prefix_empty 0
  44. 0044exact binary_digit_prefix_empty
  45. 0045rewrite <- hequal
  46. 0046rewrite <- hequal
  47. 0047exact hvalue_witness
  48. 0048intro p
  49. 0049intro n
  50. 0050intro hpower
  51. 0051intro hbound
  52. 0052have hprevious : exists value. (exists pa_b_bl_bd_previous_power pa_c_bl_bd_previous_power. ((forall pa_i_bl_bd_previous_power_repeat. (exists pa_lt_bl_bd_previous_power_repeat_bound. pa_lt_bl_bd_previous_power_repeat_bound + S pa_i_bl_bd_previous_power_repeat = l) -> (((exists pa_h_bl_bd_previous_power_repeat_decoded. pa_h_bl_bd_previous_power_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_previous_power_repeat)) * pa_c_bl_bd_previous_power)) /\ exists pa_q_bl_bd_previous_power_repeat_decoded. pa_b_bl_bd_previous_power = pa_q_bl_bd_previous_power_repeat_decoded * S ((S (pa_i_bl_bd_previous_power_repeat)) * pa_c_bl_bd_previous_power) + (2)))) /\ (exists pa_u_bl_bd_previous_power_product pa_v_bl_bd_previous_power_product. ((((exists pa_h_bl_bd_previous_power_product_start. pa_h_bl_bd_previous_power_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_previous_power_product)) /\ exists pa_q_bl_bd_previous_power_product_start. pa_u_bl_bd_previous_power_product = pa_q_bl_bd_previous_power_product_start * S ((S (0)) * pa_v_bl_bd_previous_power_product) + (1))) /\ ((((exists pa_h_bl_bd_previous_power_product_terminal. pa_h_bl_bd_previous_power_product_terminal + S (value) = S ((S (l)) * pa_v_bl_bd_previous_power_product)) /\ exists pa_q_bl_bd_previous_power_product_terminal. pa_u_bl_bd_previous_power_product = pa_q_bl_bd_previous_power_product_terminal * S ((S (l)) * pa_v_bl_bd_previous_power_product) + (value))) /\ forall pa_i_bl_bd_previous_power_product. (exists pa_lt_bl_bd_previous_power_product_bound. pa_lt_bl_bd_previous_power_product_bound + S pa_i_bl_bd_previous_power_product = l) -> exists pa_p_bl_bd_previous_power_product pa_r_bl_bd_previous_power_product pa_s_bl_bd_previous_power_product. ((((exists pa_h_bl_bd_previous_power_product_factor. pa_h_bl_bd_previous_power_product_factor + S (pa_p_bl_bd_previous_power_product) = S ((S (pa_i_bl_bd_previous_power_product)) * pa_c_bl_bd_previous_power)) /\ exists pa_q_bl_bd_previous_power_product_factor. pa_b_bl_bd_previous_power = pa_q_bl_bd_previous_power_product_factor * S ((S (pa_i_bl_bd_previous_power_product)) * pa_c_bl_bd_previous_power) + (pa_p_bl_bd_previous_power_product))) /\ ((((exists pa_h_bl_bd_previous_power_product_partial. pa_h_bl_bd_previous_power_product_partial + S (pa_r_bl_bd_previous_power_product) = S ((S (pa_i_bl_bd_previous_power_product)) * pa_v_bl_bd_previous_power_product)) /\ exists pa_q_bl_bd_previous_power_product_partial. pa_u_bl_bd_previous_power_product = pa_q_bl_bd_previous_power_product_partial * S ((S (pa_i_bl_bd_previous_power_product)) * pa_v_bl_bd_previous_power_product) + (pa_r_bl_bd_previous_power_product))) /\ ((((exists pa_h_bl_bd_previous_power_product_successor. pa_h_bl_bd_previous_power_product_successor + S (pa_s_bl_bd_previous_power_product) = S ((S (S pa_i_bl_bd_previous_power_product)) * pa_v_bl_bd_previous_power_product)) /\ exists pa_q_bl_bd_previous_power_product_successor. pa_u_bl_bd_previous_power_product = pa_q_bl_bd_previous_power_product_successor * S ((S (S pa_i_bl_bd_previous_power_product)) * pa_v_bl_bd_previous_power_product) + (pa_s_bl_bd_previous_power_product))) /\ pa_s_bl_bd_previous_power_product = pa_r_bl_bd_previous_power_product * pa_p_bl_bd_previous_power_product))))))))
  53. 0053specialize binary_power_two_exists l
  54. 0054exact binary_power_two_exists
  55. 0055cases hprevious
  56. 0056have hdouble : p = x + x
  57. 0057specialize binary_power_two_successor_double l
  58. 0058specialize binary_power_two_successor_double x
  59. 0059specialize binary_power_two_successor_double p
  60. 0060apply binary_power_two_successor_double
  61. 0061exact hprevious_witness
  62. 0062exact hpower
  63. 0063have hsplit : exists half digit. ((((digit = 0) \/ (digit = 1)) /\ n = (half + half) + digit))
  64. 0064specialize binary_length_digit_split_exists n
  65. 0065exact binary_length_digit_split_exists
  66. 0066cases hsplit
  67. 0067cases hsplit_witness
  68. 0068have hhalf : exists gap. gap + S x1 = x
  69. 0069specialize binary_digit_half_below_double n
  70. 0070specialize binary_digit_half_below_double x1
  71. 0071specialize binary_digit_half_below_double x2
  72. 0072specialize binary_digit_half_below_double x
  73. 0073apply binary_digit_half_below_double
  74. 0074exact hsplit_witness_witness
  75. 0075rewrite hdouble at hbound
  76. 0076exact hbound
  77. 0077have hprefix : exists b c. (((forall ff_index_be_bd_bounded_predecessor_digits ff_digit_be_bd_bounded_predecessor_digits. (exists ff_lt_be_bd_bounded_predecessor_digits_bound. ff_lt_be_bd_bounded_predecessor_digits_bound + S ff_index_be_bd_bounded_predecessor_digits = l) -> (((exists ff_h_be_bd_bounded_predecessor_digits_digit. ff_h_be_bd_bounded_predecessor_digits_digit + S (ff_digit_be_bd_bounded_predecessor_digits) = S ((S (ff_index_be_bd_bounded_predecessor_digits)) * c)) /\ exists ff_q_be_bd_bounded_predecessor_digits_digit. b = ff_q_be_bd_bounded_predecessor_digits_digit * S ((S (ff_index_be_bd_bounded_predecessor_digits)) * c) + (ff_digit_be_bd_bounded_predecessor_digits))) -> (ff_digit_be_bd_bounded_predecessor_digits = 0 \/ ff_digit_be_bd_bounded_predecessor_digits = 1)) /\ (exists ff_u_ph_bd_bounded_predecessor_horner ff_v_ph_bd_bounded_predecessor_horner. ((((exists fs_h_ph_bd_bounded_predecessor_horner_body_start. fs_h_ph_bd_bounded_predecessor_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_bounded_predecessor_horner)) /\ exists fs_q_ph_bd_bounded_predecessor_horner_body_start. ff_u_ph_bd_bounded_predecessor_horner = fs_q_ph_bd_bounded_predecessor_horner_body_start * S ((S (0)) * ff_v_ph_bd_bounded_predecessor_horner) + (0))) /\ ((((exists fs_h_ph_bd_bounded_predecessor_horner_body_terminal. fs_h_ph_bd_bounded_predecessor_horner_body_terminal + S (x1) = S ((S (l)) * ff_v_ph_bd_bounded_predecessor_horner)) /\ exists fs_q_ph_bd_bounded_predecessor_horner_body_terminal. ff_u_ph_bd_bounded_predecessor_horner = fs_q_ph_bd_bounded_predecessor_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_bounded_predecessor_horner) + (x1))) /\ forall ff_i_ph_bd_bounded_predecessor_horner_body_steps. (exists ph_bound_bd_bounded_predecessor_horner_body_steps. ph_bound_bd_bounded_predecessor_horner_body_steps + S ff_i_ph_bd_bounded_predecessor_horner_body_steps = l) -> exists ff_coefficient_ph_bd_bounded_predecessor_horner_body_steps ff_previous_ph_bd_bounded_predecessor_horner_body_steps ff_current_ph_bd_bounded_predecessor_horner_body_steps. ((((exists fs_h_ph_bd_bounded_predecessor_horner_body_steps_coefficient. fs_h_ph_bd_bounded_predecessor_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_bounded_predecessor_horner_body_steps) = S ((S (ff_i_ph_bd_bounded_predecessor_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_bounded_predecessor_horner_body_steps_coefficient. b = fs_q_ph_bd_bounded_predecessor_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_bounded_predecessor_horner_body_steps)) * c) + (ff_coefficient_ph_bd_bounded_predecessor_horner_body_steps))) /\ ((((exists fs_h_ph_bd_bounded_predecessor_horner_body_steps_before. fs_h_ph_bd_bounded_predecessor_horner_body_steps_before + S (ff_previous_ph_bd_bounded_predecessor_horner_body_steps) = S ((S (ff_i_ph_bd_bounded_predecessor_horner_body_steps)) * ff_v_ph_bd_bounded_predecessor_horner)) /\ exists fs_q_ph_bd_bounded_predecessor_horner_body_steps_before. ff_u_ph_bd_bounded_predecessor_horner = fs_q_ph_bd_bounded_predecessor_horner_body_steps_before * S ((S (ff_i_ph_bd_bounded_predecessor_horner_body_steps)) * ff_v_ph_bd_bounded_predecessor_horner) + (ff_previous_ph_bd_bounded_predecessor_horner_body_steps))) /\ ((((exists fs_h_ph_bd_bounded_predecessor_horner_body_steps_after. fs_h_ph_bd_bounded_predecessor_horner_body_steps_after + S (ff_current_ph_bd_bounded_predecessor_horner_body_steps) = S ((S (S ff_i_ph_bd_bounded_predecessor_horner_body_steps)) * ff_v_ph_bd_bounded_predecessor_horner)) /\ exists fs_q_ph_bd_bounded_predecessor_horner_body_steps_after. ff_u_ph_bd_bounded_predecessor_horner = fs_q_ph_bd_bounded_predecessor_horner_body_steps_after * S ((S (S ff_i_ph_bd_bounded_predecessor_horner_body_steps)) * ff_v_ph_bd_bounded_predecessor_horner) + (ff_current_ph_bd_bounded_predecessor_horner_body_steps))) /\ ff_current_ph_bd_bounded_predecessor_horner_body_steps = ff_previous_ph_bd_bounded_predecessor_horner_body_steps * 2 + ff_coefficient_ph_bd_bounded_predecessor_horner_body_steps))))))))
  78. 0078specialize IH x
  79. 0079specialize IH x1
  80. 0080apply IH
  81. 0081exact hprevious_witness
  82. 0082exact hhalf
  83. 0083cases hprefix
  84. 0084cases hprefix_witness
  85. 0085cases hprefix_witness_witness
  86. 0086cases hsplit_witness_witness
  87. 0087specialize binary_digit_horner_append x3
  88. 0088specialize binary_digit_horner_append x4
  89. 0089specialize binary_digit_horner_append l
  90. 0090specialize binary_digit_horner_append x1
  91. 0091specialize binary_digit_horner_append x2
  92. 0092specialize binary_digit_horner_append n
  93. 0093apply binary_digit_horner_append
  94. 0094exact hprefix_witness_witness_left
  95. 0095exact hprefix_witness_witness_right
  96. 0096exact hsplit_witness_witness_left
  97. 0097exact hsplit_witness_witness_right

Separate complete second-wave branches: Full T13 proof · Alpha v27.