PC0026

binary_half_scale_bounds

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

The power-of-two threshold at half the lower exponent has square at most N, while ell is at most both 2U and 3h.

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 N ell e h d U V. ell = S e -> e = (h + h) + d -> (d = 0 \/ d = 1) -> (exists pc_le_half_scale_length. pc_le_half_scale_length + (5) = (ell)) -> (exists pa_b_pc_half_scale_power pa_c_pc_half_scale_power. ((forall pa_i_pc_half_scale_power_repeat. (exists pa_lt_pc_half_scale_power_repeat_bound. pa_lt_pc_half_scale_power_repeat_bound + S pa_i_pc_half_scale_power_repeat = h) -> (((exists pa_h_pc_half_scale_power_repeat_decoded. pa_h_pc_half_scale_power_repeat_decoded + S (2) = S ((S (pa_i_pc_half_scale_power_repeat)) * pa_c_pc_half_scale_power)) /\ exists pa_q_pc_half_scale_power_repeat_decoded. pa_b_pc_half_scale_power = pa_q_pc_half_scale_power_repeat_decoded * S ((S (pa_i_pc_half_scale_power_repeat)) * pa_c_pc_half_scale_power) + (2)))) /\ (exists pa_u_pc_half_scale_power_product pa_v_pc_half_scale_power_product. ((((exists pa_h_pc_half_scale_power_product_start. pa_h_pc_half_scale_power_product_start + S (1) = S ((S (0)) * pa_v_pc_half_scale_power_product)) /\ exists pa_q_pc_half_scale_power_product_start. pa_u_pc_half_scale_power_product = pa_q_pc_half_scale_power_product_start * S ((S (0)) * pa_v_pc_half_scale_power_product) + (1))) /\ ((((exists pa_h_pc_half_scale_power_product_terminal. pa_h_pc_half_scale_power_product_terminal + S (U) = S ((S (h)) * pa_v_pc_half_scale_power_product)) /\ exists pa_q_pc_half_scale_power_product_terminal. pa_u_pc_half_scale_power_product = pa_q_pc_half_scale_power_product_terminal * S ((S (h)) * pa_v_pc_half_scale_power_product) + (U))) /\ forall pa_i_pc_half_scale_power_product. (exists pa_lt_pc_half_scale_power_product_bound. pa_lt_pc_half_scale_power_product_bound + S pa_i_pc_half_scale_power_product = h) -> exists pa_p_pc_half_scale_power_product pa_r_pc_half_scale_power_product pa_s_pc_half_scale_power_product. ((((exists pa_h_pc_half_scale_power_product_factor. pa_h_pc_half_scale_power_product_factor + S (pa_p_pc_half_scale_power_product) = S ((S (pa_i_pc_half_scale_power_product)) * pa_c_pc_half_scale_power)) /\ exists pa_q_pc_half_scale_power_product_factor. pa_b_pc_half_scale_power = pa_q_pc_half_scale_power_product_factor * S ((S (pa_i_pc_half_scale_power_product)) * pa_c_pc_half_scale_power) + (pa_p_pc_half_scale_power_product))) /\ ((((exists pa_h_pc_half_scale_power_product_partial. pa_h_pc_half_scale_power_product_partial + S (pa_r_pc_half_scale_power_product) = S ((S (pa_i_pc_half_scale_power_product)) * pa_v_pc_half_scale_power_product)) /\ exists pa_q_pc_half_scale_power_product_partial. pa_u_pc_half_scale_power_product = pa_q_pc_half_scale_power_product_partial * S ((S (pa_i_pc_half_scale_power_product)) * pa_v_pc_half_scale_power_product) + (pa_r_pc_half_scale_power_product))) /\ ((((exists pa_h_pc_half_scale_power_product_successor. pa_h_pc_half_scale_power_product_successor + S (pa_s_pc_half_scale_power_product) = S ((S (S pa_i_pc_half_scale_power_product)) * pa_v_pc_half_scale_power_product)) /\ exists pa_q_pc_half_scale_power_product_successor. pa_u_pc_half_scale_power_product = pa_q_pc_half_scale_power_product_successor * S ((S (S pa_i_pc_half_scale_power_product)) * pa_v_pc_half_scale_power_product) + (pa_s_pc_half_scale_power_product))) /\ pa_s_pc_half_scale_power_product = pa_r_pc_half_scale_power_product * pa_p_pc_half_scale_power_product)))))))) -> (exists pa_b_pc_half_scale_lower_power pa_c_pc_half_scale_lower_power. ((forall pa_i_pc_half_scale_lower_power_repeat. (exists pa_lt_pc_half_scale_lower_power_repeat_bound. pa_lt_pc_half_scale_lower_power_repeat_bound + S pa_i_pc_half_scale_lower_power_repeat = e) -> (((exists pa_h_pc_half_scale_lower_power_repeat_decoded. pa_h_pc_half_scale_lower_power_repeat_decoded + S (2) = S ((S (pa_i_pc_half_scale_lower_power_repeat)) * pa_c_pc_half_scale_lower_power)) /\ exists pa_q_pc_half_scale_lower_power_repeat_decoded. pa_b_pc_half_scale_lower_power = pa_q_pc_half_scale_lower_power_repeat_decoded * S ((S (pa_i_pc_half_scale_lower_power_repeat)) * pa_c_pc_half_scale_lower_power) + (2)))) /\ (exists pa_u_pc_half_scale_lower_power_product pa_v_pc_half_scale_lower_power_product. ((((exists pa_h_pc_half_scale_lower_power_product_start. pa_h_pc_half_scale_lower_power_product_start + S (1) = S ((S (0)) * pa_v_pc_half_scale_lower_power_product)) /\ exists pa_q_pc_half_scale_lower_power_product_start. pa_u_pc_half_scale_lower_power_product = pa_q_pc_half_scale_lower_power_product_start * S ((S (0)) * pa_v_pc_half_scale_lower_power_product) + (1))) /\ ((((exists pa_h_pc_half_scale_lower_power_product_terminal. pa_h_pc_half_scale_lower_power_product_terminal + S (V) = S ((S (e)) * pa_v_pc_half_scale_lower_power_product)) /\ exists pa_q_pc_half_scale_lower_power_product_terminal. pa_u_pc_half_scale_lower_power_product = pa_q_pc_half_scale_lower_power_product_terminal * S ((S (e)) * pa_v_pc_half_scale_lower_power_product) + (V))) /\ forall pa_i_pc_half_scale_lower_power_product. (exists pa_lt_pc_half_scale_lower_power_product_bound. pa_lt_pc_half_scale_lower_power_product_bound + S pa_i_pc_half_scale_lower_power_product = e) -> exists pa_p_pc_half_scale_lower_power_product pa_r_pc_half_scale_lower_power_product pa_s_pc_half_scale_lower_power_product. ((((exists pa_h_pc_half_scale_lower_power_product_factor. pa_h_pc_half_scale_lower_power_product_factor + S (pa_p_pc_half_scale_lower_power_product) = S ((S (pa_i_pc_half_scale_lower_power_product)) * pa_c_pc_half_scale_lower_power)) /\ exists pa_q_pc_half_scale_lower_power_product_factor. pa_b_pc_half_scale_lower_power = pa_q_pc_half_scale_lower_power_product_factor * S ((S (pa_i_pc_half_scale_lower_power_product)) * pa_c_pc_half_scale_lower_power) + (pa_p_pc_half_scale_lower_power_product))) /\ ((((exists pa_h_pc_half_scale_lower_power_product_partial. pa_h_pc_half_scale_lower_power_product_partial + S (pa_r_pc_half_scale_lower_power_product) = S ((S (pa_i_pc_half_scale_lower_power_product)) * pa_v_pc_half_scale_lower_power_product)) /\ exists pa_q_pc_half_scale_lower_power_product_partial. pa_u_pc_half_scale_lower_power_product = pa_q_pc_half_scale_lower_power_product_partial * S ((S (pa_i_pc_half_scale_lower_power_product)) * pa_v_pc_half_scale_lower_power_product) + (pa_r_pc_half_scale_lower_power_product))) /\ ((((exists pa_h_pc_half_scale_lower_power_product_successor. pa_h_pc_half_scale_lower_power_product_successor + S (pa_s_pc_half_scale_lower_power_product) = S ((S (S pa_i_pc_half_scale_lower_power_product)) * pa_v_pc_half_scale_lower_power_product)) /\ exists pa_q_pc_half_scale_lower_power_product_successor. pa_u_pc_half_scale_lower_power_product = pa_q_pc_half_scale_lower_power_product_successor * S ((S (S pa_i_pc_half_scale_lower_power_product)) * pa_v_pc_half_scale_lower_power_product) + (pa_s_pc_half_scale_lower_power_product))) /\ pa_s_pc_half_scale_lower_power_product = pa_r_pc_half_scale_lower_power_product * pa_p_pc_half_scale_lower_power_product)))))))) -> (exists pc_le_half_scale_lower. pc_le_half_scale_lower + (V) = (N)) -> (exists pc_le_half_scale_half_positive. pc_le_half_scale_half_positive + (2) = (h)) /\ ((exists pc_le_half_scale_square. pc_le_half_scale_square + (U * U) = (N)) /\ ((exists pc_le_half_scale_twice. pc_le_half_scale_twice + (ell) = (2 * U)) /\ (exists pc_le_half_scale_thrice. pc_le_half_scale_thrice + (ell) = (3 * h))))

