SK002A

perfect_power_root_table_prefix_append

Append one actual conditional root and preserve all earlier actual decoded roots in a beta prefix.

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. ∀ b. ∀ c. ∀ d. ∀ e. ∀ L. ∀ R. (∀ x. Lt(x,L) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(b,c,x,y) ∧ Pow(y,x,n)) → (∀ x. ∀ y. Lt(x,L) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)) → BetaAt(d,e,L,R) → (¬L = 0 → Dvd(L,g) → Pow(R,L,n)) → ∀ x. Lt(x,S L) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(d,e,x,y) ∧ Pow(y,x,n)

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

Definition DAG

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

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall n g b c d e L R. (forall ppf_table_degree_table_previous. (exists pvs_gap_table_previousbound. pvs_gap_table_previousbound + S (ppf_table_degree_table_previous) = (L)) -> ~(ppf_table_degree_table_previous = 0) -> (exists pvs_factor_table_previousdivisor. (g) = (ppf_table_degree_table_previous) * pvs_factor_table_previousdivisor) -> exists ppf_table_root_table_previous. (((exists ff_h_pvs_table_previousentry. ff_h_pvs_table_previousentry + S (ppf_table_root_table_previous) = S ((S (ppf_table_degree_table_previous)) * c)) /\ exists ff_q_pvs_table_previousentry. b = ff_q_pvs_table_previousentry * S ((S (ppf_table_degree_table_previous)) * c) + (ppf_table_root_table_previous))) /\ (exists pa_b_pvs_table_previouspower pa_c_pvs_table_previouspower. ((forall pa_i_pvs_table_previouspower_repeat. (exists pa_lt_pvs_table_previouspower_repeat_bound. pa_lt_pvs_table_previouspower_repeat_bound + S pa_i_pvs_table_previouspower_repeat = ppf_table_degree_table_previous) -> (((exists pa_h_pvs_table_previouspower_repeat_decoded. pa_h_pvs_table_previouspower_repeat_decoded + S (ppf_table_root_table_previous) = S ((S (pa_i_pvs_table_previouspower_repeat)) * pa_c_pvs_table_previouspower)) /\ exists pa_q_pvs_table_previouspower_repeat_decoded. pa_b_pvs_table_previouspower = pa_q_pvs_table_previouspower_repeat_decoded * S ((S (pa_i_pvs_table_previouspower_repeat)) * pa_c_pvs_table_previouspower) + (ppf_table_root_table_previous)))) /\ (exists pa_u_pvs_table_previouspower_product pa_v_pvs_table_previouspower_product. ((((exists pa_h_pvs_table_previouspower_product_start. pa_h_pvs_table_previouspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_previouspower_product)) /\ exists pa_q_pvs_table_previouspower_product_start. pa_u_pvs_table_previouspower_product = pa_q_pvs_table_previouspower_product_start * S ((S (0)) * pa_v_pvs_table_previouspower_product) + (1))) /\ ((((exists pa_h_pvs_table_previouspower_product_terminal. pa_h_pvs_table_previouspower_product_terminal + S (n) = S ((S (ppf_table_degree_table_previous)) * pa_v_pvs_table_previouspower_product)) /\ exists pa_q_pvs_table_previouspower_product_terminal. pa_u_pvs_table_previouspower_product = pa_q_pvs_table_previouspower_product_terminal * S ((S (ppf_table_degree_table_previous)) * pa_v_pvs_table_previouspower_product) + (n))) /\ forall pa_i_pvs_table_previouspower_product. (exists pa_lt_pvs_table_previouspower_product_bound. pa_lt_pvs_table_previouspower_product_bound + S pa_i_pvs_table_previouspower_product = ppf_table_degree_table_previous) -> exists pa_p_pvs_table_previouspower_product pa_r_pvs_table_previouspower_product pa_s_pvs_table_previouspower_product. ((((exists pa_h_pvs_table_previouspower_product_factor. pa_h_pvs_table_previouspower_product_factor + S (pa_p_pvs_table_previouspower_product) = S ((S (pa_i_pvs_table_previouspower_product)) * pa_c_pvs_table_previouspower)) /\ exists pa_q_pvs_table_previouspower_product_factor. pa_b_pvs_table_previouspower = pa_q_pvs_table_previouspower_product_factor * S ((S (pa_i_pvs_table_previouspower_product)) * pa_c_pvs_table_previouspower) + (pa_p_pvs_table_previouspower_product))) /\ ((((exists pa_h_pvs_table_previouspower_product_partial. pa_h_pvs_table_previouspower_product_partial + S (pa_r_pvs_table_previouspower_product) = S ((S (pa_i_pvs_table_previouspower_product)) * pa_v_pvs_table_previouspower_product)) /\ exists pa_q_pvs_table_previouspower_product_partial. pa_u_pvs_table_previouspower_product = pa_q_pvs_table_previouspower_product_partial * S ((S (pa_i_pvs_table_previouspower_product)) * pa_v_pvs_table_previouspower_product) + (pa_r_pvs_table_previouspower_product))) /\ ((((exists pa_h_pvs_table_previouspower_product_successor. pa_h_pvs_table_previouspower_product_successor + S (pa_s_pvs_table_previouspower_product) = S ((S (S pa_i_pvs_table_previouspower_product)) * pa_v_pvs_table_previouspower_product)) /\ exists pa_q_pvs_table_previouspower_product_successor. pa_u_pvs_table_previouspower_product = pa_q_pvs_table_previouspower_product_successor * S ((S (S pa_i_pvs_table_previouspower_product)) * pa_v_pvs_table_previouspower_product) + (pa_s_pvs_table_previouspower_product))) /\ pa_s_pvs_table_previouspower_product = pa_r_pvs_table_previouspower_product * pa_p_pvs_table_previouspower_product))))))))) -> (forall pfp_i_pvs_table_preserve pfp_a_pvs_table_preserve. (exists pfp_gap_pvs_table_preservebound. pfp_gap_pvs_table_preservebound + S (pfp_i_pvs_table_preserve) = (L)) -> (((exists ff_h_pfp_pvs_table_preserveold. ff_h_pfp_pvs_table_preserveold + S (pfp_a_pvs_table_preserve) = S ((S (pfp_i_pvs_table_preserve)) * c)) /\ exists ff_q_pfp_pvs_table_preserveold. b = ff_q_pfp_pvs_table_preserveold * S ((S (pfp_i_pvs_table_preserve)) * c) + (pfp_a_pvs_table_preserve))) -> (((exists ff_h_pfp_pvs_table_preservenew. ff_h_pfp_pvs_table_preservenew + S (pfp_a_pvs_table_preserve) = S ((S (pfp_i_pvs_table_preserve)) * e)) /\ exists ff_q_pfp_pvs_table_preservenew. d = ff_q_pfp_pvs_table_preservenew * S ((S (pfp_i_pvs_table_preserve)) * e) + (pfp_a_pvs_table_preserve)))) -> (((exists ff_h_pvs_table_last. ff_h_pvs_table_last + S (R) = S ((S (L)) * e)) /\ exists ff_q_pvs_table_last. d = ff_q_pvs_table_last * S ((S (L)) * e) + (R))) -> (~(L = 0) -> (exists pvs_factor_table_last_divisor. (g) = (L) * pvs_factor_table_last_divisor) -> (exists pa_b_pvs_table_last_power pa_c_pvs_table_last_power. ((forall pa_i_pvs_table_last_power_repeat. (exists pa_lt_pvs_table_last_power_repeat_bound. pa_lt_pvs_table_last_power_repeat_bound + S pa_i_pvs_table_last_power_repeat = L) -> (((exists pa_h_pvs_table_last_power_repeat_decoded. pa_h_pvs_table_last_power_repeat_decoded + S (R) = S ((S (pa_i_pvs_table_last_power_repeat)) * pa_c_pvs_table_last_power)) /\ exists pa_q_pvs_table_last_power_repeat_decoded. pa_b_pvs_table_last_power = pa_q_pvs_table_last_power_repeat_decoded * S ((S (pa_i_pvs_table_last_power_repeat)) * pa_c_pvs_table_last_power) + (R)))) /\ (exists pa_u_pvs_table_last_power_product pa_v_pvs_table_last_power_product. ((((exists pa_h_pvs_table_last_power_product_start. pa_h_pvs_table_last_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_last_power_product)) /\ exists pa_q_pvs_table_last_power_product_start. pa_u_pvs_table_last_power_product = pa_q_pvs_table_last_power_product_start * S ((S (0)) * pa_v_pvs_table_last_power_product) + (1))) /\ ((((exists pa_h_pvs_table_last_power_product_terminal. pa_h_pvs_table_last_power_product_terminal + S (n) = S ((S (L)) * pa_v_pvs_table_last_power_product)) /\ exists pa_q_pvs_table_last_power_product_terminal. pa_u_pvs_table_last_power_product = pa_q_pvs_table_last_power_product_terminal * S ((S (L)) * pa_v_pvs_table_last_power_product) + (n))) /\ forall pa_i_pvs_table_last_power_product. (exists pa_lt_pvs_table_last_power_product_bound. pa_lt_pvs_table_last_power_product_bound + S pa_i_pvs_table_last_power_product = L) -> exists pa_p_pvs_table_last_power_product pa_r_pvs_table_last_power_product pa_s_pvs_table_last_power_product. ((((exists pa_h_pvs_table_last_power_product_factor. pa_h_pvs_table_last_power_product_factor + S (pa_p_pvs_table_last_power_product) = S ((S (pa_i_pvs_table_last_power_product)) * pa_c_pvs_table_last_power)) /\ exists pa_q_pvs_table_last_power_product_factor. pa_b_pvs_table_last_power = pa_q_pvs_table_last_power_product_factor * S ((S (pa_i_pvs_table_last_power_product)) * pa_c_pvs_table_last_power) + (pa_p_pvs_table_last_power_product))) /\ ((((exists pa_h_pvs_table_last_power_product_partial. pa_h_pvs_table_last_power_product_partial + S (pa_r_pvs_table_last_power_product) = S ((S (pa_i_pvs_table_last_power_product)) * pa_v_pvs_table_last_power_product)) /\ exists pa_q_pvs_table_last_power_product_partial. pa_u_pvs_table_last_power_product = pa_q_pvs_table_last_power_product_partial * S ((S (pa_i_pvs_table_last_power_product)) * pa_v_pvs_table_last_power_product) + (pa_r_pvs_table_last_power_product))) /\ ((((exists pa_h_pvs_table_last_power_product_successor. pa_h_pvs_table_last_power_product_successor + S (pa_s_pvs_table_last_power_product) = S ((S (S pa_i_pvs_table_last_power_product)) * pa_v_pvs_table_last_power_product)) /\ exists pa_q_pvs_table_last_power_product_successor. pa_u_pvs_table_last_power_product = pa_q_pvs_table_last_power_product_successor * S ((S (S pa_i_pvs_table_last_power_product)) * pa_v_pvs_table_last_power_product) + (pa_s_pvs_table_last_power_product))) /\ pa_s_pvs_table_last_power_product = pa_r_pvs_table_last_power_product * pa_p_pvs_table_last_power_product))))))))) -> (forall ppf_table_degree_table_next. (exists pvs_gap_table_nextbound. pvs_gap_table_nextbound + S (ppf_table_degree_table_next) = (S L)) -> ~(ppf_table_degree_table_next = 0) -> (exists pvs_factor_table_nextdivisor. (g) = (ppf_table_degree_table_next) * pvs_factor_table_nextdivisor) -> exists ppf_table_root_table_next. (((exists ff_h_pvs_table_nextentry. ff_h_pvs_table_nextentry + S (ppf_table_root_table_next) = S ((S (ppf_table_degree_table_next)) * e)) /\ exists ff_q_pvs_table_nextentry. d = ff_q_pvs_table_nextentry * S ((S (ppf_table_degree_table_next)) * e) + (ppf_table_root_table_next))) /\ (exists pa_b_pvs_table_nextpower pa_c_pvs_table_nextpower. ((forall pa_i_pvs_table_nextpower_repeat. (exists pa_lt_pvs_table_nextpower_repeat_bound. pa_lt_pvs_table_nextpower_repeat_bound + S pa_i_pvs_table_nextpower_repeat = ppf_table_degree_table_next) -> (((exists pa_h_pvs_table_nextpower_repeat_decoded. pa_h_pvs_table_nextpower_repeat_decoded + S (ppf_table_root_table_next) = S ((S (pa_i_pvs_table_nextpower_repeat)) * pa_c_pvs_table_nextpower)) /\ exists pa_q_pvs_table_nextpower_repeat_decoded. pa_b_pvs_table_nextpower = pa_q_pvs_table_nextpower_repeat_decoded * S ((S (pa_i_pvs_table_nextpower_repeat)) * pa_c_pvs_table_nextpower) + (ppf_table_root_table_next)))) /\ (exists pa_u_pvs_table_nextpower_product pa_v_pvs_table_nextpower_product. ((((exists pa_h_pvs_table_nextpower_product_start. pa_h_pvs_table_nextpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_nextpower_product)) /\ exists pa_q_pvs_table_nextpower_product_start. pa_u_pvs_table_nextpower_product = pa_q_pvs_table_nextpower_product_start * S ((S (0)) * pa_v_pvs_table_nextpower_product) + (1))) /\ ((((exists pa_h_pvs_table_nextpower_product_terminal. pa_h_pvs_table_nextpower_product_terminal + S (n) = S ((S (ppf_table_degree_table_next)) * pa_v_pvs_table_nextpower_product)) /\ exists pa_q_pvs_table_nextpower_product_terminal. pa_u_pvs_table_nextpower_product = pa_q_pvs_table_nextpower_product_terminal * S ((S (ppf_table_degree_table_next)) * pa_v_pvs_table_nextpower_product) + (n))) /\ forall pa_i_pvs_table_nextpower_product. (exists pa_lt_pvs_table_nextpower_product_bound. pa_lt_pvs_table_nextpower_product_bound + S pa_i_pvs_table_nextpower_product = ppf_table_degree_table_next) -> exists pa_p_pvs_table_nextpower_product pa_r_pvs_table_nextpower_product pa_s_pvs_table_nextpower_product. ((((exists pa_h_pvs_table_nextpower_product_factor. pa_h_pvs_table_nextpower_product_factor + S (pa_p_pvs_table_nextpower_product) = S ((S (pa_i_pvs_table_nextpower_product)) * pa_c_pvs_table_nextpower)) /\ exists pa_q_pvs_table_nextpower_product_factor. pa_b_pvs_table_nextpower = pa_q_pvs_table_nextpower_product_factor * S ((S (pa_i_pvs_table_nextpower_product)) * pa_c_pvs_table_nextpower) + (pa_p_pvs_table_nextpower_product))) /\ ((((exists pa_h_pvs_table_nextpower_product_partial. pa_h_pvs_table_nextpower_product_partial + S (pa_r_pvs_table_nextpower_product) = S ((S (pa_i_pvs_table_nextpower_product)) * pa_v_pvs_table_nextpower_product)) /\ exists pa_q_pvs_table_nextpower_product_partial. pa_u_pvs_table_nextpower_product = pa_q_pvs_table_nextpower_product_partial * S ((S (pa_i_pvs_table_nextpower_product)) * pa_v_pvs_table_nextpower_product) + (pa_r_pvs_table_nextpower_product))) /\ ((((exists pa_h_pvs_table_nextpower_product_successor. pa_h_pvs_table_nextpower_product_successor + S (pa_s_pvs_table_nextpower_product) = S ((S (S pa_i_pvs_table_nextpower_product)) * pa_v_pvs_table_nextpower_product)) /\ exists pa_q_pvs_table_nextpower_product_successor. pa_u_pvs_table_nextpower_product = pa_q_pvs_table_nextpower_product_successor * S ((S (S pa_i_pvs_table_nextpower_product)) * pa_v_pvs_table_nextpower_product) + (pa_s_pvs_table_nextpower_product))) /\ pa_s_pvs_table_nextpower_product = pa_r_pvs_table_nextpower_product * pa_p_pvs_table_nextpower_product)))))))))

