SK002B

perfect_power_root_table_conditional_entry

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

Decidable degree-zero and divisor tests construct a real root where required and a harmless zero filler elsewhere.

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 g L. (forall ppf_degree_table_available. ~(ppf_degree_table_available = 0) -> (exists pvs_factor_table_availabledivisor. (g) = (ppf_degree_table_available) * pvs_factor_table_availabledivisor) -> exists ppf_root_table_available. (exists pa_b_pvs_table_availablepower pa_c_pvs_table_availablepower. ((forall pa_i_pvs_table_availablepower_repeat. (exists pa_lt_pvs_table_availablepower_repeat_bound. pa_lt_pvs_table_availablepower_repeat_bound + S pa_i_pvs_table_availablepower_repeat = ppf_degree_table_available) -> (((exists pa_h_pvs_table_availablepower_repeat_decoded. pa_h_pvs_table_availablepower_repeat_decoded + S (ppf_root_table_available) = S ((S (pa_i_pvs_table_availablepower_repeat)) * pa_c_pvs_table_availablepower)) /\ exists pa_q_pvs_table_availablepower_repeat_decoded. pa_b_pvs_table_availablepower = pa_q_pvs_table_availablepower_repeat_decoded * S ((S (pa_i_pvs_table_availablepower_repeat)) * pa_c_pvs_table_availablepower) + (ppf_root_table_available)))) /\ (exists pa_u_pvs_table_availablepower_product pa_v_pvs_table_availablepower_product. ((((exists pa_h_pvs_table_availablepower_product_start. pa_h_pvs_table_availablepower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_availablepower_product)) /\ exists pa_q_pvs_table_availablepower_product_start. pa_u_pvs_table_availablepower_product = pa_q_pvs_table_availablepower_product_start * S ((S (0)) * pa_v_pvs_table_availablepower_product) + (1))) /\ ((((exists pa_h_pvs_table_availablepower_product_terminal. pa_h_pvs_table_availablepower_product_terminal + S (n) = S ((S (ppf_degree_table_available)) * pa_v_pvs_table_availablepower_product)) /\ exists pa_q_pvs_table_availablepower_product_terminal. pa_u_pvs_table_availablepower_product = pa_q_pvs_table_availablepower_product_terminal * S ((S (ppf_degree_table_available)) * pa_v_pvs_table_availablepower_product) + (n))) /\ forall pa_i_pvs_table_availablepower_product. (exists pa_lt_pvs_table_availablepower_product_bound. pa_lt_pvs_table_availablepower_product_bound + S pa_i_pvs_table_availablepower_product = ppf_degree_table_available) -> exists pa_p_pvs_table_availablepower_product pa_r_pvs_table_availablepower_product pa_s_pvs_table_availablepower_product. ((((exists pa_h_pvs_table_availablepower_product_factor. pa_h_pvs_table_availablepower_product_factor + S (pa_p_pvs_table_availablepower_product) = S ((S (pa_i_pvs_table_availablepower_product)) * pa_c_pvs_table_availablepower)) /\ exists pa_q_pvs_table_availablepower_product_factor. pa_b_pvs_table_availablepower = pa_q_pvs_table_availablepower_product_factor * S ((S (pa_i_pvs_table_availablepower_product)) * pa_c_pvs_table_availablepower) + (pa_p_pvs_table_availablepower_product))) /\ ((((exists pa_h_pvs_table_availablepower_product_partial. pa_h_pvs_table_availablepower_product_partial + S (pa_r_pvs_table_availablepower_product) = S ((S (pa_i_pvs_table_availablepower_product)) * pa_v_pvs_table_availablepower_product)) /\ exists pa_q_pvs_table_availablepower_product_partial. pa_u_pvs_table_availablepower_product = pa_q_pvs_table_availablepower_product_partial * S ((S (pa_i_pvs_table_availablepower_product)) * pa_v_pvs_table_availablepower_product) + (pa_r_pvs_table_availablepower_product))) /\ ((((exists pa_h_pvs_table_availablepower_product_successor. pa_h_pvs_table_availablepower_product_successor + S (pa_s_pvs_table_availablepower_product) = S ((S (S pa_i_pvs_table_availablepower_product)) * pa_v_pvs_table_availablepower_product)) /\ exists pa_q_pvs_table_availablepower_product_successor. pa_u_pvs_table_availablepower_product = pa_q_pvs_table_availablepower_product_successor * S ((S (S pa_i_pvs_table_availablepower_product)) * pa_v_pvs_table_availablepower_product) + (pa_s_pvs_table_availablepower_product))) /\ pa_s_pvs_table_availablepower_product = pa_r_pvs_table_availablepower_product * pa_p_pvs_table_availablepower_product))))))))) -> exists R. ~(L = 0) -> (exists pvs_factor_table_degree_divisor. (g) = (L) * pvs_factor_table_degree_divisor) -> (exists pa_b_pvs_table_selected_root pa_c_pvs_table_selected_root. ((forall pa_i_pvs_table_selected_root_repeat. (exists pa_lt_pvs_table_selected_root_repeat_bound. pa_lt_pvs_table_selected_root_repeat_bound + S pa_i_pvs_table_selected_root_repeat = L) -> (((exists pa_h_pvs_table_selected_root_repeat_decoded. pa_h_pvs_table_selected_root_repeat_decoded + S (R) = S ((S (pa_i_pvs_table_selected_root_repeat)) * pa_c_pvs_table_selected_root)) /\ exists pa_q_pvs_table_selected_root_repeat_decoded. pa_b_pvs_table_selected_root = pa_q_pvs_table_selected_root_repeat_decoded * S ((S (pa_i_pvs_table_selected_root_repeat)) * pa_c_pvs_table_selected_root) + (R)))) /\ (exists pa_u_pvs_table_selected_root_product pa_v_pvs_table_selected_root_product. ((((exists pa_h_pvs_table_selected_root_product_start. pa_h_pvs_table_selected_root_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_selected_root_product)) /\ exists pa_q_pvs_table_selected_root_product_start. pa_u_pvs_table_selected_root_product = pa_q_pvs_table_selected_root_product_start * S ((S (0)) * pa_v_pvs_table_selected_root_product) + (1))) /\ ((((exists pa_h_pvs_table_selected_root_product_terminal. pa_h_pvs_table_selected_root_product_terminal + S (n) = S ((S (L)) * pa_v_pvs_table_selected_root_product)) /\ exists pa_q_pvs_table_selected_root_product_terminal. pa_u_pvs_table_selected_root_product = pa_q_pvs_table_selected_root_product_terminal * S ((S (L)) * pa_v_pvs_table_selected_root_product) + (n))) /\ forall pa_i_pvs_table_selected_root_product. (exists pa_lt_pvs_table_selected_root_product_bound. pa_lt_pvs_table_selected_root_product_bound + S pa_i_pvs_table_selected_root_product = L) -> exists pa_p_pvs_table_selected_root_product pa_r_pvs_table_selected_root_product pa_s_pvs_table_selected_root_product. ((((exists pa_h_pvs_table_selected_root_product_factor. pa_h_pvs_table_selected_root_product_factor + S (pa_p_pvs_table_selected_root_product) = S ((S (pa_i_pvs_table_selected_root_product)) * pa_c_pvs_table_selected_root)) /\ exists pa_q_pvs_table_selected_root_product_factor. pa_b_pvs_table_selected_root = pa_q_pvs_table_selected_root_product_factor * S ((S (pa_i_pvs_table_selected_root_product)) * pa_c_pvs_table_selected_root) + (pa_p_pvs_table_selected_root_product))) /\ ((((exists pa_h_pvs_table_selected_root_product_partial. pa_h_pvs_table_selected_root_product_partial + S (pa_r_pvs_table_selected_root_product) = S ((S (pa_i_pvs_table_selected_root_product)) * pa_v_pvs_table_selected_root_product)) /\ exists pa_q_pvs_table_selected_root_product_partial. pa_u_pvs_table_selected_root_product = pa_q_pvs_table_selected_root_product_partial * S ((S (pa_i_pvs_table_selected_root_product)) * pa_v_pvs_table_selected_root_product) + (pa_r_pvs_table_selected_root_product))) /\ ((((exists pa_h_pvs_table_selected_root_product_successor. pa_h_pvs_table_selected_root_product_successor + S (pa_s_pvs_table_selected_root_product) = S ((S (S pa_i_pvs_table_selected_root_product)) * pa_v_pvs_table_selected_root_product)) /\ exists pa_q_pvs_table_selected_root_product_successor. pa_u_pvs_table_selected_root_product = pa_q_pvs_table_selected_root_product_successor * S ((S (S pa_i_pvs_table_selected_root_product)) * pa_v_pvs_table_selected_root_product) + (pa_s_pvs_table_selected_root_product))) /\ pa_s_pvs_table_selected_root_product = pa_r_pvs_table_selected_root_product * pa_p_pvs_table_selected_root_product))))))))

