BT00SL

pow_successor_compose_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

One shared power-totality premise constructs a successor power.

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 PA statement

forall a e r n. (forall bpt_a_successor bpt_e_successor. exists bpt_x_successor. (exists ff_b_bpt_value_successor ff_c_bpt_value_successor. ((forall ff_i_bpt_value_successor_repeat. (exists ff_lt_bpt_value_successor_repeat_bound. ff_lt_bpt_value_successor_repeat_bound + S ff_i_bpt_value_successor_repeat = bpt_e_successor) -> (((exists ff_h_bpt_value_successor_repeat_decoded. ff_h_bpt_value_successor_repeat_decoded + S (bpt_a_successor) = S ((S (ff_i_bpt_value_successor_repeat)) * ff_c_bpt_value_successor)) /\ exists ff_q_bpt_value_successor_repeat_decoded. ff_b_bpt_value_successor = ff_q_bpt_value_successor_repeat_decoded * S ((S (ff_i_bpt_value_successor_repeat)) * ff_c_bpt_value_successor) + (bpt_a_successor)))) /\ (exists ff_u_bpt_value_successor_product ff_v_bpt_value_successor_product. ((((exists ff_h_bpt_value_successor_product_start. ff_h_bpt_value_successor_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_start. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_start * S ((S (0)) * ff_v_bpt_value_successor_product) + (1))) /\ ((((exists ff_h_bpt_value_successor_product_terminal. ff_h_bpt_value_successor_product_terminal + S (bpt_x_successor) = S ((S (bpt_e_successor)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_terminal. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_terminal * S ((S (bpt_e_successor)) * ff_v_bpt_value_successor_product) + (bpt_x_successor))) /\ forall ff_i_bpt_value_successor_product. (exists ff_lt_bpt_value_successor_product_bound. ff_lt_bpt_value_successor_product_bound + S ff_i_bpt_value_successor_product = bpt_e_successor) -> exists ff_p_bpt_value_successor_product ff_r_bpt_value_successor_product ff_s_bpt_value_successor_product. ((((exists ff_h_bpt_value_successor_product_factor. ff_h_bpt_value_successor_product_factor + S (ff_p_bpt_value_successor_product) = S ((S (ff_i_bpt_value_successor_product)) * ff_c_bpt_value_successor)) /\ exists ff_q_bpt_value_successor_product_factor. ff_b_bpt_value_successor = ff_q_bpt_value_successor_product_factor * S ((S (ff_i_bpt_value_successor_product)) * ff_c_bpt_value_successor) + (ff_p_bpt_value_successor_product))) /\ ((((exists ff_h_bpt_value_successor_product_partial. ff_h_bpt_value_successor_product_partial + S (ff_r_bpt_value_successor_product) = S ((S (ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_partial. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_partial * S ((S (ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product) + (ff_r_bpt_value_successor_product))) /\ ((((exists ff_h_bpt_value_successor_product_successor. ff_h_bpt_value_successor_product_successor + S (ff_s_bpt_value_successor_product) = S ((S (S ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product)) /\ exists ff_q_bpt_value_successor_product_successor. ff_u_bpt_value_successor_product = ff_q_bpt_value_successor_product_successor * S ((S (S ff_i_bpt_value_successor_product)) * ff_v_bpt_value_successor_product) + (ff_s_bpt_value_successor_product))) /\ ff_s_bpt_value_successor_product = ff_r_bpt_value_successor_product * ff_p_bpt_value_successor_product))))))))) -> (exists ff_b_bpt_predecessor ff_c_bpt_predecessor. ((forall ff_i_bpt_predecessor_repeat. (exists ff_lt_bpt_predecessor_repeat_bound. ff_lt_bpt_predecessor_repeat_bound + S ff_i_bpt_predecessor_repeat = e) -> (((exists ff_h_bpt_predecessor_repeat_decoded. ff_h_bpt_predecessor_repeat_decoded + S (a) = S ((S (ff_i_bpt_predecessor_repeat)) * ff_c_bpt_predecessor)) /\ exists ff_q_bpt_predecessor_repeat_decoded. ff_b_bpt_predecessor = ff_q_bpt_predecessor_repeat_decoded * S ((S (ff_i_bpt_predecessor_repeat)) * ff_c_bpt_predecessor) + (a)))) /\ (exists ff_u_bpt_predecessor_product ff_v_bpt_predecessor_product. ((((exists ff_h_bpt_predecessor_product_start. ff_h_bpt_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_start. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_start * S ((S (0)) * ff_v_bpt_predecessor_product) + (1))) /\ ((((exists ff_h_bpt_predecessor_product_terminal. ff_h_bpt_predecessor_product_terminal + S (r) = S ((S (e)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_terminal. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_terminal * S ((S (e)) * ff_v_bpt_predecessor_product) + (r))) /\ forall ff_i_bpt_predecessor_product. (exists ff_lt_bpt_predecessor_product_bound. ff_lt_bpt_predecessor_product_bound + S ff_i_bpt_predecessor_product = e) -> exists ff_p_bpt_predecessor_product ff_r_bpt_predecessor_product ff_s_bpt_predecessor_product. ((((exists ff_h_bpt_predecessor_product_factor. ff_h_bpt_predecessor_product_factor + S (ff_p_bpt_predecessor_product) = S ((S (ff_i_bpt_predecessor_product)) * ff_c_bpt_predecessor)) /\ exists ff_q_bpt_predecessor_product_factor. ff_b_bpt_predecessor = ff_q_bpt_predecessor_product_factor * S ((S (ff_i_bpt_predecessor_product)) * ff_c_bpt_predecessor) + (ff_p_bpt_predecessor_product))) /\ ((((exists ff_h_bpt_predecessor_product_partial. ff_h_bpt_predecessor_product_partial + S (ff_r_bpt_predecessor_product) = S ((S (ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_partial. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_partial * S ((S (ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product) + (ff_r_bpt_predecessor_product))) /\ ((((exists ff_h_bpt_predecessor_product_successor. ff_h_bpt_predecessor_product_successor + S (ff_s_bpt_predecessor_product) = S ((S (S ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product)) /\ exists ff_q_bpt_predecessor_product_successor. ff_u_bpt_predecessor_product = ff_q_bpt_predecessor_product_successor * S ((S (S ff_i_bpt_predecessor_product)) * ff_v_bpt_predecessor_product) + (ff_s_bpt_predecessor_product))) /\ ff_s_bpt_predecessor_product = ff_r_bpt_predecessor_product * ff_p_bpt_predecessor_product)))))))) -> n = r * a -> (exists pa_b_bpt_successor pa_c_bpt_successor. ((forall pa_i_bpt_successor_repeat. (exists pa_lt_bpt_successor_repeat_bound. pa_lt_bpt_successor_repeat_bound + S pa_i_bpt_successor_repeat = S e) -> (((exists pa_h_bpt_successor_repeat_decoded. pa_h_bpt_successor_repeat_decoded + S (a) = S ((S (pa_i_bpt_successor_repeat)) * pa_c_bpt_successor)) /\ exists pa_q_bpt_successor_repeat_decoded. pa_b_bpt_successor = pa_q_bpt_successor_repeat_decoded * S ((S (pa_i_bpt_successor_repeat)) * pa_c_bpt_successor) + (a)))) /\ (exists pa_u_bpt_successor_product pa_v_bpt_successor_product. ((((exists pa_h_bpt_successor_product_start. pa_h_bpt_successor_product_start + S (1) = S ((S (0)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_start. pa_u_bpt_successor_product = pa_q_bpt_successor_product_start * S ((S (0)) * pa_v_bpt_successor_product) + (1))) /\ ((((exists pa_h_bpt_successor_product_terminal. pa_h_bpt_successor_product_terminal + S (n) = S ((S (S e)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_terminal. pa_u_bpt_successor_product = pa_q_bpt_successor_product_terminal * S ((S (S e)) * pa_v_bpt_successor_product) + (n))) /\ forall pa_i_bpt_successor_product. (exists pa_lt_bpt_successor_product_bound. pa_lt_bpt_successor_product_bound + S pa_i_bpt_successor_product = S e) -> exists pa_p_bpt_successor_product pa_r_bpt_successor_product pa_s_bpt_successor_product. ((((exists pa_h_bpt_successor_product_factor. pa_h_bpt_successor_product_factor + S (pa_p_bpt_successor_product) = S ((S (pa_i_bpt_successor_product)) * pa_c_bpt_successor)) /\ exists pa_q_bpt_successor_product_factor. pa_b_bpt_successor = pa_q_bpt_successor_product_factor * S ((S (pa_i_bpt_successor_product)) * pa_c_bpt_successor) + (pa_p_bpt_successor_product))) /\ ((((exists pa_h_bpt_successor_product_partial. pa_h_bpt_successor_product_partial + S (pa_r_bpt_successor_product) = S ((S (pa_i_bpt_successor_product)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_partial. pa_u_bpt_successor_product = pa_q_bpt_successor_product_partial * S ((S (pa_i_bpt_successor_product)) * pa_v_bpt_successor_product) + (pa_r_bpt_successor_product))) /\ ((((exists pa_h_bpt_successor_product_successor. pa_h_bpt_successor_product_successor + S (pa_s_bpt_successor_product) = S ((S (S pa_i_bpt_successor_product)) * pa_v_bpt_successor_product)) /\ exists pa_q_bpt_successor_product_successor. pa_u_bpt_successor_product = pa_q_bpt_successor_product_successor * S ((S (S pa_i_bpt_successor_product)) * pa_v_bpt_successor_product) + (pa_s_bpt_successor_product))) /\ pa_s_bpt_successor_product = pa_r_bpt_successor_product * pa_p_bpt_successor_product))))))))

Structural proof guide

One shared power-totality premise constructs a successor power.

Direct prerequisites: pow_successor_pair_mul. The authored body proceeds by case analysis (1), intermediate claims (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT0095 pow_successor_pair_mul

Direct dependents

BT00SO pow_two_seed_bundle_from_total BT00W4 pow_three_five_le_pow_four_four_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

30 script commands · 5 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.

Named ingredients (1)
pow successor pair mul

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

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

  1. L1
    intro a
  2. L2
    intro e
  3. L3
    intro r
  4. L4
    intro n
  5. L5
    intro htotal
  6. L6
    intro hprevious
  7. L7
    intro hn
02Establish hsuccessorL8–11

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

  1. L8
    have hsuccessor : ∃ x. Pow(a,S e,x)Definitions: Pow
  2. L9
    specialize htotal a
  3. L10
    specialize htotal (S e)
  4. L11
    exact htotal
03Separate the logical casesL12–12

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

  1. L12
    cases hsuccessor
04Establish hxL13–22

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

  1. L13
    have hx : x = r * a
  2. L14
    specialize pow_successor_pair_mul a
  3. L15
    specialize pow_successor_pair_mul e
  4. L16
    specialize pow_successor_pair_mul (S e)
  5. L17
    specialize pow_successor_pair_mul r
  6. L18
    specialize pow_successor_pair_mul x
  7. L19
    apply pow_successor_pair_mul
  8. L20
    refl
  9. L21
    exact hprevious
  10. L22
    exact hsuccessor_witness
05Establish hxnL23–30

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

  1. L23
    have hxn : x = n
  2. L24
    trans r * a
  3. L25
    exact hx
  4. L26
    symm
  5. L27
    exact hn
  6. L28
    rewrite <- hxn
  7. L29
    rewrite <- hxn
  8. L30
    exact hsuccessor_witness

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003intro r
  4. 0004intro n
  5. 0005intro htotal
  6. 0006intro hprevious
  7. 0007intro hn
  8. 0008have hsuccessor : exists x. (exists pa_b_bpt_successor_witness pa_c_bpt_successor_witness. ((forall pa_i_bpt_successor_witness_repeat. (exists pa_lt_bpt_successor_witness_repeat_bound. pa_lt_bpt_successor_witness_repeat_bound + S pa_i_bpt_successor_witness_repeat = S e) -> (((exists pa_h_bpt_successor_witness_repeat_decoded. pa_h_bpt_successor_witness_repeat_decoded + S (a) = S ((S (pa_i_bpt_successor_witness_repeat)) * pa_c_bpt_successor_witness)) /\ exists pa_q_bpt_successor_witness_repeat_decoded. pa_b_bpt_successor_witness = pa_q_bpt_successor_witness_repeat_decoded * S ((S (pa_i_bpt_successor_witness_repeat)) * pa_c_bpt_successor_witness) + (a)))) /\ (exists pa_u_bpt_successor_witness_product pa_v_bpt_successor_witness_product. ((((exists pa_h_bpt_successor_witness_product_start. pa_h_bpt_successor_witness_product_start + S (1) = S ((S (0)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_start. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_start * S ((S (0)) * pa_v_bpt_successor_witness_product) + (1))) /\ ((((exists pa_h_bpt_successor_witness_product_terminal. pa_h_bpt_successor_witness_product_terminal + S (x) = S ((S (S e)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_terminal. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_terminal * S ((S (S e)) * pa_v_bpt_successor_witness_product) + (x))) /\ forall pa_i_bpt_successor_witness_product. (exists pa_lt_bpt_successor_witness_product_bound. pa_lt_bpt_successor_witness_product_bound + S pa_i_bpt_successor_witness_product = S e) -> exists pa_p_bpt_successor_witness_product pa_r_bpt_successor_witness_product pa_s_bpt_successor_witness_product. ((((exists pa_h_bpt_successor_witness_product_factor. pa_h_bpt_successor_witness_product_factor + S (pa_p_bpt_successor_witness_product) = S ((S (pa_i_bpt_successor_witness_product)) * pa_c_bpt_successor_witness)) /\ exists pa_q_bpt_successor_witness_product_factor. pa_b_bpt_successor_witness = pa_q_bpt_successor_witness_product_factor * S ((S (pa_i_bpt_successor_witness_product)) * pa_c_bpt_successor_witness) + (pa_p_bpt_successor_witness_product))) /\ ((((exists pa_h_bpt_successor_witness_product_partial. pa_h_bpt_successor_witness_product_partial + S (pa_r_bpt_successor_witness_product) = S ((S (pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_partial. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_partial * S ((S (pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product) + (pa_r_bpt_successor_witness_product))) /\ ((((exists pa_h_bpt_successor_witness_product_successor. pa_h_bpt_successor_witness_product_successor + S (pa_s_bpt_successor_witness_product) = S ((S (S pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product)) /\ exists pa_q_bpt_successor_witness_product_successor. pa_u_bpt_successor_witness_product = pa_q_bpt_successor_witness_product_successor * S ((S (S pa_i_bpt_successor_witness_product)) * pa_v_bpt_successor_witness_product) + (pa_s_bpt_successor_witness_product))) /\ pa_s_bpt_successor_witness_product = pa_r_bpt_successor_witness_product * pa_p_bpt_successor_witness_product))))))))
  9. 0009specialize htotal a
  10. 0010specialize htotal (S e)
  11. 0011exact htotal
  12. 0012cases hsuccessor
  13. 0013have hx : x = r * a
  14. 0014specialize pow_successor_pair_mul a
  15. 0015specialize pow_successor_pair_mul e
  16. 0016specialize pow_successor_pair_mul (S e)
  17. 0017specialize pow_successor_pair_mul r
  18. 0018specialize pow_successor_pair_mul x
  19. 0019apply pow_successor_pair_mul
  20. 0020refl
  21. 0021exact hprevious
  22. 0022exact hsuccessor_witness
  23. 0023have hxn : x = n
  24. 0024trans r * a
  25. 0025exact hx
  26. 0026symm
  27. 0027exact hn
  28. 0028rewrite <- hxn
  29. 0029rewrite <- hxn
  30. 0030exact hsuccessor_witness