Constructive proof overview

Generated structural guide

The power-of-two threshold at half the lower exponent has square at most N, while ell is at most both 2U and 3h.

The unchanged tactic script uses 12 declared prerequisites and contains 112 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_of_succ_le_succ Stable theorem; checked-use authorized PC0021 binary_split_half_lower_bound pow_exists Stable theorem; checked-use authorized pow_add Stable theorem; checked-use authorized binary_power_two_exponent_monotone Alpha theorem; checked-use authorized le_add_right Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized PC0022 binary_split_successor_le_double_successor PC0015 binary_power_two_dominates_successor euclidean_log_double_monotone Alpha theorem; checked-use authorized pairing_double_equals_two_mul Alpha theorem; checked-use authorized PC0023 double_successor_le_triple_above_one

Direct dependents

PC002A prime_count_chebyshev_upper

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

112 script commands · 22 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 (4)
binary split half lower boundbinary split successor le double successorbinary power two dominates successordouble successor le triple above one

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro ell
  3. L3
    intro e
  4. L4
    intro h
  5. L5
    intro d
  6. L6
    intro U
  7. L7
    intro V
  8. L8
    intro hl
  9. L9
    intro he
  10. L10
    intro hd
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hell
  2. L12
    intro hU
  3. L13
    intro hV
  4. L14
    intro hVN
