BT00S5

pow_successor_compose

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

A checked predecessor power composes with one multiplication step.

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. (exists ff_b_bpb_predecessor ff_c_bpb_predecessor. ((forall ff_i_bpb_predecessor_repeat. (exists ff_lt_bpb_predecessor_repeat_bound. ff_lt_bpb_predecessor_repeat_bound + S ff_i_bpb_predecessor_repeat = e) -> (((exists ff_h_bpb_predecessor_repeat_decoded. ff_h_bpb_predecessor_repeat_decoded + S (a) = S ((S (ff_i_bpb_predecessor_repeat)) * ff_c_bpb_predecessor)) /\ exists ff_q_bpb_predecessor_repeat_decoded. ff_b_bpb_predecessor = ff_q_bpb_predecessor_repeat_decoded * S ((S (ff_i_bpb_predecessor_repeat)) * ff_c_bpb_predecessor) + (a)))) /\ (exists ff_u_bpb_predecessor_product ff_v_bpb_predecessor_product. ((((exists ff_h_bpb_predecessor_product_start. ff_h_bpb_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_start. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_start * S ((S (0)) * ff_v_bpb_predecessor_product) + (1))) /\ ((((exists ff_h_bpb_predecessor_product_terminal. ff_h_bpb_predecessor_product_terminal + S (r) = S ((S (e)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_terminal. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_terminal * S ((S (e)) * ff_v_bpb_predecessor_product) + (r))) /\ forall ff_i_bpb_predecessor_product. (exists ff_lt_bpb_predecessor_product_bound. ff_lt_bpb_predecessor_product_bound + S ff_i_bpb_predecessor_product = e) -> exists ff_p_bpb_predecessor_product ff_r_bpb_predecessor_product ff_s_bpb_predecessor_product. ((((exists ff_h_bpb_predecessor_product_factor. ff_h_bpb_predecessor_product_factor + S (ff_p_bpb_predecessor_product) = S ((S (ff_i_bpb_predecessor_product)) * ff_c_bpb_predecessor)) /\ exists ff_q_bpb_predecessor_product_factor. ff_b_bpb_predecessor = ff_q_bpb_predecessor_product_factor * S ((S (ff_i_bpb_predecessor_product)) * ff_c_bpb_predecessor) + (ff_p_bpb_predecessor_product))) /\ ((((exists ff_h_bpb_predecessor_product_partial. ff_h_bpb_predecessor_product_partial + S (ff_r_bpb_predecessor_product) = S ((S (ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_partial. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_partial * S ((S (ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product) + (ff_r_bpb_predecessor_product))) /\ ((((exists ff_h_bpb_predecessor_product_successor. ff_h_bpb_predecessor_product_successor + S (ff_s_bpb_predecessor_product) = S ((S (S ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product)) /\ exists ff_q_bpb_predecessor_product_successor. ff_u_bpb_predecessor_product = ff_q_bpb_predecessor_product_successor * S ((S (S ff_i_bpb_predecessor_product)) * ff_v_bpb_predecessor_product) + (ff_s_bpb_predecessor_product))) /\ ff_s_bpb_predecessor_product = ff_r_bpb_predecessor_product * ff_p_bpb_predecessor_product)))))))) -> n = r * a -> (exists pa_b_bpb_successor pa_c_bpb_successor. ((forall pa_i_bpb_successor_repeat. (exists pa_lt_bpb_successor_repeat_bound. pa_lt_bpb_successor_repeat_bound + S pa_i_bpb_successor_repeat = S e) -> (((exists pa_h_bpb_successor_repeat_decoded. pa_h_bpb_successor_repeat_decoded + S (a) = S ((S (pa_i_bpb_successor_repeat)) * pa_c_bpb_successor)) /\ exists pa_q_bpb_successor_repeat_decoded. pa_b_bpb_successor = pa_q_bpb_successor_repeat_decoded * S ((S (pa_i_bpb_successor_repeat)) * pa_c_bpb_successor) + (a)))) /\ (exists pa_u_bpb_successor_product pa_v_bpb_successor_product. ((((exists pa_h_bpb_successor_product_start. pa_h_bpb_successor_product_start + S (1) = S ((S (0)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_start. pa_u_bpb_successor_product = pa_q_bpb_successor_product_start * S ((S (0)) * pa_v_bpb_successor_product) + (1))) /\ ((((exists pa_h_bpb_successor_product_terminal. pa_h_bpb_successor_product_terminal + S (n) = S ((S (S e)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_terminal. pa_u_bpb_successor_product = pa_q_bpb_successor_product_terminal * S ((S (S e)) * pa_v_bpb_successor_product) + (n))) /\ forall pa_i_bpb_successor_product. (exists pa_lt_bpb_successor_product_bound. pa_lt_bpb_successor_product_bound + S pa_i_bpb_successor_product = S e) -> exists pa_p_bpb_successor_product pa_r_bpb_successor_product pa_s_bpb_successor_product. ((((exists pa_h_bpb_successor_product_factor. pa_h_bpb_successor_product_factor + S (pa_p_bpb_successor_product) = S ((S (pa_i_bpb_successor_product)) * pa_c_bpb_successor)) /\ exists pa_q_bpb_successor_product_factor. pa_b_bpb_successor = pa_q_bpb_successor_product_factor * S ((S (pa_i_bpb_successor_product)) * pa_c_bpb_successor) + (pa_p_bpb_successor_product))) /\ ((((exists pa_h_bpb_successor_product_partial. pa_h_bpb_successor_product_partial + S (pa_r_bpb_successor_product) = S ((S (pa_i_bpb_successor_product)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_partial. pa_u_bpb_successor_product = pa_q_bpb_successor_product_partial * S ((S (pa_i_bpb_successor_product)) * pa_v_bpb_successor_product) + (pa_r_bpb_successor_product))) /\ ((((exists pa_h_bpb_successor_product_successor. pa_h_bpb_successor_product_successor + S (pa_s_bpb_successor_product) = S ((S (S pa_i_bpb_successor_product)) * pa_v_bpb_successor_product)) /\ exists pa_q_bpb_successor_product_successor. pa_u_bpb_successor_product = pa_q_bpb_successor_product_successor * S ((S (S pa_i_bpb_successor_product)) * pa_v_bpb_successor_product) + (pa_s_bpb_successor_product))) /\ pa_s_bpb_successor_product = pa_r_bpb_successor_product * pa_p_bpb_successor_product))))))))

Structural proof guide

A checked predecessor power composes with one multiplication step.

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

Proof neighborhood

Direct dependencies

BT0080 pow_exists BT0095 pow_successor_pair_mul

Direct dependents

BT00VP central_binom_odd_middle_le_four_pow

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

29 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 (2)
pow existspow 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–6

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 hprevious
  6. L6
    intro hn
02Establish hsuccessorL7–10

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

  1. L7
    have hsuccessor : ∃ x. Pow(a,S e,x)Definitions: Pow
  2. L8
    specialize pow_exists a
  3. L9
    specialize pow_exists (S e)
  4. L10
    exact pow_exists
03Separate the logical casesL11–11

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

  1. L11
    cases hsuccessor
04Establish hxL12–21

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

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

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

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

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003intro r
  4. 0004intro n
  5. 0005intro hprevious
  6. 0006intro hn
  7. 0007have hsuccessor : exists x. (exists pa_b_bpb_successor_witness pa_c_bpb_successor_witness. ((forall pa_i_bpb_successor_witness_repeat. (exists pa_lt_bpb_successor_witness_repeat_bound. pa_lt_bpb_successor_witness_repeat_bound + S pa_i_bpb_successor_witness_repeat = S e) -> (((exists pa_h_bpb_successor_witness_repeat_decoded. pa_h_bpb_successor_witness_repeat_decoded + S (a) = S ((S (pa_i_bpb_successor_witness_repeat)) * pa_c_bpb_successor_witness)) /\ exists pa_q_bpb_successor_witness_repeat_decoded. pa_b_bpb_successor_witness = pa_q_bpb_successor_witness_repeat_decoded * S ((S (pa_i_bpb_successor_witness_repeat)) * pa_c_bpb_successor_witness) + (a)))) /\ (exists pa_u_bpb_successor_witness_product pa_v_bpb_successor_witness_product. ((((exists pa_h_bpb_successor_witness_product_start. pa_h_bpb_successor_witness_product_start + S (1) = S ((S (0)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_start. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_start * S ((S (0)) * pa_v_bpb_successor_witness_product) + (1))) /\ ((((exists pa_h_bpb_successor_witness_product_terminal. pa_h_bpb_successor_witness_product_terminal + S (x) = S ((S (S e)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_terminal. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_terminal * S ((S (S e)) * pa_v_bpb_successor_witness_product) + (x))) /\ forall pa_i_bpb_successor_witness_product. (exists pa_lt_bpb_successor_witness_product_bound. pa_lt_bpb_successor_witness_product_bound + S pa_i_bpb_successor_witness_product = S e) -> exists pa_p_bpb_successor_witness_product pa_r_bpb_successor_witness_product pa_s_bpb_successor_witness_product. ((((exists pa_h_bpb_successor_witness_product_factor. pa_h_bpb_successor_witness_product_factor + S (pa_p_bpb_successor_witness_product) = S ((S (pa_i_bpb_successor_witness_product)) * pa_c_bpb_successor_witness)) /\ exists pa_q_bpb_successor_witness_product_factor. pa_b_bpb_successor_witness = pa_q_bpb_successor_witness_product_factor * S ((S (pa_i_bpb_successor_witness_product)) * pa_c_bpb_successor_witness) + (pa_p_bpb_successor_witness_product))) /\ ((((exists pa_h_bpb_successor_witness_product_partial. pa_h_bpb_successor_witness_product_partial + S (pa_r_bpb_successor_witness_product) = S ((S (pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_partial. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_partial * S ((S (pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product) + (pa_r_bpb_successor_witness_product))) /\ ((((exists pa_h_bpb_successor_witness_product_successor. pa_h_bpb_successor_witness_product_successor + S (pa_s_bpb_successor_witness_product) = S ((S (S pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product)) /\ exists pa_q_bpb_successor_witness_product_successor. pa_u_bpb_successor_witness_product = pa_q_bpb_successor_witness_product_successor * S ((S (S pa_i_bpb_successor_witness_product)) * pa_v_bpb_successor_witness_product) + (pa_s_bpb_successor_witness_product))) /\ pa_s_bpb_successor_witness_product = pa_r_bpb_successor_witness_product * pa_p_bpb_successor_witness_product))))))))
  8. 0008specialize pow_exists a
  9. 0009specialize pow_exists (S e)
  10. 0010exact pow_exists
  11. 0011cases hsuccessor
  12. 0012have hx : x = r * a
  13. 0013specialize pow_successor_pair_mul a
  14. 0014specialize pow_successor_pair_mul e
  15. 0015specialize pow_successor_pair_mul (S e)
  16. 0016specialize pow_successor_pair_mul r
  17. 0017specialize pow_successor_pair_mul x
  18. 0018apply pow_successor_pair_mul
  19. 0019refl
  20. 0020exact hprevious
  21. 0021exact hsuccessor_witness
  22. 0022have hxn : x = n
  23. 0023trans r * a
  24. 0024exact hx
  25. 0025symm
  26. 0026exact hn
  27. 0027rewrite <- hxn
  28. 0028rewrite <- hxn
  29. 0029exact hsuccessor_witness