SK002D

perfect_power_root_table_exists

A positive gcd bounds all its positive divisors, so a finite table through index g covers every perfect-power degree.

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. ¬g = 0 → (∀ x. ¬x = 0 → Dvd(x,g) → ∃ y. Pow(y,x,n)) → ∃ x. ∃ y. PerfectPowerRootTable(n,g,x,y)

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

Definition DAG

PerfectPowerRootTable(n,g,b,c) · 1Lt(a,b) · 1Dvd(d,n) · 2BetaAt(b,c,i,x) · 1Pow(a,e,z) · 2

Actual proof prerequisites

perfect_power_root_table_prefix_existsdivisor_le_nonzero · checked external prerequisitesucc_le_succ · checked external prerequisite
Original expanded first-order statement 
forall n g. ~(g = 0) -> (forall ppf_degree_complete_table_available. ~(ppf_degree_complete_table_available = 0) -> (exists pvs_factor_complete_table_availabledivisor. (g) = (ppf_degree_complete_table_available) * pvs_factor_complete_table_availabledivisor) -> exists ppf_root_complete_table_available. (exists pa_b_pvs_complete_table_availablepower pa_c_pvs_complete_table_availablepower. ((forall pa_i_pvs_complete_table_availablepower_repeat. (exists pa_lt_pvs_complete_table_availablepower_repeat_bound. pa_lt_pvs_complete_table_availablepower_repeat_bound + S pa_i_pvs_complete_table_availablepower_repeat = ppf_degree_complete_table_available) -> (((exists pa_h_pvs_complete_table_availablepower_repeat_decoded. pa_h_pvs_complete_table_availablepower_repeat_decoded + S (ppf_root_complete_table_available) = S ((S (pa_i_pvs_complete_table_availablepower_repeat)) * pa_c_pvs_complete_table_availablepower)) /\ exists pa_q_pvs_complete_table_availablepower_repeat_decoded. pa_b_pvs_complete_table_availablepower = pa_q_pvs_complete_table_availablepower_repeat_decoded * S ((S (pa_i_pvs_complete_table_availablepower_repeat)) * pa_c_pvs_complete_table_availablepower) + (ppf_root_complete_table_available)))) /\ (exists pa_u_pvs_complete_table_availablepower_product pa_v_pvs_complete_table_availablepower_product. ((((exists pa_h_pvs_complete_table_availablepower_product_start. pa_h_pvs_complete_table_availablepower_product_start + S (1) = S ((S (0)) * pa_v_pvs_complete_table_availablepower_product)) /\ exists pa_q_pvs_complete_table_availablepower_product_start. pa_u_pvs_complete_table_availablepower_product = pa_q_pvs_complete_table_availablepower_product_start * S ((S (0)) * pa_v_pvs_complete_table_availablepower_product) + (1))) /\ ((((exists pa_h_pvs_complete_table_availablepower_product_terminal. pa_h_pvs_complete_table_availablepower_product_terminal + S (n) = S ((S (ppf_degree_complete_table_available)) * pa_v_pvs_complete_table_availablepower_product)) /\ exists pa_q_pvs_complete_table_availablepower_product_terminal. pa_u_pvs_complete_table_availablepower_product = pa_q_pvs_complete_table_availablepower_product_terminal * S ((S (ppf_degree_complete_table_available)) * pa_v_pvs_complete_table_availablepower_product) + (n))) /\ forall pa_i_pvs_complete_table_availablepower_product. (exists pa_lt_pvs_complete_table_availablepower_product_bound. pa_lt_pvs_complete_table_availablepower_product_bound + S pa_i_pvs_complete_table_availablepower_product = ppf_degree_complete_table_available) -> exists pa_p_pvs_complete_table_availablepower_product pa_r_pvs_complete_table_availablepower_product pa_s_pvs_complete_table_availablepower_product. ((((exists pa_h_pvs_complete_table_availablepower_product_factor. pa_h_pvs_complete_table_availablepower_product_factor + S (pa_p_pvs_complete_table_availablepower_product) = S ((S (pa_i_pvs_complete_table_availablepower_product)) * pa_c_pvs_complete_table_availablepower)) /\ exists pa_q_pvs_complete_table_availablepower_product_factor. pa_b_pvs_complete_table_availablepower = pa_q_pvs_complete_table_availablepower_product_factor * S ((S (pa_i_pvs_complete_table_availablepower_product)) * pa_c_pvs_complete_table_availablepower) + (pa_p_pvs_complete_table_availablepower_product))) /\ ((((exists pa_h_pvs_complete_table_availablepower_product_partial. pa_h_pvs_complete_table_availablepower_product_partial + S (pa_r_pvs_complete_table_availablepower_product) = S ((S (pa_i_pvs_complete_table_availablepower_product)) * pa_v_pvs_complete_table_availablepower_product)) /\ exists pa_q_pvs_complete_table_availablepower_product_partial. pa_u_pvs_complete_table_availablepower_product = pa_q_pvs_complete_table_availablepower_product_partial * S ((S (pa_i_pvs_complete_table_availablepower_product)) * pa_v_pvs_complete_table_availablepower_product) + (pa_r_pvs_complete_table_availablepower_product))) /\ ((((exists pa_h_pvs_complete_table_availablepower_product_successor. pa_h_pvs_complete_table_availablepower_product_successor + S (pa_s_pvs_complete_table_availablepower_product) = S ((S (S pa_i_pvs_complete_table_availablepower_product)) * pa_v_pvs_complete_table_availablepower_product)) /\ exists pa_q_pvs_complete_table_availablepower_product_successor. pa_u_pvs_complete_table_availablepower_product = pa_q_pvs_complete_table_availablepower_product_successor * S ((S (S pa_i_pvs_complete_table_availablepower_product)) * pa_v_pvs_complete_table_availablepower_product) + (pa_s_pvs_complete_table_availablepower_product))) /\ pa_s_pvs_complete_table_availablepower_product = pa_r_pvs_complete_table_availablepower_product * pa_p_pvs_complete_table_availablepower_product))))))))) -> exists b c. (forall ppf_table_degree_complete_table. ~(ppf_table_degree_complete_table = 0) -> (exists pvs_factor_complete_tabledivisor. (g) = (ppf_table_degree_complete_table) * pvs_factor_complete_tabledivisor) -> exists ppf_table_root_complete_table. (((exists ff_h_pvs_complete_tableentry. ff_h_pvs_complete_tableentry + S (ppf_table_root_complete_table) = S ((S (ppf_table_degree_complete_table)) * c)) /\ exists ff_q_pvs_complete_tableentry. b = ff_q_pvs_complete_tableentry * S ((S (ppf_table_degree_complete_table)) * c) + (ppf_table_root_complete_table))) /\ (exists pa_b_pvs_complete_tablepower pa_c_pvs_complete_tablepower. ((forall pa_i_pvs_complete_tablepower_repeat. (exists pa_lt_pvs_complete_tablepower_repeat_bound. pa_lt_pvs_complete_tablepower_repeat_bound + S pa_i_pvs_complete_tablepower_repeat = ppf_table_degree_complete_table) -> (((exists pa_h_pvs_complete_tablepower_repeat_decoded. pa_h_pvs_complete_tablepower_repeat_decoded + S (ppf_table_root_complete_table) = S ((S (pa_i_pvs_complete_tablepower_repeat)) * pa_c_pvs_complete_tablepower)) /\ exists pa_q_pvs_complete_tablepower_repeat_decoded. pa_b_pvs_complete_tablepower = pa_q_pvs_complete_tablepower_repeat_decoded * S ((S (pa_i_pvs_complete_tablepower_repeat)) * pa_c_pvs_complete_tablepower) + (ppf_table_root_complete_table)))) /\ (exists pa_u_pvs_complete_tablepower_product pa_v_pvs_complete_tablepower_product. ((((exists pa_h_pvs_complete_tablepower_product_start. pa_h_pvs_complete_tablepower_product_start + S (1) = S ((S (0)) * pa_v_pvs_complete_tablepower_product)) /\ exists pa_q_pvs_complete_tablepower_product_start. pa_u_pvs_complete_tablepower_product = pa_q_pvs_complete_tablepower_product_start * S ((S (0)) * pa_v_pvs_complete_tablepower_product) + (1))) /\ ((((exists pa_h_pvs_complete_tablepower_product_terminal. pa_h_pvs_complete_tablepower_product_terminal + S (n) = S ((S (ppf_table_degree_complete_table)) * pa_v_pvs_complete_tablepower_product)) /\ exists pa_q_pvs_complete_tablepower_product_terminal. pa_u_pvs_complete_tablepower_product = pa_q_pvs_complete_tablepower_product_terminal * S ((S (ppf_table_degree_complete_table)) * pa_v_pvs_complete_tablepower_product) + (n))) /\ forall pa_i_pvs_complete_tablepower_product. (exists pa_lt_pvs_complete_tablepower_product_bound. pa_lt_pvs_complete_tablepower_product_bound + S pa_i_pvs_complete_tablepower_product = ppf_table_degree_complete_table) -> exists pa_p_pvs_complete_tablepower_product pa_r_pvs_complete_tablepower_product pa_s_pvs_complete_tablepower_product. ((((exists pa_h_pvs_complete_tablepower_product_factor. pa_h_pvs_complete_tablepower_product_factor + S (pa_p_pvs_complete_tablepower_product) = S ((S (pa_i_pvs_complete_tablepower_product)) * pa_c_pvs_complete_tablepower)) /\ exists pa_q_pvs_complete_tablepower_product_factor. pa_b_pvs_complete_tablepower = pa_q_pvs_complete_tablepower_product_factor * S ((S (pa_i_pvs_complete_tablepower_product)) * pa_c_pvs_complete_tablepower) + (pa_p_pvs_complete_tablepower_product))) /\ ((((exists pa_h_pvs_complete_tablepower_product_partial. pa_h_pvs_complete_tablepower_product_partial + S (pa_r_pvs_complete_tablepower_product) = S ((S (pa_i_pvs_complete_tablepower_product)) * pa_v_pvs_complete_tablepower_product)) /\ exists pa_q_pvs_complete_tablepower_product_partial. pa_u_pvs_complete_tablepower_product = pa_q_pvs_complete_tablepower_product_partial * S ((S (pa_i_pvs_complete_tablepower_product)) * pa_v_pvs_complete_tablepower_product) + (pa_r_pvs_complete_tablepower_product))) /\ ((((exists pa_h_pvs_complete_tablepower_product_successor. pa_h_pvs_complete_tablepower_product_successor + S (pa_s_pvs_complete_tablepower_product) = S ((S (S pa_i_pvs_complete_tablepower_product)) * pa_v_pvs_complete_tablepower_product)) /\ exists pa_q_pvs_complete_tablepower_product_successor. pa_u_pvs_complete_tablepower_product = pa_q_pvs_complete_tablepower_product_successor * S ((S (S pa_i_pvs_complete_tablepower_product)) * pa_v_pvs_complete_tablepower_product) + (pa_s_pvs_complete_tablepower_product))) /\ pa_s_pvs_complete_tablepower_product = pa_r_pvs_complete_tablepower_product * pa_p_pvs_complete_tablepower_product)))))))))