03Establish he4L15–20

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

  1. L15
    have he4 : exists g. g + 4 = e
  2. L16
    specialize le_of_succ_le_succ 4
  3. L17
    specialize le_of_succ_le_succ e
  4. L18
    apply le_of_succ_le_succ
  5. L19
    rewrite <- hl
  6. L20
    exact hell
04Establish hh2L21–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary split half lower bound.

  1. L21
    have hh2 : exists g. g + 2 = h
  2. L22
    specialize binary_split_half_lower_bound e
  3. L23
    specialize binary_split_half_lower_bound h
  4. L24
    specialize binary_split_half_lower_bound d
  5. L25
    specialize binary_split_half_lower_bound 2
  6. L26
    apply binary_split_half_lower_bound
  7. L27
    exact hd
  8. L28
    exact he
05Establish hfourL29–32

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

  1. L29
    have hfour : 2 + 2 = 4
  2. L30
    norm_num
  3. L31
    rewrite hfour
  4. L32
    exact he4
06Establish hWL33–36

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

  1. L33
    have hW : ∃ W. PowTwo(h + h,W)Definitions: PowTwo
  2. L34
    specialize pow_exists 2
  3. L35
    specialize pow_exists (h + h)
  4. L36
    apply pow_exists
07Separate the logical casesL37–37

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

  1. L37
    cases hW
08Establish hsquareL38–47

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

  1. L38
    have hsquare : x = U * U
  2. L39
    specialize pow_add 2
  3. L40
    specialize pow_add h
  4. L41
    specialize pow_add h
  5. L42
    specialize pow_add (h + h)
  6. L43
    specialize pow_add U
  7. L44
    specialize pow_add U
  8. L45
    specialize pow_add x
  9. L46
    apply pow_add
  10. L47
    refl
09Use earlier factsL48–50

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

  1. L48
    exact hU
  2. L49
    exact hU
  3. L50
    exact hW_witness
