SK002C

perfect_power_root_table_prefix_exists

Finite induction constructs an actual beta table from the already proved pointwise root theorem, without any finite-choice axiom.

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

∀ L. ∀ n. ∀ g. (∀ x. ¬x = 0 → Dvd(x,g) → ∃ y. Pow(y,x,n)) → ∃ x. ∃ y. ∀ z. Lt(z,L) → ¬z = 0 → Dvd(z,g) → ∃ m. BetaAt(x,y,z,m) ∧ Pow(m,z,n)

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

Definition DAG

Lt(a,b) · 3Dvd(d,n) · 4BetaAt(b,c,i,x) · 5Pow(a,e,z) · 4

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisiteperfect_power_root_table_conditional_entrybeta_prefix_extend · checked external prerequisiteperfect_power_root_table_prefix_append
Original expanded first-order statement 
forall L n g. (forall ppf_degree_table_prefix_available. ~(ppf_degree_table_prefix_available = 0) -> (exists pvs_factor_table_prefix_availabledivisor. (g) = (ppf_degree_table_prefix_available) * pvs_factor_table_prefix_availabledivisor) -> exists ppf_root_table_prefix_available. (exists pa_b_pvs_table_prefix_availablepower pa_c_pvs_table_prefix_availablepower. ((forall pa_i_pvs_table_prefix_availablepower_repeat. (exists pa_lt_pvs_table_prefix_availablepower_repeat_bound. pa_lt_pvs_table_prefix_availablepower_repeat_bound + S pa_i_pvs_table_prefix_availablepower_repeat = ppf_degree_table_prefix_available) -> (((exists pa_h_pvs_table_prefix_availablepower_repeat_decoded. pa_h_pvs_table_prefix_availablepower_repeat_decoded + S (ppf_root_table_prefix_available) = S ((S (pa_i_pvs_table_prefix_availablepower_repeat)) * pa_c_pvs_table_prefix_availablepower)) /\ exists pa_q_pvs_table_prefix_availablepower_repeat_decoded. pa_b_pvs_table_prefix_availablepower = pa_q_pvs_table_prefix_availablepower_repeat_decoded * S ((S (pa_i_pvs_table_prefix_availablepower_repeat)) * pa_c_pvs_table_prefix_availablepower) + (ppf_root_table_prefix_available)))) /\ (exists pa_u_pvs_table_prefix_availablepower_product pa_v_pvs_table_prefix_availablepower_product. ((((exists pa_h_pvs_table_prefix_availablepower_product_start. pa_h_pvs_table_prefix_availablepower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_start. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_start * S ((S (0)) * pa_v_pvs_table_prefix_availablepower_product) + (1))) /\ ((((exists pa_h_pvs_table_prefix_availablepower_product_terminal. pa_h_pvs_table_prefix_availablepower_product_terminal + S (n) = S ((S (ppf_degree_table_prefix_available)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_terminal. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_terminal * S ((S (ppf_degree_table_prefix_available)) * pa_v_pvs_table_prefix_availablepower_product) + (n))) /\ forall pa_i_pvs_table_prefix_availablepower_product. (exists pa_lt_pvs_table_prefix_availablepower_product_bound. pa_lt_pvs_table_prefix_availablepower_product_bound + S pa_i_pvs_table_prefix_availablepower_product = ppf_degree_table_prefix_available) -> exists pa_p_pvs_table_prefix_availablepower_product pa_r_pvs_table_prefix_availablepower_product pa_s_pvs_table_prefix_availablepower_product. ((((exists pa_h_pvs_table_prefix_availablepower_product_factor. pa_h_pvs_table_prefix_availablepower_product_factor + S (pa_p_pvs_table_prefix_availablepower_product) = S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_c_pvs_table_prefix_availablepower)) /\ exists pa_q_pvs_table_prefix_availablepower_product_factor. pa_b_pvs_table_prefix_availablepower = pa_q_pvs_table_prefix_availablepower_product_factor * S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_c_pvs_table_prefix_availablepower) + (pa_p_pvs_table_prefix_availablepower_product))) /\ ((((exists pa_h_pvs_table_prefix_availablepower_product_partial. pa_h_pvs_table_prefix_availablepower_product_partial + S (pa_r_pvs_table_prefix_availablepower_product) = S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_partial. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_partial * S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product) + (pa_r_pvs_table_prefix_availablepower_product))) /\ ((((exists pa_h_pvs_table_prefix_availablepower_product_successor. pa_h_pvs_table_prefix_availablepower_product_successor + S (pa_s_pvs_table_prefix_availablepower_product) = S ((S (S pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_successor. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_successor * S ((S (S pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product) + (pa_s_pvs_table_prefix_availablepower_product))) /\ pa_s_pvs_table_prefix_availablepower_product = pa_r_pvs_table_prefix_availablepower_product * pa_p_pvs_table_prefix_availablepower_product))))))))) -> exists b c. (forall ppf_table_degree_table_prefix_constructed. (exists pvs_gap_table_prefix_constructedbound. pvs_gap_table_prefix_constructedbound + S (ppf_table_degree_table_prefix_constructed) = (L)) -> ~(ppf_table_degree_table_prefix_constructed = 0) -> (exists pvs_factor_table_prefix_constructeddivisor. (g) = (ppf_table_degree_table_prefix_constructed) * pvs_factor_table_prefix_constructeddivisor) -> exists ppf_table_root_table_prefix_constructed. (((exists ff_h_pvs_table_prefix_constructedentry. ff_h_pvs_table_prefix_constructedentry + S (ppf_table_root_table_prefix_constructed) = S ((S (ppf_table_degree_table_prefix_constructed)) * c)) /\ exists ff_q_pvs_table_prefix_constructedentry. b = ff_q_pvs_table_prefix_constructedentry * S ((S (ppf_table_degree_table_prefix_constructed)) * c) + (ppf_table_root_table_prefix_constructed))) /\ (exists pa_b_pvs_table_prefix_constructedpower pa_c_pvs_table_prefix_constructedpower. ((forall pa_i_pvs_table_prefix_constructedpower_repeat. (exists pa_lt_pvs_table_prefix_constructedpower_repeat_bound. pa_lt_pvs_table_prefix_constructedpower_repeat_bound + S pa_i_pvs_table_prefix_constructedpower_repeat = ppf_table_degree_table_prefix_constructed) -> (((exists pa_h_pvs_table_prefix_constructedpower_repeat_decoded. pa_h_pvs_table_prefix_constructedpower_repeat_decoded + S (ppf_table_root_table_prefix_constructed) = S ((S (pa_i_pvs_table_prefix_constructedpower_repeat)) * pa_c_pvs_table_prefix_constructedpower)) /\ exists pa_q_pvs_table_prefix_constructedpower_repeat_decoded. pa_b_pvs_table_prefix_constructedpower = pa_q_pvs_table_prefix_constructedpower_repeat_decoded * S ((S (pa_i_pvs_table_prefix_constructedpower_repeat)) * pa_c_pvs_table_prefix_constructedpower) + (ppf_table_root_table_prefix_constructed)))) /\ (exists pa_u_pvs_table_prefix_constructedpower_product pa_v_pvs_table_prefix_constructedpower_product. ((((exists pa_h_pvs_table_prefix_constructedpower_product_start. pa_h_pvs_table_prefix_constructedpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_start. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_start * S ((S (0)) * pa_v_pvs_table_prefix_constructedpower_product) + (1))) /\ ((((exists pa_h_pvs_table_prefix_constructedpower_product_terminal. pa_h_pvs_table_prefix_constructedpower_product_terminal + S (n) = S ((S (ppf_table_degree_table_prefix_constructed)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_terminal. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_terminal * S ((S (ppf_table_degree_table_prefix_constructed)) * pa_v_pvs_table_prefix_constructedpower_product) + (n))) /\ forall pa_i_pvs_table_prefix_constructedpower_product. (exists pa_lt_pvs_table_prefix_constructedpower_product_bound. pa_lt_pvs_table_prefix_constructedpower_product_bound + S pa_i_pvs_table_prefix_constructedpower_product = ppf_table_degree_table_prefix_constructed) -> exists pa_p_pvs_table_prefix_constructedpower_product pa_r_pvs_table_prefix_constructedpower_product pa_s_pvs_table_prefix_constructedpower_product. ((((exists pa_h_pvs_table_prefix_constructedpower_product_factor. pa_h_pvs_table_prefix_constructedpower_product_factor + S (pa_p_pvs_table_prefix_constructedpower_product) = S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_c_pvs_table_prefix_constructedpower)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_factor. pa_b_pvs_table_prefix_constructedpower = pa_q_pvs_table_prefix_constructedpower_product_factor * S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_c_pvs_table_prefix_constructedpower) + (pa_p_pvs_table_prefix_constructedpower_product))) /\ ((((exists pa_h_pvs_table_prefix_constructedpower_product_partial. pa_h_pvs_table_prefix_constructedpower_product_partial + S (pa_r_pvs_table_prefix_constructedpower_product) = S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_partial. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_partial * S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product) + (pa_r_pvs_table_prefix_constructedpower_product))) /\ ((((exists pa_h_pvs_table_prefix_constructedpower_product_successor. pa_h_pvs_table_prefix_constructedpower_product_successor + S (pa_s_pvs_table_prefix_constructedpower_product) = S ((S (S pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_successor. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_successor * S ((S (S pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product) + (pa_s_pvs_table_prefix_constructedpower_product))) /\ pa_s_pvs_table_prefix_constructedpower_product = pa_r_pvs_table_prefix_constructedpower_product * pa_p_pvs_table_prefix_constructedpower_product)))))))))

Complete tactic proof in conservative notation

All 56 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

56 script commands · 16 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.

Named ingredients (2)
perfect power root table conditional entryperfect power root table prefix append
01Fix variables and assumptionsL1–1

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

  1. L1
    intro L
02Induction on LL2–5

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

  1. L2
    induction L
  2. L3
    intro n
  3. L4
    intro g
  4. L5
    intro havailable
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–11

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

  1. L8
    intro k
  2. L9
    intro hbound
  3. L10
    intro hk
  4. L11
    intro hdiv
05Separate the logical casesL12–12

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

  1. L12
    exfalso
06Use earlier factsL13–15

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

  1. L13
    specialize factor_permutation_below_zero_impossible (k)
  2. L14
    apply factor_permutation_below_zero_impossible
  3. L15
    exact hbound
07Fix variables and assumptionsL16–18

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

  1. L16
    intro n
  2. L17
    intro g
  3. L18
    intro havailable
08Establish hrootL19–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply perfect power root table conditional entry.

  1. L19
    have hroot : ∃ R. ¬L = 0 → Dvd(L,g) → Pow(R,L,n)Definitions: Dvd(L,g)Pow(R,L,n)Original native command in the exact edition
  2. L20
    specialize perfect_power_root_table_conditional_entry (n)
  3. L21
    specialize perfect_power_root_table_conditional_entry (g)
  4. L22
    specialize perfect_power_root_table_conditional_entry (L)
  5. L23
    apply perfect_power_root_table_conditional_entry
  6. L24
    exact havailable
09Separate the logical casesL25–25

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

  1. L25
    cases hroot
10Establish hpreviousL26–30

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

  1. L26
    have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,L) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(b,c,x,y) ∧ Pow(y,x,n)Definitions: Lt(x,L)Dvd(x,g)BetaAt(b,c,x,y)Pow(y,x,n)Original native command in the exact edition
  2. L27
    specialize IH (n)
  3. L28
    specialize IH (g)
  4. L29
    apply IH
  5. L30
    exact havailable
11Separate the logical casesL31–32

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

  1. L31
    cases hprevious
  2. L32
    cases hprevious_witness
12Establish hextendL33–38

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

  1. L33
    have hextend : ∃ b. ∃ c. BetaAt(b,c,L,x) ∧ (∀ y. ∀ z. Lt(y,L) → BetaAt(x1,x2,y,z) → BetaAt(b,c,y,z))Definitions: BetaAt(b,c,L,x)Lt(y,L)BetaAt(x1,x2,y,z)BetaAt(b,c,y,z)Original native command in the exact edition
  2. L34
    specialize beta_prefix_extend (L)
  3. L35
    specialize beta_prefix_extend (x1)
  4. L36
    specialize beta_prefix_extend (x2)
  5. L37
    specialize beta_prefix_extend (x)
  6. L38
    apply beta_prefix_extend
13Separate the logical casesL39–41

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

  1. L39
    cases hextend
  2. L40
    cases hextend_witness
  3. L41
    cases hextend_witness_witness
14Construct an explicit witnessL42–43

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

  1. L42
    exists x3
  2. L43
    exists x4
15Use earlier factsL44–53

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

  1. L44
    specialize perfect_power_root_table_prefix_append (n)
  2. L45
    specialize perfect_power_root_table_prefix_append (g)
  3. L46
    specialize perfect_power_root_table_prefix_append (x1)
  4. L47
    specialize perfect_power_root_table_prefix_append (x2)
  5. L48
    specialize perfect_power_root_table_prefix_append (x3)
  6. L49
    specialize perfect_power_root_table_prefix_append (x4)
  7. L50
    specialize perfect_power_root_table_prefix_append (L)
  8. L51
    specialize perfect_power_root_table_prefix_append (x)
  9. L52
    apply perfect_power_root_table_prefix_append
  10. L53
    exact hprevious_witness_witness
16Use earlier factsL54–56

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

  1. L54
    exact hextend_witness_witness_right
  2. L55
    exact hextend_witness_witness_left
  3. L56
    exact hroot_witness

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro L
  2. 0002induction L
  3. 0003intro n
  4. 0004intro g
  5. 0005intro havailable
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro k
  9. 0009intro hbound
  10. 0010intro hk
  11. 0011intro hdiv
  12. 0012exfalso
  13. 0013specialize factor_permutation_below_zero_impossible (k)
  14. 0014apply factor_permutation_below_zero_impossible
  15. 0015exact hbound
  16. 0016intro n
  17. 0017intro g
  18. 0018intro havailable
  19. 0019have hroot : ∃ R. ¬L = 0 → Dvd(L,g) → Pow(R,L,n)
  20. 0020specialize perfect_power_root_table_conditional_entry (n)
  21. 0021specialize perfect_power_root_table_conditional_entry (g)
  22. 0022specialize perfect_power_root_table_conditional_entry (L)
  23. 0023apply perfect_power_root_table_conditional_entry
  24. 0024exact havailable
  25. 0025cases hroot
  26. 0026have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,L) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(b,c,x,y) ∧ Pow(y,x,n)
  27. 0027specialize IH (n)
  28. 0028specialize IH (g)
  29. 0029apply IH
  30. 0030exact havailable
  31. 0031cases hprevious
  32. 0032cases hprevious_witness
  33. 0033have hextend : ∃ b. ∃ c. BetaAt(b,c,L,x) ∧ (∀ y. ∀ z. Lt(y,L) → BetaAt(x1,x2,y,z) → BetaAt(b,c,y,z))
  34. 0034specialize beta_prefix_extend (L)
  35. 0035specialize beta_prefix_extend (x1)
  36. 0036specialize beta_prefix_extend (x2)
  37. 0037specialize beta_prefix_extend (x)
  38. 0038apply beta_prefix_extend
  39. 0039cases hextend
  40. 0040cases hextend_witness
  41. 0041cases hextend_witness_witness
  42. 0042exists x3
  43. 0043exists x4
  44. 0044specialize perfect_power_root_table_prefix_append (n)
  45. 0045specialize perfect_power_root_table_prefix_append (g)
  46. 0046specialize perfect_power_root_table_prefix_append (x1)
  47. 0047specialize perfect_power_root_table_prefix_append (x2)
  48. 0048specialize perfect_power_root_table_prefix_append (x3)
  49. 0049specialize perfect_power_root_table_prefix_append (x4)
  50. 0050specialize perfect_power_root_table_prefix_append (L)
  51. 0051specialize perfect_power_root_table_prefix_append (x)
  52. 0052apply perfect_power_root_table_prefix_append
  53. 0053exact hprevious_witness_witness
  54. 0054exact hextend_witness_witness_right
  55. 0055exact hextend_witness_witness_left
  56. 0056exact hroot_witness