SK001F

prime_exponent_prefix_gcd_successor

The canonical gcd of the old actual prefix gcd and final decoded exponent is the gcd of the successor 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

∀ b. ∀ c. ∀ l. ∀ g. ∀ v. ∀ h. PrimeExponentPrefixGCD(b,c,l,g) → BetaAt(b,c,l,v) → Dvd(h,g) ∧ Dvd(h,v) ∧ (∀ x. Dvd(x,g) → Dvd(x,v) → Dvd(x,h)) → PrimeExponentPrefixGCD(b,c,S l,h)

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

Definition DAG

PrimeExponentPrefixGCD(b,c,l,g) · 2Dvd(d,n) · 5BetaAt(b,c,i,x) · 1

Actual proof prerequisites

is_gcd_dvd_left · checked external prerequisiteis_gcd_dvd_right · checked external prerequisiteprime_exponent_common_divisor_factorprime_exponent_common_divisor_successoris_gcd_greatest · checked external prerequisiteprime_exponent_common_divisor_drople_refl · checked external prerequisite
Original expanded first-order statement 
forall b c l g v h. (((forall ppf_index_gcd_prefixcommon ppf_entry_gcd_prefixcommon. (exists pvs_gap_gcd_prefixcommonbound. pvs_gap_gcd_prefixcommonbound + S (ppf_index_gcd_prefixcommon) = (l)) -> (((exists ff_h_pvs_gcd_prefixcommonentry. ff_h_pvs_gcd_prefixcommonentry + S (ppf_entry_gcd_prefixcommon) = S ((S (ppf_index_gcd_prefixcommon)) * c)) /\ exists ff_q_pvs_gcd_prefixcommonentry. b = ff_q_pvs_gcd_prefixcommonentry * S ((S (ppf_index_gcd_prefixcommon)) * c) + (ppf_entry_gcd_prefixcommon))) -> (exists pvs_factor_gcd_prefixcommondivisor. (ppf_entry_gcd_prefixcommon) = (g) * pvs_factor_gcd_prefixcommondivisor)) /\ (forall ppf_common_gcd_prefix. (forall ppf_index_gcd_prefixother ppf_entry_gcd_prefixother. (exists pvs_gap_gcd_prefixotherbound. pvs_gap_gcd_prefixotherbound + S (ppf_index_gcd_prefixother) = (l)) -> (((exists ff_h_pvs_gcd_prefixotherentry. ff_h_pvs_gcd_prefixotherentry + S (ppf_entry_gcd_prefixother) = S ((S (ppf_index_gcd_prefixother)) * c)) /\ exists ff_q_pvs_gcd_prefixotherentry. b = ff_q_pvs_gcd_prefixotherentry * S ((S (ppf_index_gcd_prefixother)) * c) + (ppf_entry_gcd_prefixother))) -> (exists pvs_factor_gcd_prefixotherdivisor. (ppf_entry_gcd_prefixother) = (ppf_common_gcd_prefix) * pvs_factor_gcd_prefixotherdivisor)) -> (exists pvs_factor_gcd_prefixgreatest. (g) = (ppf_common_gcd_prefix) * pvs_factor_gcd_prefixgreatest)))) -> (((exists ff_h_pvs_gcd_last. ff_h_pvs_gcd_last + S (v) = S ((S (l)) * c)) /\ exists ff_q_pvs_gcd_last. b = ff_q_pvs_gcd_last * S ((S (l)) * c) + (v))) -> ((((exists hag_left_factor_ppf_gcd_merge. g = h * hag_left_factor_ppf_gcd_merge) /\ (exists hag_right_factor_ppf_gcd_merge. v = h * hag_right_factor_ppf_gcd_merge)) /\ forall hag_divisor_ppf_gcd_merge. (exists hag_common_left_ppf_gcd_merge. g = hag_divisor_ppf_gcd_merge * hag_common_left_ppf_gcd_merge) -> (exists hag_common_right_ppf_gcd_merge. v = hag_divisor_ppf_gcd_merge * hag_common_right_ppf_gcd_merge) -> exists hag_greatest_factor_ppf_gcd_merge. h = hag_divisor_ppf_gcd_merge * hag_greatest_factor_ppf_gcd_merge)) -> (((forall ppf_index_gcd_successorcommon ppf_entry_gcd_successorcommon. (exists pvs_gap_gcd_successorcommonbound. pvs_gap_gcd_successorcommonbound + S (ppf_index_gcd_successorcommon) = (S l)) -> (((exists ff_h_pvs_gcd_successorcommonentry. ff_h_pvs_gcd_successorcommonentry + S (ppf_entry_gcd_successorcommon) = S ((S (ppf_index_gcd_successorcommon)) * c)) /\ exists ff_q_pvs_gcd_successorcommonentry. b = ff_q_pvs_gcd_successorcommonentry * S ((S (ppf_index_gcd_successorcommon)) * c) + (ppf_entry_gcd_successorcommon))) -> (exists pvs_factor_gcd_successorcommondivisor. (ppf_entry_gcd_successorcommon) = (h) * pvs_factor_gcd_successorcommondivisor)) /\ (forall ppf_common_gcd_successor. (forall ppf_index_gcd_successorother ppf_entry_gcd_successorother. (exists pvs_gap_gcd_successorotherbound. pvs_gap_gcd_successorotherbound + S (ppf_index_gcd_successorother) = (S l)) -> (((exists ff_h_pvs_gcd_successorotherentry. ff_h_pvs_gcd_successorotherentry + S (ppf_entry_gcd_successorother) = S ((S (ppf_index_gcd_successorother)) * c)) /\ exists ff_q_pvs_gcd_successorotherentry. b = ff_q_pvs_gcd_successorotherentry * S ((S (ppf_index_gcd_successorother)) * c) + (ppf_entry_gcd_successorother))) -> (exists pvs_factor_gcd_successorotherdivisor. (ppf_entry_gcd_successorother) = (ppf_common_gcd_successor) * pvs_factor_gcd_successorotherdivisor)) -> (exists pvs_factor_gcd_successorgreatest. (h) = (ppf_common_gcd_successor) * pvs_factor_gcd_successorgreatest))))