Complete tactic proof in conservative notation

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

55 script commands · 21 reading checkpoints · 2 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–10

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

  1. L1
    intro n
  2. L2
    intro g
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro L
  8. L8
    intro R
  9. L9
    intro hprevious
  10. L10
    intro hpreserve
02Fix variables and assumptionsL11–16

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

  1. L11
    intro hlast
  2. L12
    intro hroot
  3. L13
    intro k
  4. L14
    intro hkbound
  5. L15
    intro hk
  6. L16
    intro hdiv
03Establish hcaseL17–21

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

  1. L17
    have hcase : k = L ∨ Lt(k,L)Definitions: Lt(k,L)Original native command in the exact edition
  2. L18
    specialize finite_lt_succ_eq_or_lt (L)
  3. L19
    specialize finite_lt_succ_eq_or_lt (k)
  4. L20
    apply finite_lt_succ_eq_or_lt
  5. L21
    exact hkbound
04Separate the logical casesL22–22

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

  1. L22
    cases hcase
05Construct an explicit witnessL23–23

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

  1. L23
    exists R
06Separate the logical casesL24–24

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

  1. L24
    split
07Calculate and transport equalitiesL25–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    rewrite hcase_left
  2. L26
    rewrite hcase_left
08Use earlier factsL27–27

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

  1. L27
    exact hlast
