PC000D

beta_product_bit_weighted_lower_power

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

An actual bit-weighted finite product has the corresponding lower bound by a power of its actual bit sum.

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 b c d f B l z k Q. (forall pc_index_weight_lower_source pc_factor_weight_lower_source pc_bit_weight_lower_source. (exists pc_lt_weight_lower_source_index. pc_lt_weight_lower_source_index + S (pc_index_weight_lower_source) = (l)) -> (((exists fs_h_pc_weight_lower_source_factor. fs_h_pc_weight_lower_source_factor + S (pc_factor_weight_lower_source) = S ((S (pc_index_weight_lower_source)) * c)) /\ exists fs_q_pc_weight_lower_source_factor. b = fs_q_pc_weight_lower_source_factor * S ((S (pc_index_weight_lower_source)) * c) + (pc_factor_weight_lower_source))) -> (((exists fs_h_pc_weight_lower_source_bit. fs_h_pc_weight_lower_source_bit + S (pc_bit_weight_lower_source) = S ((S (pc_index_weight_lower_source)) * f)) /\ exists fs_q_pc_weight_lower_source_bit. d = fs_q_pc_weight_lower_source_bit * S ((S (pc_index_weight_lower_source)) * f) + (pc_bit_weight_lower_source))) -> ((pc_bit_weight_lower_source = 0 /\ (exists pc_le_weight_lower_source_zero. pc_le_weight_lower_source_zero + (1) = (pc_factor_weight_lower_source))) \/ (pc_bit_weight_lower_source = 1 /\ (exists pc_le_weight_lower_source_one. pc_le_weight_lower_source_one + (B) = (pc_factor_weight_lower_source))))) -> (exists ff_u_pc_weight_lower_product ff_v_pc_weight_lower_product. ((((exists ff_h_pc_weight_lower_product_start. ff_h_pc_weight_lower_product_start + S (1) = S ((S (0)) * ff_v_pc_weight_lower_product)) /\ exists ff_q_pc_weight_lower_product_start. ff_u_pc_weight_lower_product = ff_q_pc_weight_lower_product_start * S ((S (0)) * ff_v_pc_weight_lower_product) + (1))) /\ ((((exists ff_h_pc_weight_lower_product_terminal. ff_h_pc_weight_lower_product_terminal + S (z) = S ((S (l)) * ff_v_pc_weight_lower_product)) /\ exists ff_q_pc_weight_lower_product_terminal. ff_u_pc_weight_lower_product = ff_q_pc_weight_lower_product_terminal * S ((S (l)) * ff_v_pc_weight_lower_product) + (z))) /\ forall ff_i_pc_weight_lower_product. (exists ff_lt_pc_weight_lower_product_bound. ff_lt_pc_weight_lower_product_bound + S ff_i_pc_weight_lower_product = l) -> exists ff_p_pc_weight_lower_product ff_r_pc_weight_lower_product ff_s_pc_weight_lower_product. ((((exists ff_h_pc_weight_lower_product_factor. ff_h_pc_weight_lower_product_factor + S (ff_p_pc_weight_lower_product) = S ((S (ff_i_pc_weight_lower_product)) * c)) /\ exists ff_q_pc_weight_lower_product_factor. b = ff_q_pc_weight_lower_product_factor * S ((S (ff_i_pc_weight_lower_product)) * c) + (ff_p_pc_weight_lower_product))) /\ ((((exists ff_h_pc_weight_lower_product_partial. ff_h_pc_weight_lower_product_partial + S (ff_r_pc_weight_lower_product) = S ((S (ff_i_pc_weight_lower_product)) * ff_v_pc_weight_lower_product)) /\ exists ff_q_pc_weight_lower_product_partial. ff_u_pc_weight_lower_product = ff_q_pc_weight_lower_product_partial * S ((S (ff_i_pc_weight_lower_product)) * ff_v_pc_weight_lower_product) + (ff_r_pc_weight_lower_product))) /\ ((((exists ff_h_pc_weight_lower_product_successor. ff_h_pc_weight_lower_product_successor + S (ff_s_pc_weight_lower_product) = S ((S (S ff_i_pc_weight_lower_product)) * ff_v_pc_weight_lower_product)) /\ exists ff_q_pc_weight_lower_product_successor. ff_u_pc_weight_lower_product = ff_q_pc_weight_lower_product_successor * S ((S (S ff_i_pc_weight_lower_product)) * ff_v_pc_weight_lower_product) + (ff_s_pc_weight_lower_product))) /\ ff_s_pc_weight_lower_product = ff_r_pc_weight_lower_product * ff_p_pc_weight_lower_product)))))) -> (exists fs_u_pc_weight_lower_sum fs_v_pc_weight_lower_sum. ((((exists fs_h_pc_weight_lower_sum_body_start. fs_h_pc_weight_lower_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_weight_lower_sum)) /\ exists fs_q_pc_weight_lower_sum_body_start. fs_u_pc_weight_lower_sum = fs_q_pc_weight_lower_sum_body_start * S ((S (0)) * fs_v_pc_weight_lower_sum) + (0))) /\ ((((exists fs_h_pc_weight_lower_sum_body_terminal. fs_h_pc_weight_lower_sum_body_terminal + S (k) = S ((S (l)) * fs_v_pc_weight_lower_sum)) /\ exists fs_q_pc_weight_lower_sum_body_terminal. fs_u_pc_weight_lower_sum = fs_q_pc_weight_lower_sum_body_terminal * S ((S (l)) * fs_v_pc_weight_lower_sum) + (k))) /\ forall fs_i_pc_weight_lower_sum_body_steps. (exists fs_lt_pc_weight_lower_sum_body_steps_bound. fs_lt_pc_weight_lower_sum_body_steps_bound + S fs_i_pc_weight_lower_sum_body_steps = l) -> exists fs_a_pc_weight_lower_sum_body_steps fs_r_pc_weight_lower_sum_body_steps fs_s_pc_weight_lower_sum_body_steps. ((((exists fs_h_pc_weight_lower_sum_body_steps_summand. fs_h_pc_weight_lower_sum_body_steps_summand + S (fs_a_pc_weight_lower_sum_body_steps) = S ((S (fs_i_pc_weight_lower_sum_body_steps)) * f)) /\ exists fs_q_pc_weight_lower_sum_body_steps_summand. d = fs_q_pc_weight_lower_sum_body_steps_summand * S ((S (fs_i_pc_weight_lower_sum_body_steps)) * f) + (fs_a_pc_weight_lower_sum_body_steps))) /\ ((((exists fs_h_pc_weight_lower_sum_body_steps_partial. fs_h_pc_weight_lower_sum_body_steps_partial + S (fs_r_pc_weight_lower_sum_body_steps) = S ((S (fs_i_pc_weight_lower_sum_body_steps)) * fs_v_pc_weight_lower_sum)) /\ exists fs_q_pc_weight_lower_sum_body_steps_partial. fs_u_pc_weight_lower_sum = fs_q_pc_weight_lower_sum_body_steps_partial * S ((S (fs_i_pc_weight_lower_sum_body_steps)) * fs_v_pc_weight_lower_sum) + (fs_r_pc_weight_lower_sum_body_steps))) /\ ((((exists fs_h_pc_weight_lower_sum_body_steps_successor. fs_h_pc_weight_lower_sum_body_steps_successor + S (fs_s_pc_weight_lower_sum_body_steps) = S ((S (S fs_i_pc_weight_lower_sum_body_steps)) * fs_v_pc_weight_lower_sum)) /\ exists fs_q_pc_weight_lower_sum_body_steps_successor. fs_u_pc_weight_lower_sum = fs_q_pc_weight_lower_sum_body_steps_successor * S ((S (S fs_i_pc_weight_lower_sum_body_steps)) * fs_v_pc_weight_lower_sum) + (fs_s_pc_weight_lower_sum_body_steps))) /\ fs_s_pc_weight_lower_sum_body_steps = fs_r_pc_weight_lower_sum_body_steps + fs_a_pc_weight_lower_sum_body_steps)))))) -> (exists pa_b_pc_weight_lower_power pa_c_pc_weight_lower_power. ((forall pa_i_pc_weight_lower_power_repeat. (exists pa_lt_pc_weight_lower_power_repeat_bound. pa_lt_pc_weight_lower_power_repeat_bound + S pa_i_pc_weight_lower_power_repeat = k) -> (((exists pa_h_pc_weight_lower_power_repeat_decoded. pa_h_pc_weight_lower_power_repeat_decoded + S (B) = S ((S (pa_i_pc_weight_lower_power_repeat)) * pa_c_pc_weight_lower_power)) /\ exists pa_q_pc_weight_lower_power_repeat_decoded. pa_b_pc_weight_lower_power = pa_q_pc_weight_lower_power_repeat_decoded * S ((S (pa_i_pc_weight_lower_power_repeat)) * pa_c_pc_weight_lower_power) + (B)))) /\ (exists pa_u_pc_weight_lower_power_product pa_v_pc_weight_lower_power_product. ((((exists pa_h_pc_weight_lower_power_product_start. pa_h_pc_weight_lower_power_product_start + S (1) = S ((S (0)) * pa_v_pc_weight_lower_power_product)) /\ exists pa_q_pc_weight_lower_power_product_start. pa_u_pc_weight_lower_power_product = pa_q_pc_weight_lower_power_product_start * S ((S (0)) * pa_v_pc_weight_lower_power_product) + (1))) /\ ((((exists pa_h_pc_weight_lower_power_product_terminal. pa_h_pc_weight_lower_power_product_terminal + S (Q) = S ((S (k)) * pa_v_pc_weight_lower_power_product)) /\ exists pa_q_pc_weight_lower_power_product_terminal. pa_u_pc_weight_lower_power_product = pa_q_pc_weight_lower_power_product_terminal * S ((S (k)) * pa_v_pc_weight_lower_power_product) + (Q))) /\ forall pa_i_pc_weight_lower_power_product. (exists pa_lt_pc_weight_lower_power_product_bound. pa_lt_pc_weight_lower_power_product_bound + S pa_i_pc_weight_lower_power_product = k) -> exists pa_p_pc_weight_lower_power_product pa_r_pc_weight_lower_power_product pa_s_pc_weight_lower_power_product. ((((exists pa_h_pc_weight_lower_power_product_factor. pa_h_pc_weight_lower_power_product_factor + S (pa_p_pc_weight_lower_power_product) = S ((S (pa_i_pc_weight_lower_power_product)) * pa_c_pc_weight_lower_power)) /\ exists pa_q_pc_weight_lower_power_product_factor. pa_b_pc_weight_lower_power = pa_q_pc_weight_lower_power_product_factor * S ((S (pa_i_pc_weight_lower_power_product)) * pa_c_pc_weight_lower_power) + (pa_p_pc_weight_lower_power_product))) /\ ((((exists pa_h_pc_weight_lower_power_product_partial. pa_h_pc_weight_lower_power_product_partial + S (pa_r_pc_weight_lower_power_product) = S ((S (pa_i_pc_weight_lower_power_product)) * pa_v_pc_weight_lower_power_product)) /\ exists pa_q_pc_weight_lower_power_product_partial. pa_u_pc_weight_lower_power_product = pa_q_pc_weight_lower_power_product_partial * S ((S (pa_i_pc_weight_lower_power_product)) * pa_v_pc_weight_lower_power_product) + (pa_r_pc_weight_lower_power_product))) /\ ((((exists pa_h_pc_weight_lower_power_product_successor. pa_h_pc_weight_lower_power_product_successor + S (pa_s_pc_weight_lower_power_product) = S ((S (S pa_i_pc_weight_lower_power_product)) * pa_v_pc_weight_lower_power_product)) /\ exists pa_q_pc_weight_lower_power_product_successor. pa_u_pc_weight_lower_power_product = pa_q_pc_weight_lower_power_product_successor * S ((S (S pa_i_pc_weight_lower_power_product)) * pa_v_pc_weight_lower_power_product) + (pa_s_pc_weight_lower_power_product))) /\ pa_s_pc_weight_lower_power_product = pa_r_pc_weight_lower_power_product * pa_p_pc_weight_lower_power_product)))))))) -> (exists pc_le_weight_lower_result. pc_le_weight_lower_result + (Q) = (z))