Complete tactic proof in conservative notation

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

57 script commands · 8 reading checkpoints · 0 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 (3)
prime exponent common divisor successorprime exponent common divisor factorprime exponent common divisor drop
01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro g
  5. L5
    intro v
  6. L6
    intro h
  7. L7
    intro hprefix
  8. L8
    intro hlast
  9. L9
    intro hmerge
02Separate the logical casesL10–11

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

  1. L10
    cases hprefix
  2. L11
    split
03Use earlier factsL12–21

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

  1. L12
    specialize prime_exponent_common_divisor_successor (b)
  2. L13
    specialize prime_exponent_common_divisor_successor (c)
  3. L14
    specialize prime_exponent_common_divisor_successor (l)
  4. L15
    specialize prime_exponent_common_divisor_successor (h)
  5. L16
    specialize prime_exponent_common_divisor_successor (v)
  6. L17
    apply prime_exponent_common_divisor_successor
  7. L18
    specialize prime_exponent_common_divisor_factor (b)
  8. L19
    specialize prime_exponent_common_divisor_factor (c)
  9. L20
    specialize prime_exponent_common_divisor_factor (l)
  10. L21
    specialize prime_exponent_common_divisor_factor (g)
04Use earlier factsL22–31

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

  1. L22
    specialize prime_exponent_common_divisor_factor (h)
  2. L23
    apply prime_exponent_common_divisor_factor
  3. L24
    exact hprefix_left
  4. L25
    specialize is_gcd_dvd_left (h)
  5. L26
    specialize is_gcd_dvd_left (g)
  6. L27
    specialize is_gcd_dvd_left (v)
  7. L28
    apply is_gcd_dvd_left
  8. L29
    exact hmerge
  9. L30
    exact hlast
  10. L31
    specialize is_gcd_dvd_right (h)
