SK002B

perfect_power_root_table_conditional_entry

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

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

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.

For n>1 the exponent gcd and a real beta table classify and witness all positive root degrees. The unit n=1 has a separate uniform certificate for every positive degree. Zero is excluded. NaturalSquarefreeDecomposition is deliberately distinct from the unrelated polynomial definition.

Exact theorem in conservative defined notation

∀ n. ∀ g. ∀ L. (∀ x. ¬x = 0 → Dvd(x,g) → ∃ y. Pow(y,x,n)) → ∃ x. ¬L = 0 → Dvd(L,g) → Pow(x,L,n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Dvd(d,n) · 4Pow(a,e,z) · 3

Actual proof prerequisites

eq_decidable · checked external prerequisitemultiple_decidable · checked external prerequisite
Original expanded first-order 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))))))))

Complete tactic proof in conservative notation

All 36 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Dvd(L,g) ∨ ¬Dvd(L,g)Definitions: Dvd(L,g)Original native command in the exact edition
  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(R,L,n)Original native command in the exact edition
  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 defined 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 : Dvd(L,g) ∨ ¬Dvd(L,g)
  17. 0017specialize multiple_decidable (L)
  18. 0018specialize multiple_decidable (g)
  19. 0019apply multiple_decidable
  20. 0020cases hdiv
  21. 0021have hroot : ∃ R. Pow(R,L,n)
  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