Complete tactic proof in conservative notation

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

29 script commands · 7 reading checkpoints · 1 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 (1)
perfect power root table prefix exists
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 hg
  4. L4
    intro havailable
02Establish htableL5–10

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

  1. L5
    have htable : ∃ b. ∃ c. ∀ x. Lt(x,S g) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(b,c,x,y) ∧ Pow(y,x,n)Definitions: Lt(x,S g)Dvd(x,g)BetaAt(b,c,x,y)Pow(y,x,n)Original native command in the exact edition
  2. L6
    specialize perfect_power_root_table_prefix_exists (S g)
  3. L7
    specialize perfect_power_root_table_prefix_exists (n)
  4. L8
    specialize perfect_power_root_table_prefix_exists (g)
  5. L9
    apply perfect_power_root_table_prefix_exists
  6. L10
    exact havailable
03Separate the logical casesL11–12

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

  1. L11
    cases htable
  2. L12
    cases htable_witness
04Construct an explicit witnessL13–14

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

  1. L13
    exists x
  2. L14
    exists x1
05Fix variables and assumptionsL15–17

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

  1. L15
    intro k
  2. L16
    intro hk
  3. L17
    intro hdiv
06Use earlier factsL18–27

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

  1. L18
    specialize htable_witness_witness (k)
  2. L19
    apply htable_witness_witness
  3. L20
    specialize succ_le_succ (k)
  4. L21
    specialize succ_le_succ (g)
  5. L22
    apply succ_le_succ
  6. L23
    specialize divisor_le_nonzero (k)
  7. L24
    specialize divisor_le_nonzero (g)
  8. L25
    apply divisor_le_nonzero
  9. L26
    exact hg
  10. L27
    exact hdiv