Constructive proof overview

Generated structural guide

An actual bit-weighted finite product has the corresponding lower bound by a power of its actual bit sum.

The unchanged tactic script uses 13 declared prerequisites and contains 158 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_product_zero Stable theorem; checked-use authorized beta_sum_zero Stable theorem; checked-use authorized pow_zero Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized beta_product_succ_decompose Stable theorem; checked-use authorized beta_sum_succ_decompose Stable theorem; checked-use authorized pow_exists Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized pow_functional Stable theorem; checked-use authorized pow_successor_pair_mul Stable theorem; checked-use authorized mul_le_mul Alpha theorem; checked-use authorized le_trans Stable theorem; checked-use authorized le_mul_of_one_le_right Alpha theorem; checked-use authorized

Direct dependents

PC0020 primorial_cutoff_count_power_bound

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

158 script commands · 27 reading checkpoints · 12 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.

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–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro f
  5. L5
    intro B
02Induction on lL6–13

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

  1. L6
    induction l
  2. L7
    intro z
  3. L8
    intro k
  4. L9
    intro Q
  5. L10
    intro hw
  6. L11
    intro hz
  7. L12
    intro hk
  8. L13
    intro hQ
03Establish hz1L14–19

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

  1. L14
    have hz1 : z = 1
  2. L15
    specialize beta_product_zero b
  3. L16
    specialize beta_product_zero c
  4. L17
    specialize beta_product_zero z
  5. L18
    apply beta_product_zero
  6. L19
    exact hz