09Calculate and transport equalitiesL28–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L28
    rewrite hcase_left
  2. L29
    rewrite hcase_left
  3. L30
    rewrite hcase_left
  4. L31
    rewrite hcase_left
10Use earlier factsL32–32

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

  1. L32
    apply hroot
11Fix variables and assumptionsL33–33

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

  1. L33
    intro hLzero
12Use earlier factsL34–34

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

  1. L34
    apply hk
13Calculate and transport equalitiesL35–35

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L35
    trans L
14Use earlier factsL36–37

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

  1. L36
    exact hcase_left
  2. L37
    exact hLzero
15Calculate and transport equalitiesL38–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L38
    rewrite hcase_left at hdiv
16Use earlier factsL39–39

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

  1. L39
    exact hdiv
17Establish hentryL40–45

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

  1. L40
    have hentry : ∃ r. BetaAt(b,c,k,r) ∧ Pow(r,k,n)Definitions: BetaAt(b,c,k,r)Pow(r,k,n)Original native command in the exact edition
  2. L41
    specialize hprevious (k)
  3. L42
    apply hprevious
  4. L43
    exact hcase_right
  5. L44
    exact hk
  6. L45
    exact hdiv
18Separate the logical casesL46–47

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

  1. L46
    cases hentry
  2. L47
    cases hentry_witness