Constructive proof overview

Generated structural guide

Decidable degree-zero and divisor tests construct a real root where required and a harmless zero filler elsewhere.

The unchanged tactic script uses 2 declared prerequisites and contains 36 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized multiple_decidable Stable theorem; checked-use authorized

Direct dependents

SK002C perfect_power_root_table_prefix_exists

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

36 script commands · 18 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.

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

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

  1. L1
    intro n
  2. L2
    intro g
  3. L3
    intro L
  4. L4
    intro havailable
02Establish hzeroL5–8

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

  1. L5
    have hzero : L = 0 \/ ~(L = 0)
  2. L6
    specialize eq_decidable (L)
  3. L7
    specialize eq_decidable (0)
  4. L8
    apply eq_decidable
03Separate the logical casesL9–9

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

  1. L9
    cases hzero
04Construct an explicit witnessL10–10

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

  1. L10
    exists 0
05Fix variables and assumptionsL11–12

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

  1. L11
    intro hL
  2. L12
    intro hdiv
06Separate the logical casesL13–13

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

  1. L13
    exfalso
07Use earlier factsL14–15

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

  1. L14
    apply hL
  2. L15
    exact hzero_left
08Establish hdivL16–19

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

  1. L16
    have hdiv : (exists pvs_factor_table_decidable_divisor. (g) = (L) * pvs_factor_table_decidable_divisor) \/ ~(exists pvs_factor_table_decidable_nondivisor. (g) = (L) * pvs_factor_table_decidable_nondivisor)
  2. L17
    specialize multiple_decidable (L)
  3. L18
    specialize multiple_decidable (g)
  4. L19
    apply multiple_decidable