04Establish hk0L20–25

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

  1. L20
    have hk0 : k = 0
  2. L21
    specialize beta_sum_zero d
  3. L22
    specialize beta_sum_zero f
  4. L23
    specialize beta_sum_zero k
  5. L24
    apply beta_sum_zero
  6. L25
    exact hk
05Establish hQ1L26–35

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

  1. L26
    have hQ1 : Q = 1
  2. L27
    specialize pow_zero B
  3. L28
    specialize pow_zero k
  4. L29
    specialize pow_zero Q
  5. L30
    apply pow_zero
  6. L31
    exact hk0
  7. L32
    exact hQ
  8. L33
    rewrite hz1
  9. L34
    rewrite hQ1
  10. L35
    specialize le_refl 1
06Use earlier factsL36–36

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

  1. L36
    apply le_refl
07Fix variables and assumptionsL37–43

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

  1. L37
    intro z
  2. L38
    intro k
  3. L39
    intro Q
  4. L40
    intro hw
  5. L41
    intro hz
  6. L42
    intro hk
  7. L43
    intro hQ
08Establish hprodL44–50

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

  1. L44
    have hprod : ∃ a. ∃ w. BetaAt(b,c,l,a) ∧ (Product(b,c,l,w) ∧ z = w · a)Definitions: BetaAtProduct
  2. L45
    specialize beta_product_succ_decompose b
  3. L46
    specialize beta_product_succ_decompose c
  4. L47
    specialize beta_product_succ_decompose l
  5. L48
    specialize beta_product_succ_decompose z
  6. L49
    apply beta_product_succ_decompose
  7. L50
    exact hz