10Establish hUVL51–60

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

  1. L51
    have hUV : exists g. g + x = V
  2. L52
    specialize binary_power_two_exponent_monotone (h + h)
  3. L53
    specialize binary_power_two_exponent_monotone e
  4. L54
    specialize binary_power_two_exponent_monotone x
  5. L55
    specialize binary_power_two_exponent_monotone V
  6. L56
    apply binary_power_two_exponent_monotone
  7. L57
    rewrite he
  8. L58
    specialize le_add_right (h + h)
  9. L59
    specialize le_add_right d
  10. L60
    apply le_add_right
11Use earlier factsL61–62

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

  1. L61
    exact hW_witness
  2. L62
    exact hV
12Establish hsquareNL63–70

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

  1. L63
    have hsquareN : exists g. g + U * U = N
  2. L64
    rewrite <- hsquare
  3. L65
    specialize le_trans x
  4. L66
    specialize le_trans V
  5. L67
    specialize le_trans N
  6. L68
    apply le_trans
  7. L69
    exact hUV
  8. L70
    exact hVN
13Establish hlengthhalfL71–79

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

  1. L71
    have hlengthhalf : exists g. g + ell = S h + S h
  2. L72
    specialize binary_split_successor_le_double_successor e
  3. L73
    specialize binary_split_successor_le_double_successor h
  4. L74
    specialize binary_split_successor_le_double_successor d
  5. L75
    specialize binary_split_successor_le_double_successor ell
  6. L76
    apply binary_split_successor_le_double_successor
  7. L77
    exact hd
  8. L78
    exact he
  9. L79
    exact hl
14Establish hhalfpowerL80–84

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

  1. L80
    have hhalfpower : exists g. g + S h = U
  2. L81
    specialize binary_power_two_dominates_successor h
  3. L82
    specialize binary_power_two_dominates_successor U
  4. L83
    apply binary_power_two_dominates_successor
  5. L84
    exact hU
15Establish hlengthpowerL85–94

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

  1. L85
    have hlengthpower : exists g. g + ell = U + U
  2. L86
    specialize le_trans ell
  3. L87
    specialize le_trans (S h + S h)
  4. L88
    specialize le_trans (U + U)
  5. L89
    apply le_trans
  6. L90
    exact hlengthhalf
  7. L91
    specialize euclidean_log_double_monotone (S h)
  8. L92
    specialize euclidean_log_double_monotone U
  9. L93
    apply euclidean_log_double_monotone
  10. L94
    exact hhalfpower
16Separate the logical casesL95–95

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

  1. L95
    split
17Use earlier factsL96–96

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

  1. L96
    exact hh2
18Separate the logical casesL97–97

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

  1. L97
    split
19Use earlier factsL98–98

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

  1. L98
    exact hsquareN
20Separate the logical casesL99–99

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

  1. L99
    split
21Establish hdoubleL100–109

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pairing double equals two mul.

  1. L100
    have hdouble : U + U = 2 * U
  2. L101
    specialize pairing_double_equals_two_mul U
  3. L102
    apply pairing_double_equals_two_mul
  4. L103
    rewrite hdouble at hlengthpower
  5. L104
    exact hlengthpower
  6. L105
    specialize le_trans ell
  7. L106
    specialize le_trans (S h + S h)
  8. L107
    specialize le_trans (3 * h)
  9. L108
    apply le_trans
  10. L109
    exact hlengthhalf
22Use earlier factsL110–112

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

  1. L110
    specialize double_successor_le_triple_above_one h
  2. L111
    apply double_successor_le_triple_above_one
  3. L112
    exact hh2

Library-wide reading audit