05Use earlier factsL32–35

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

  1. L32
    specialize is_gcd_dvd_right (g)
  2. L33
    specialize is_gcd_dvd_right (v)
  3. L34
    apply is_gcd_dvd_right
  4. L35
    exact hmerge
06Fix variables and assumptionsL36–37

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

  1. L36
    intro d
  2. L37
    intro hcommon
07Use earlier factsL38–47

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

  1. L38
    specialize is_gcd_greatest (h)
  2. L39
    specialize is_gcd_greatest (g)
  3. L40
    specialize is_gcd_greatest (v)
  4. L41
    specialize is_gcd_greatest (d)
  5. L42
    apply is_gcd_greatest
  6. L43
    exact hmerge
  7. L44
    specialize hprefix_right (d)
  8. L45
    apply hprefix_right
  9. L46
    specialize prime_exponent_common_divisor_drop (b)
  10. L47
    specialize prime_exponent_common_divisor_drop (c)
08Use earlier factsL48–57

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

  1. L48
    specialize prime_exponent_common_divisor_drop (l)
  2. L49
    specialize prime_exponent_common_divisor_drop (d)
  3. L50
    apply prime_exponent_common_divisor_drop
  4. L51
    exact hcommon
  5. L52
    specialize hcommon (l)
  6. L53
    specialize hcommon (v)
  7. L54
    apply hcommon
  8. L55
    specialize le_refl (S l)
  9. L56
    apply le_refl
  10. L57
    exact hlast

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro g
  5. 0005intro v
  6. 0006intro h
  7. 0007intro hprefix
  8. 0008intro hlast
  9. 0009intro hmerge
  10. 0010cases hprefix
  11. 0011split
  12. 0012specialize prime_exponent_common_divisor_successor (b)
  13. 0013specialize prime_exponent_common_divisor_successor (c)
  14. 0014specialize prime_exponent_common_divisor_successor (l)
  15. 0015specialize prime_exponent_common_divisor_successor (h)
  16. 0016specialize prime_exponent_common_divisor_successor (v)
  17. 0017apply prime_exponent_common_divisor_successor
  18. 0018specialize prime_exponent_common_divisor_factor (b)
  19. 0019specialize prime_exponent_common_divisor_factor (c)
  20. 0020specialize prime_exponent_common_divisor_factor (l)
  21. 0021specialize prime_exponent_common_divisor_factor (g)
  22. 0022specialize prime_exponent_common_divisor_factor (h)
  23. 0023apply prime_exponent_common_divisor_factor
  24. 0024exact hprefix_left
  25. 0025specialize is_gcd_dvd_left (h)
  26. 0026specialize is_gcd_dvd_left (g)
  27. 0027specialize is_gcd_dvd_left (v)
  28. 0028apply is_gcd_dvd_left
  29. 0029exact hmerge
  30. 0030exact hlast
  31. 0031specialize is_gcd_dvd_right (h)
  32. 0032specialize is_gcd_dvd_right (g)
  33. 0033specialize is_gcd_dvd_right (v)
  34. 0034apply is_gcd_dvd_right
  35. 0035exact hmerge
  36. 0036intro d
  37. 0037intro hcommon
  38. 0038specialize is_gcd_greatest (h)
  39. 0039specialize is_gcd_greatest (g)
  40. 0040specialize is_gcd_greatest (v)
  41. 0041specialize is_gcd_greatest (d)
  42. 0042apply is_gcd_greatest
  43. 0043exact hmerge
  44. 0044specialize hprefix_right (d)
  45. 0045apply hprefix_right
  46. 0046specialize prime_exponent_common_divisor_drop (b)
  47. 0047specialize prime_exponent_common_divisor_drop (c)
  48. 0048specialize prime_exponent_common_divisor_drop (l)
  49. 0049specialize prime_exponent_common_divisor_drop (d)
  50. 0050apply prime_exponent_common_divisor_drop
  51. 0051exact hcommon
  52. 0052specialize hcommon (l)
  53. 0053specialize hcommon (v)
  54. 0054apply hcommon
  55. 0055specialize le_refl (S l)
  56. 0056apply le_refl
  57. 0057exact hlast