09Separate the logical casesL51–54

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

  1. L51
    cases hprod
  2. L52
    cases hprod_witness
  3. L53
    cases hprod_witness_witness
  4. L54
    cases hprod_witness_witness_right
10Establish hsumL55–61

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

  1. L55
    have hsum : ∃ e. ∃ K. BetaAt(d,f,l,e) ∧ (Sum(d,f,l,K) ∧ k = K + e)Definitions: BetaAtSum
  2. L56
    specialize beta_sum_succ_decompose d
  3. L57
    specialize beta_sum_succ_decompose f
  4. L58
    specialize beta_sum_succ_decompose l
  5. L59
    specialize beta_sum_succ_decompose k
  6. L60
    apply beta_sum_succ_decompose
  7. L61
    exact hk
11Separate the logical casesL62–65

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

  1. L62
    cases hsum
  2. L63
    cases hsum_witness
  3. L64
    cases hsum_witness_witness
  4. L65
    cases hsum_witness_witness_right
12Establish hpL66–69

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

  1. L66
    have hp : ∃ R. Pow(B,x3,R)Definitions: Pow
  2. L67
    specialize pow_exists B
  3. L68
    specialize pow_exists x3
  4. L69
    apply pow_exists
13Separate the logical casesL70–70

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

  1. L70
    cases hp
14Establish hpreL71–80

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

  1. L71
    have hpre : exists pc_le_weight_previous_bound. pc_le_weight_previous_bound + (x4) = (x1)
  2. L72
    specialize IH x1
  3. L73
    specialize IH x3
  4. L74
    specialize IH x4
  5. L75
    apply IH
  6. L76
    intro i
  7. L77
    intro a
  8. L78
    intro e
  9. L79
    intro hi
  10. L80
    intro ha
15Fix variables and assumptionsL81–81

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

  1. L81
    intro he
16Use earlier factsL82–91

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

  1. L82
    specialize hw i
  2. L83
    specialize hw a
  3. L84
    specialize hw e
  4. L85
    apply hw
  5. L86
    specialize le_succ (S i)
  6. L87
    specialize le_succ l
  7. L88
    apply le_succ
  8. L89
    exact hi
  9. L90
    exact ha
  10. L91
    exact he
17Use earlier factsL92–94

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

  1. L92
    exact hprod_witness_witness_right_left
  2. L93
    exact hsum_witness_witness_right_left
  3. L94
    exact hp_witness