19Construct an explicit witnessL48–48

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

  1. L48
    exists x
20Separate the logical casesL49–49

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

  1. L49
    split
21Use earlier factsL50–55

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

  1. L50
    specialize hpreserve (k)
  2. L51
    specialize hpreserve (x)
  3. L52
    apply hpreserve
  4. L53
    exact hcase_right
  5. L54
    exact hentry_witness_left
  6. L55
    exact hentry_witness_right

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro n
  2. 0002intro g
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro L
  8. 0008intro R
  9. 0009intro hprevious
  10. 0010intro hpreserve
  11. 0011intro hlast
  12. 0012intro hroot
  13. 0013intro k
  14. 0014intro hkbound
  15. 0015intro hk
  16. 0016intro hdiv
  17. 0017have hcase : k = L ∨ Lt(k,L)
  18. 0018specialize finite_lt_succ_eq_or_lt (L)
  19. 0019specialize finite_lt_succ_eq_or_lt (k)
  20. 0020apply finite_lt_succ_eq_or_lt
  21. 0021exact hkbound
  22. 0022cases hcase
  23. 0023exists R
  24. 0024split
  25. 0025rewrite hcase_left
  26. 0026rewrite hcase_left
  27. 0027exact hlast
  28. 0028rewrite hcase_left
  29. 0029rewrite hcase_left
  30. 0030rewrite hcase_left
  31. 0031rewrite hcase_left
  32. 0032apply hroot
  33. 0033intro hLzero
  34. 0034apply hk
  35. 0035trans L
  36. 0036exact hcase_left
  37. 0037exact hLzero
  38. 0038rewrite hcase_left at hdiv
  39. 0039exact hdiv
  40. 0040have hentry : ∃ r. BetaAt(b,c,k,r) ∧ Pow(r,k,n)
  41. 0041specialize hprevious (k)
  42. 0042apply hprevious
  43. 0043exact hcase_right
  44. 0044exact hk
  45. 0045exact hdiv
  46. 0046cases hentry
  47. 0047cases hentry_witness
  48. 0048exists x
  49. 0049split
  50. 0050specialize hpreserve (k)
  51. 0051specialize hpreserve (x)
  52. 0052apply hpreserve
  53. 0053exact hcase_right
  54. 0054exact hentry_witness_left
  55. 0055exact hentry_witness_right