Original exact command ledger · 112 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro e
  4. 0004intro h
  5. 0005intro d
  6. 0006intro U
  7. 0007intro V
  8. 0008intro hl
  9. 0009intro he
  10. 0010intro hd
  11. 0011intro hell
  12. 0012intro hU
  13. 0013intro hV
  14. 0014intro hVN
  15. 0015have he4 : exists g. g + 4 = e
  16. 0016specialize le_of_succ_le_succ 4
  17. 0017specialize le_of_succ_le_succ e
  18. 0018apply le_of_succ_le_succ
  19. 0019rewrite <- hl
  20. 0020exact hell
  21. 0021have hh2 : exists g. g + 2 = h
  22. 0022specialize binary_split_half_lower_bound e
  23. 0023specialize binary_split_half_lower_bound h
  24. 0024specialize binary_split_half_lower_bound d
  25. 0025specialize binary_split_half_lower_bound 2
  26. 0026apply binary_split_half_lower_bound
  27. 0027exact hd
  28. 0028exact he
  29. 0029have hfour : 2 + 2 = 4
  30. 0030norm_num
  31. 0031rewrite hfour
  32. 0032exact he4
  33. 0033have hW : exists W. exists pa_b_pc_half_scale_square_power pa_c_pc_half_scale_square_power. ((forall pa_i_pc_half_scale_square_power_repeat. (exists pa_lt_pc_half_scale_square_power_repeat_bound. pa_lt_pc_half_scale_square_power_repeat_bound + S pa_i_pc_half_scale_square_power_repeat = h + h) -> (((exists pa_h_pc_half_scale_square_power_repeat_decoded. pa_h_pc_half_scale_square_power_repeat_decoded + S (2) = S ((S (pa_i_pc_half_scale_square_power_repeat)) * pa_c_pc_half_scale_square_power)) /\ exists pa_q_pc_half_scale_square_power_repeat_decoded. pa_b_pc_half_scale_square_power = pa_q_pc_half_scale_square_power_repeat_decoded * S ((S (pa_i_pc_half_scale_square_power_repeat)) * pa_c_pc_half_scale_square_power) + (2)))) /\ (exists pa_u_pc_half_scale_square_power_product pa_v_pc_half_scale_square_power_product. ((((exists pa_h_pc_half_scale_square_power_product_start. pa_h_pc_half_scale_square_power_product_start + S (1) = S ((S (0)) * pa_v_pc_half_scale_square_power_product)) /\ exists pa_q_pc_half_scale_square_power_product_start. pa_u_pc_half_scale_square_power_product = pa_q_pc_half_scale_square_power_product_start * S ((S (0)) * pa_v_pc_half_scale_square_power_product) + (1))) /\ ((((exists pa_h_pc_half_scale_square_power_product_terminal. pa_h_pc_half_scale_square_power_product_terminal + S (W) = S ((S (h + h)) * pa_v_pc_half_scale_square_power_product)) /\ exists pa_q_pc_half_scale_square_power_product_terminal. pa_u_pc_half_scale_square_power_product = pa_q_pc_half_scale_square_power_product_terminal * S ((S (h + h)) * pa_v_pc_half_scale_square_power_product) + (W))) /\ forall pa_i_pc_half_scale_square_power_product. (exists pa_lt_pc_half_scale_square_power_product_bound. pa_lt_pc_half_scale_square_power_product_bound + S pa_i_pc_half_scale_square_power_product = h + h) -> exists pa_p_pc_half_scale_square_power_product pa_r_pc_half_scale_square_power_product pa_s_pc_half_scale_square_power_product. ((((exists pa_h_pc_half_scale_square_power_product_factor. pa_h_pc_half_scale_square_power_product_factor + S (pa_p_pc_half_scale_square_power_product) = S ((S (pa_i_pc_half_scale_square_power_product)) * pa_c_pc_half_scale_square_power)) /\ exists pa_q_pc_half_scale_square_power_product_factor. pa_b_pc_half_scale_square_power = pa_q_pc_half_scale_square_power_product_factor * S ((S (pa_i_pc_half_scale_square_power_product)) * pa_c_pc_half_scale_square_power) + (pa_p_pc_half_scale_square_power_product))) /\ ((((exists pa_h_pc_half_scale_square_power_product_partial. pa_h_pc_half_scale_square_power_product_partial + S (pa_r_pc_half_scale_square_power_product) = S ((S (pa_i_pc_half_scale_square_power_product)) * pa_v_pc_half_scale_square_power_product)) /\ exists pa_q_pc_half_scale_square_power_product_partial. pa_u_pc_half_scale_square_power_product = pa_q_pc_half_scale_square_power_product_partial * S ((S (pa_i_pc_half_scale_square_power_product)) * pa_v_pc_half_scale_square_power_product) + (pa_r_pc_half_scale_square_power_product))) /\ ((((exists pa_h_pc_half_scale_square_power_product_successor. pa_h_pc_half_scale_square_power_product_successor + S (pa_s_pc_half_scale_square_power_product) = S ((S (S pa_i_pc_half_scale_square_power_product)) * pa_v_pc_half_scale_square_power_product)) /\ exists pa_q_pc_half_scale_square_power_product_successor. pa_u_pc_half_scale_square_power_product = pa_q_pc_half_scale_square_power_product_successor * S ((S (S pa_i_pc_half_scale_square_power_product)) * pa_v_pc_half_scale_square_power_product) + (pa_s_pc_half_scale_square_power_product))) /\ pa_s_pc_half_scale_square_power_product = pa_r_pc_half_scale_square_power_product * pa_p_pc_half_scale_square_power_product)))))))
  34. 0034specialize pow_exists 2
  35. 0035specialize pow_exists (h + h)
  36. 0036apply pow_exists
  37. 0037cases hW
  38. 0038have hsquare : x = U * U
  39. 0039specialize pow_add 2
  40. 0040specialize pow_add h
  41. 0041specialize pow_add h
  42. 0042specialize pow_add (h + h)
  43. 0043specialize pow_add U
  44. 0044specialize pow_add U
  45. 0045specialize pow_add x
  46. 0046apply pow_add
  47. 0047refl
  48. 0048exact hU
  49. 0049exact hU
  50. 0050exact hW_witness
  51. 0051have hUV : exists g. g + x = V
  52. 0052specialize binary_power_two_exponent_monotone (h + h)
  53. 0053specialize binary_power_two_exponent_monotone e
  54. 0054specialize binary_power_two_exponent_monotone x
  55. 0055specialize binary_power_two_exponent_monotone V
  56. 0056apply binary_power_two_exponent_monotone
  57. 0057rewrite he
  58. 0058specialize le_add_right (h + h)
  59. 0059specialize le_add_right d
  60. 0060apply le_add_right
  61. 0061exact hW_witness
  62. 0062exact hV
  63. 0063have hsquareN : exists g. g + U * U = N
  64. 0064rewrite <- hsquare
  65. 0065specialize le_trans x
  66. 0066specialize le_trans V
  67. 0067specialize le_trans N
  68. 0068apply le_trans
  69. 0069exact hUV
  70. 0070exact hVN
  71. 0071have hlengthhalf : exists g. g + ell = S h + S h
  72. 0072specialize binary_split_successor_le_double_successor e
  73. 0073specialize binary_split_successor_le_double_successor h
  74. 0074specialize binary_split_successor_le_double_successor d
  75. 0075specialize binary_split_successor_le_double_successor ell
  76. 0076apply binary_split_successor_le_double_successor
  77. 0077exact hd
  78. 0078exact he
  79. 0079exact hl
  80. 0080have hhalfpower : exists g. g + S h = U
  81. 0081specialize binary_power_two_dominates_successor h
  82. 0082specialize binary_power_two_dominates_successor U
  83. 0083apply binary_power_two_dominates_successor
  84. 0084exact hU
  85. 0085have hlengthpower : exists g. g + ell = U + U
  86. 0086specialize le_trans ell
  87. 0087specialize le_trans (S h + S h)
  88. 0088specialize le_trans (U + U)
  89. 0089apply le_trans
  90. 0090exact hlengthhalf
  91. 0091specialize euclidean_log_double_monotone (S h)
  92. 0092specialize euclidean_log_double_monotone U
  93. 0093apply euclidean_log_double_monotone
  94. 0094exact hhalfpower
  95. 0095split
  96. 0096exact hh2
  97. 0097split
  98. 0098exact hsquareN
  99. 0099split
  100. 0100have hdouble : U + U = 2 * U
  101. 0101specialize pairing_double_equals_two_mul U
  102. 0102apply pairing_double_equals_two_mul
  103. 0103rewrite hdouble at hlengthpower
  104. 0104exact hlengthpower
  105. 0105specialize le_trans ell
  106. 0106specialize le_trans (S h + S h)
  107. 0107specialize le_trans (3 * h)
  108. 0108apply le_trans
  109. 0109exact hlengthhalf
  110. 0110specialize double_successor_le_triple_above_one h
  111. 0111apply double_successor_le_triple_above_one
  112. 0112exact hh2