07Use earlier factsL28–29

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

  1. L28
    exact hk
  2. L29
    exact hdiv

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro n
  2. 0002intro g
  3. 0003intro hg
  4. 0004intro havailable
  5. 0005have htable : ∃ b. ∃ c. ∀ x. Lt(x,S g) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(b,c,x,y) ∧ Pow(y,x,n)
  6. 0006specialize perfect_power_root_table_prefix_exists (S g)
  7. 0007specialize perfect_power_root_table_prefix_exists (n)
  8. 0008specialize perfect_power_root_table_prefix_exists (g)
  9. 0009apply perfect_power_root_table_prefix_exists
  10. 0010exact havailable
  11. 0011cases htable
  12. 0012cases htable_witness
  13. 0013exists x
  14. 0014exists x1
  15. 0015intro k
  16. 0016intro hk
  17. 0017intro hdiv
  18. 0018specialize htable_witness_witness (k)
  19. 0019apply htable_witness_witness
  20. 0020specialize succ_le_succ (k)
  21. 0021specialize succ_le_succ (g)
  22. 0022apply succ_le_succ
  23. 0023specialize divisor_le_nonzero (k)
  24. 0024specialize divisor_le_nonzero (g)
  25. 0025apply divisor_le_nonzero
  26. 0026exact hg
  27. 0027exact hdiv
  28. 0028exact hk
  29. 0029exact hdiv