18Establish hlastL95–103

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

  1. L95
    have hlast : (x2 = 0 /\ (exists pc_le_weight_last_zero. pc_le_weight_last_zero + (1) = (x))) \/ (x2 = 1 /\ (exists pc_le_weight_last_one. pc_le_weight_last_one + (B) = (x)))
  2. L96
    specialize hw l
  3. L97
    specialize hw x
  4. L98
    specialize hw x2
  5. L99
    apply hw
  6. L100
    specialize le_refl (S l)
  7. L101
    apply le_refl
  8. L102
    exact hprod_witness_witness_left
  9. L103
    exact hsum_witness_witness_left
19Separate the logical casesL104–105

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

  1. L104
    cases hlast
  2. L105
    cases hlast_left
20Establish hk0L106–114

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

  1. L106
    have hk0 : k = x3
  2. L107
    trans x3 + x2
  3. L108
    exact hsum_witness_witness_right_right
  4. L109
    rewrite hlast_left_left
  5. L110
    apply PA3
  6. L111
    rewrite hk0 at hQ
  7. L112
    rewrite hk0 at hQ
  8. L113
    rewrite hk0 at hQ
  9. L114
    rewrite hk0 at hQ
21Establish hQ0L115–124

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

  1. L115
    have hQ0 : Q = x4
  2. L116
    specialize pow_functional B
  3. L117
    specialize pow_functional x3
  4. L118
    specialize pow_functional Q
  5. L119
    specialize pow_functional x4
  6. L120
    apply pow_functional
  7. L121
    exact hQ
  8. L122
    exact hp_witness
  9. L123
    rewrite hprod_witness_witness_right_right
  10. L124
    rewrite hQ0
22Use earlier factsL125–133

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

  1. L125
    specialize le_trans x4
  2. L126
    specialize le_trans x1
  3. L127
    specialize le_trans (x1 * x)
  4. L128
    apply le_trans
  5. L129
    exact hpre
  6. L130
    specialize le_mul_of_one_le_right x1
  7. L131
    specialize le_mul_of_one_le_right x
  8. L132
    apply le_mul_of_one_le_right
  9. L133
    exact hlast_left_right
23Separate the logical casesL134–134

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

  1. L134
    cases hlast_right
24Establish hk1L135–139

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

  1. L135
    have hk1 : k = S x3
  2. L136
    trans x3 + x2
  3. L137
    exact hsum_witness_witness_right_right
  4. L138
    rewrite hlast_right_left
  5. L139
    simp
25Establish hQ1L140–149

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

  1. L140
    have hQ1 : Q = x4 * B
  2. L141
    specialize pow_successor_pair_mul B
  3. L142
    specialize pow_successor_pair_mul x3
  4. L143
    specialize pow_successor_pair_mul k
  5. L144
    specialize pow_successor_pair_mul x4
  6. L145
    specialize pow_successor_pair_mul Q
  7. L146
    apply pow_successor_pair_mul
  8. L147
    exact hk1
  9. L148
    exact hp_witness
  10. L149
    exact hQ
26Calculate and transport equalitiesL150–151

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

  1. L150
    rewrite hprod_witness_witness_right_right
  2. L151
    rewrite hQ1
27Use earlier factsL152–158

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

  1. L152
    specialize mul_le_mul x4
  2. L153
    specialize mul_le_mul x1
  3. L154
    specialize mul_le_mul B
  4. L155
    specialize mul_le_mul x
  5. L156
    apply mul_le_mul
  6. L157
    exact hpre
  7. L158
    exact hlast_right_right

Library-wide reading audit