09Separate the logical casesL20–20

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

  1. L20
    cases hdiv
10Establish hrootL21–25

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

  1. L21
    have hroot : ∃ R. Pow(R,L,n)Definitions: Pow
  2. L22
    specialize havailable (L)
  3. L23
    apply havailable
  4. L24
    exact hzero_right
  5. L25
    exact hdiv_left
11Separate the logical casesL26–26

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

  1. L26
    cases hroot
12Construct an explicit witnessL27–27

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

  1. L27
    exists x
13Fix variables and assumptionsL28–29

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

  1. L28
    intro hL
  2. L29
    intro hdivisor
14Use earlier factsL30–30

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

  1. L30
    exact hroot_witness
15Construct an explicit witnessL31–31

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

  1. L31
    exists 0
16Fix variables and assumptionsL32–33

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

  1. L32
    intro hL
  2. L33
    intro hdivisor
17Separate the logical casesL34–34

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

  1. L34
    exfalso
18Use earlier factsL35–36

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

  1. L35
    apply hdiv_right
  2. L36
    exact hdivisor

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro n
  2. 0002intro g
  3. 0003intro L
  4. 0004intro havailable
  5. 0005have hzero : L = 0 \/ ~(L = 0)
  6. 0006specialize eq_decidable (L)
  7. 0007specialize eq_decidable (0)
  8. 0008apply eq_decidable
  9. 0009cases hzero
  10. 0010exists 0
  11. 0011intro hL
  12. 0012intro hdiv
  13. 0013exfalso
  14. 0014apply hL
  15. 0015exact hzero_left
  16. 0016have hdiv : (exists pvs_factor_table_decidable_divisor. (g) = (L) * pvs_factor_table_decidable_divisor) \/ ~(exists pvs_factor_table_decidable_nondivisor. (g) = (L) * pvs_factor_table_decidable_nondivisor)
  17. 0017specialize multiple_decidable (L)
  18. 0018specialize multiple_decidable (g)
  19. 0019apply multiple_decidable
  20. 0020cases hdiv
  21. 0021have hroot : exists R. (exists pa_b_pvs_table_chosen pa_c_pvs_table_chosen. ((forall pa_i_pvs_table_chosen_repeat. (exists pa_lt_pvs_table_chosen_repeat_bound. pa_lt_pvs_table_chosen_repeat_bound + S pa_i_pvs_table_chosen_repeat = L) -> (((exists pa_h_pvs_table_chosen_repeat_decoded. pa_h_pvs_table_chosen_repeat_decoded + S (R) = S ((S (pa_i_pvs_table_chosen_repeat)) * pa_c_pvs_table_chosen)) /\ exists pa_q_pvs_table_chosen_repeat_decoded. pa_b_pvs_table_chosen = pa_q_pvs_table_chosen_repeat_decoded * S ((S (pa_i_pvs_table_chosen_repeat)) * pa_c_pvs_table_chosen) + (R)))) /\ (exists pa_u_pvs_table_chosen_product pa_v_pvs_table_chosen_product. ((((exists pa_h_pvs_table_chosen_product_start. pa_h_pvs_table_chosen_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_chosen_product)) /\ exists pa_q_pvs_table_chosen_product_start. pa_u_pvs_table_chosen_product = pa_q_pvs_table_chosen_product_start * S ((S (0)) * pa_v_pvs_table_chosen_product) + (1))) /\ ((((exists pa_h_pvs_table_chosen_product_terminal. pa_h_pvs_table_chosen_product_terminal + S (n) = S ((S (L)) * pa_v_pvs_table_chosen_product)) /\ exists pa_q_pvs_table_chosen_product_terminal. pa_u_pvs_table_chosen_product = pa_q_pvs_table_chosen_product_terminal * S ((S (L)) * pa_v_pvs_table_chosen_product) + (n))) /\ forall pa_i_pvs_table_chosen_product. (exists pa_lt_pvs_table_chosen_product_bound. pa_lt_pvs_table_chosen_product_bound + S pa_i_pvs_table_chosen_product = L) -> exists pa_p_pvs_table_chosen_product pa_r_pvs_table_chosen_product pa_s_pvs_table_chosen_product. ((((exists pa_h_pvs_table_chosen_product_factor. pa_h_pvs_table_chosen_product_factor + S (pa_p_pvs_table_chosen_product) = S ((S (pa_i_pvs_table_chosen_product)) * pa_c_pvs_table_chosen)) /\ exists pa_q_pvs_table_chosen_product_factor. pa_b_pvs_table_chosen = pa_q_pvs_table_chosen_product_factor * S ((S (pa_i_pvs_table_chosen_product)) * pa_c_pvs_table_chosen) + (pa_p_pvs_table_chosen_product))) /\ ((((exists pa_h_pvs_table_chosen_product_partial. pa_h_pvs_table_chosen_product_partial + S (pa_r_pvs_table_chosen_product) = S ((S (pa_i_pvs_table_chosen_product)) * pa_v_pvs_table_chosen_product)) /\ exists pa_q_pvs_table_chosen_product_partial. pa_u_pvs_table_chosen_product = pa_q_pvs_table_chosen_product_partial * S ((S (pa_i_pvs_table_chosen_product)) * pa_v_pvs_table_chosen_product) + (pa_r_pvs_table_chosen_product))) /\ ((((exists pa_h_pvs_table_chosen_product_successor. pa_h_pvs_table_chosen_product_successor + S (pa_s_pvs_table_chosen_product) = S ((S (S pa_i_pvs_table_chosen_product)) * pa_v_pvs_table_chosen_product)) /\ exists pa_q_pvs_table_chosen_product_successor. pa_u_pvs_table_chosen_product = pa_q_pvs_table_chosen_product_successor * S ((S (S pa_i_pvs_table_chosen_product)) * pa_v_pvs_table_chosen_product) + (pa_s_pvs_table_chosen_product))) /\ pa_s_pvs_table_chosen_product = pa_r_pvs_table_chosen_product * pa_p_pvs_table_chosen_product))))))))
  22. 0022specialize havailable (L)
  23. 0023apply havailable
  24. 0024exact hzero_right
  25. 0025exact hdiv_left
  26. 0026cases hroot
  27. 0027exists x
  28. 0028intro hL
  29. 0029intro hdivisor
  30. 0030exact hroot_witness
  31. 0031exists 0
  32. 0032intro hL
  33. 0033intro hdivisor
  34. 0034exfalso
  35. 0035apply hdiv_right
  36. 0036exact hdivisor