Original exact command ledger · 158 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro f
  5. 0005intro B
  6. 0006induction l
  7. 0007intro z
  8. 0008intro k
  9. 0009intro Q
  10. 0010intro hw
  11. 0011intro hz
  12. 0012intro hk
  13. 0013intro hQ
  14. 0014have hz1 : z = 1
  15. 0015specialize beta_product_zero b
  16. 0016specialize beta_product_zero c
  17. 0017specialize beta_product_zero z
  18. 0018apply beta_product_zero
  19. 0019exact hz
  20. 0020have hk0 : k = 0
  21. 0021specialize beta_sum_zero d
  22. 0022specialize beta_sum_zero f
  23. 0023specialize beta_sum_zero k
  24. 0024apply beta_sum_zero
  25. 0025exact hk
  26. 0026have hQ1 : Q = 1
  27. 0027specialize pow_zero B
  28. 0028specialize pow_zero k
  29. 0029specialize pow_zero Q
  30. 0030apply pow_zero
  31. 0031exact hk0
  32. 0032exact hQ
  33. 0033rewrite hz1
  34. 0034rewrite hQ1
  35. 0035specialize le_refl 1
  36. 0036apply le_refl
  37. 0037intro z
  38. 0038intro k
  39. 0039intro Q
  40. 0040intro hw
  41. 0041intro hz
  42. 0042intro hk
  43. 0043intro hQ
  44. 0044have hprod : exists a w. (((exists fs_h_pc_weight_last_factor. fs_h_pc_weight_last_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_pc_weight_last_factor. b = fs_q_pc_weight_last_factor * S ((S (l)) * c) + (a))) /\ ((exists ff_u_pc_weight_previous_product ff_v_pc_weight_previous_product. ((((exists ff_h_pc_weight_previous_product_start. ff_h_pc_weight_previous_product_start + S (1) = S ((S (0)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_start. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_start * S ((S (0)) * ff_v_pc_weight_previous_product) + (1))) /\ ((((exists ff_h_pc_weight_previous_product_terminal. ff_h_pc_weight_previous_product_terminal + S (w) = S ((S (l)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_terminal. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_terminal * S ((S (l)) * ff_v_pc_weight_previous_product) + (w))) /\ forall ff_i_pc_weight_previous_product. (exists ff_lt_pc_weight_previous_product_bound. ff_lt_pc_weight_previous_product_bound + S ff_i_pc_weight_previous_product = l) -> exists ff_p_pc_weight_previous_product ff_r_pc_weight_previous_product ff_s_pc_weight_previous_product. ((((exists ff_h_pc_weight_previous_product_factor. ff_h_pc_weight_previous_product_factor + S (ff_p_pc_weight_previous_product) = S ((S (ff_i_pc_weight_previous_product)) * c)) /\ exists ff_q_pc_weight_previous_product_factor. b = ff_q_pc_weight_previous_product_factor * S ((S (ff_i_pc_weight_previous_product)) * c) + (ff_p_pc_weight_previous_product))) /\ ((((exists ff_h_pc_weight_previous_product_partial. ff_h_pc_weight_previous_product_partial + S (ff_r_pc_weight_previous_product) = S ((S (ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_partial. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_partial * S ((S (ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product) + (ff_r_pc_weight_previous_product))) /\ ((((exists ff_h_pc_weight_previous_product_successor. ff_h_pc_weight_previous_product_successor + S (ff_s_pc_weight_previous_product) = S ((S (S ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_successor. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_successor * S ((S (S ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product) + (ff_s_pc_weight_previous_product))) /\ ff_s_pc_weight_previous_product = ff_r_pc_weight_previous_product * ff_p_pc_weight_previous_product)))))) /\ z = w * a)
  45. 0045specialize beta_product_succ_decompose b
  46. 0046specialize beta_product_succ_decompose c
  47. 0047specialize beta_product_succ_decompose l
  48. 0048specialize beta_product_succ_decompose z
  49. 0049apply beta_product_succ_decompose
  50. 0050exact hz
  51. 0051cases hprod
  52. 0052cases hprod_witness
  53. 0053cases hprod_witness_witness
  54. 0054cases hprod_witness_witness_right
  55. 0055have hsum : exists e K. (((exists fs_h_pc_weight_last_bit. fs_h_pc_weight_last_bit + S (e) = S ((S (l)) * f)) /\ exists fs_q_pc_weight_last_bit. d = fs_q_pc_weight_last_bit * S ((S (l)) * f) + (e))) /\ ((exists fs_u_pc_weight_previous_sum fs_v_pc_weight_previous_sum. ((((exists fs_h_pc_weight_previous_sum_body_start. fs_h_pc_weight_previous_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_start. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_start * S ((S (0)) * fs_v_pc_weight_previous_sum) + (0))) /\ ((((exists fs_h_pc_weight_previous_sum_body_terminal. fs_h_pc_weight_previous_sum_body_terminal + S (K) = S ((S (l)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_terminal. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_terminal * S ((S (l)) * fs_v_pc_weight_previous_sum) + (K))) /\ forall fs_i_pc_weight_previous_sum_body_steps. (exists fs_lt_pc_weight_previous_sum_body_steps_bound. fs_lt_pc_weight_previous_sum_body_steps_bound + S fs_i_pc_weight_previous_sum_body_steps = l) -> exists fs_a_pc_weight_previous_sum_body_steps fs_r_pc_weight_previous_sum_body_steps fs_s_pc_weight_previous_sum_body_steps. ((((exists fs_h_pc_weight_previous_sum_body_steps_summand. fs_h_pc_weight_previous_sum_body_steps_summand + S (fs_a_pc_weight_previous_sum_body_steps) = S ((S (fs_i_pc_weight_previous_sum_body_steps)) * f)) /\ exists fs_q_pc_weight_previous_sum_body_steps_summand. d = fs_q_pc_weight_previous_sum_body_steps_summand * S ((S (fs_i_pc_weight_previous_sum_body_steps)) * f) + (fs_a_pc_weight_previous_sum_body_steps))) /\ ((((exists fs_h_pc_weight_previous_sum_body_steps_partial. fs_h_pc_weight_previous_sum_body_steps_partial + S (fs_r_pc_weight_previous_sum_body_steps) = S ((S (fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_steps_partial. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_steps_partial * S ((S (fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum) + (fs_r_pc_weight_previous_sum_body_steps))) /\ ((((exists fs_h_pc_weight_previous_sum_body_steps_successor. fs_h_pc_weight_previous_sum_body_steps_successor + S (fs_s_pc_weight_previous_sum_body_steps) = S ((S (S fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_steps_successor. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_steps_successor * S ((S (S fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum) + (fs_s_pc_weight_previous_sum_body_steps))) /\ fs_s_pc_weight_previous_sum_body_steps = fs_r_pc_weight_previous_sum_body_steps + fs_a_pc_weight_previous_sum_body_steps)))))) /\ k = K + e)
  56. 0056specialize beta_sum_succ_decompose d
  57. 0057specialize beta_sum_succ_decompose f
  58. 0058specialize beta_sum_succ_decompose l
  59. 0059specialize beta_sum_succ_decompose k
  60. 0060apply beta_sum_succ_decompose
  61. 0061exact hk
  62. 0062cases hsum
  63. 0063cases hsum_witness
  64. 0064cases hsum_witness_witness
  65. 0065cases hsum_witness_witness_right
  66. 0066have hp : exists R. exists pa_b_pc_weight_previous_power pa_c_pc_weight_previous_power. ((forall pa_i_pc_weight_previous_power_repeat. (exists pa_lt_pc_weight_previous_power_repeat_bound. pa_lt_pc_weight_previous_power_repeat_bound + S pa_i_pc_weight_previous_power_repeat = x3) -> (((exists pa_h_pc_weight_previous_power_repeat_decoded. pa_h_pc_weight_previous_power_repeat_decoded + S (B) = S ((S (pa_i_pc_weight_previous_power_repeat)) * pa_c_pc_weight_previous_power)) /\ exists pa_q_pc_weight_previous_power_repeat_decoded. pa_b_pc_weight_previous_power = pa_q_pc_weight_previous_power_repeat_decoded * S ((S (pa_i_pc_weight_previous_power_repeat)) * pa_c_pc_weight_previous_power) + (B)))) /\ (exists pa_u_pc_weight_previous_power_product pa_v_pc_weight_previous_power_product. ((((exists pa_h_pc_weight_previous_power_product_start. pa_h_pc_weight_previous_power_product_start + S (1) = S ((S (0)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_start. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_start * S ((S (0)) * pa_v_pc_weight_previous_power_product) + (1))) /\ ((((exists pa_h_pc_weight_previous_power_product_terminal. pa_h_pc_weight_previous_power_product_terminal + S (R) = S ((S (x3)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_terminal. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_terminal * S ((S (x3)) * pa_v_pc_weight_previous_power_product) + (R))) /\ forall pa_i_pc_weight_previous_power_product. (exists pa_lt_pc_weight_previous_power_product_bound. pa_lt_pc_weight_previous_power_product_bound + S pa_i_pc_weight_previous_power_product = x3) -> exists pa_p_pc_weight_previous_power_product pa_r_pc_weight_previous_power_product pa_s_pc_weight_previous_power_product. ((((exists pa_h_pc_weight_previous_power_product_factor. pa_h_pc_weight_previous_power_product_factor + S (pa_p_pc_weight_previous_power_product) = S ((S (pa_i_pc_weight_previous_power_product)) * pa_c_pc_weight_previous_power)) /\ exists pa_q_pc_weight_previous_power_product_factor. pa_b_pc_weight_previous_power = pa_q_pc_weight_previous_power_product_factor * S ((S (pa_i_pc_weight_previous_power_product)) * pa_c_pc_weight_previous_power) + (pa_p_pc_weight_previous_power_product))) /\ ((((exists pa_h_pc_weight_previous_power_product_partial. pa_h_pc_weight_previous_power_product_partial + S (pa_r_pc_weight_previous_power_product) = S ((S (pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_partial. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_partial * S ((S (pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product) + (pa_r_pc_weight_previous_power_product))) /\ ((((exists pa_h_pc_weight_previous_power_product_successor. pa_h_pc_weight_previous_power_product_successor + S (pa_s_pc_weight_previous_power_product) = S ((S (S pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_successor. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_successor * S ((S (S pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product) + (pa_s_pc_weight_previous_power_product))) /\ pa_s_pc_weight_previous_power_product = pa_r_pc_weight_previous_power_product * pa_p_pc_weight_previous_power_product)))))))
  67. 0067specialize pow_exists B
  68. 0068specialize pow_exists x3
  69. 0069apply pow_exists
  70. 0070cases hp
  71. 0071have hpre : exists pc_le_weight_previous_bound. pc_le_weight_previous_bound + (x4) = (x1)
  72. 0072specialize IH x1
  73. 0073specialize IH x3
  74. 0074specialize IH x4
  75. 0075apply IH
  76. 0076intro i
  77. 0077intro a
  78. 0078intro e
  79. 0079intro hi
  80. 0080intro ha
  81. 0081intro he
  82. 0082specialize hw i
  83. 0083specialize hw a
  84. 0084specialize hw e
  85. 0085apply hw
  86. 0086specialize le_succ (S i)
  87. 0087specialize le_succ l
  88. 0088apply le_succ
  89. 0089exact hi
  90. 0090exact ha
  91. 0091exact he
  92. 0092exact hprod_witness_witness_right_left
  93. 0093exact hsum_witness_witness_right_left
  94. 0094exact hp_witness
  95. 0095have hlast : (x2 = 0 /\ (exists pc_le_weight_last_zero. pc_le_weight_last_zero + (1) = (x))) \/ (x2 = 1 /\ (exists pc_le_weight_last_one. pc_le_weight_last_one + (B) = (x)))
  96. 0096specialize hw l
  97. 0097specialize hw x
  98. 0098specialize hw x2
  99. 0099apply hw
  100. 0100specialize le_refl (S l)
  101. 0101apply le_refl
  102. 0102exact hprod_witness_witness_left
  103. 0103exact hsum_witness_witness_left
  104. 0104cases hlast
  105. 0105cases hlast_left
  106. 0106have hk0 : k = x3
  107. 0107trans x3 + x2
  108. 0108exact hsum_witness_witness_right_right
  109. 0109rewrite hlast_left_left
  110. 0110apply PA3
  111. 0111rewrite hk0 at hQ
  112. 0112rewrite hk0 at hQ
  113. 0113rewrite hk0 at hQ
  114. 0114rewrite hk0 at hQ
  115. 0115have hQ0 : Q = x4
  116. 0116specialize pow_functional B
  117. 0117specialize pow_functional x3
  118. 0118specialize pow_functional Q
  119. 0119specialize pow_functional x4
  120. 0120apply pow_functional
  121. 0121exact hQ
  122. 0122exact hp_witness
  123. 0123rewrite hprod_witness_witness_right_right
  124. 0124rewrite hQ0
  125. 0125specialize le_trans x4
  126. 0126specialize le_trans x1
  127. 0127specialize le_trans (x1 * x)
  128. 0128apply le_trans
  129. 0129exact hpre
  130. 0130specialize le_mul_of_one_le_right x1
  131. 0131specialize le_mul_of_one_le_right x
  132. 0132apply le_mul_of_one_le_right
  133. 0133exact hlast_left_right
  134. 0134cases hlast_right
  135. 0135have hk1 : k = S x3
  136. 0136trans x3 + x2
  137. 0137exact hsum_witness_witness_right_right
  138. 0138rewrite hlast_right_left
  139. 0139simp
  140. 0140have hQ1 : Q = x4 * B
  141. 0141specialize pow_successor_pair_mul B
  142. 0142specialize pow_successor_pair_mul x3
  143. 0143specialize pow_successor_pair_mul k
  144. 0144specialize pow_successor_pair_mul x4
  145. 0145specialize pow_successor_pair_mul Q
  146. 0146apply pow_successor_pair_mul
  147. 0147exact hk1
  148. 0148exact hp_witness
  149. 0149exact hQ
  150. 0150rewrite hprod_witness_witness_right_right
  151. 0151rewrite hQ1
  152. 0152specialize mul_le_mul x4
  153. 0153specialize mul_le_mul x1
  154. 0154specialize mul_le_mul B
  155. 0155specialize mul_le_mul x
  156. 0156apply mul_le_mul
  157. 0157exact hpre
  158. 0158exact hlast_right_right