SK0020

prime_exponent_prefix_gcd_exists

Ordinary finite induction constructs a genuine gcd of every actual beta prefix, including empty and zero-entry prefixes.

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. ∀ b. ∀ c. ∃ g. PrimeExponentPrefixGCD(b,c,l,g)

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

prime_exponent_prefix_gcd_emptybeta_at_exists · checked external prerequisitecanonical_gcd_exists · checked external prerequisiteprime_exponent_prefix_gcd_successor
Original expanded first-order statement 
forall l b c. exists g. (((forall ppf_index_gcd_existscommon ppf_entry_gcd_existscommon. (exists pvs_gap_gcd_existscommonbound. pvs_gap_gcd_existscommonbound + S (ppf_index_gcd_existscommon) = (l)) -> (((exists ff_h_pvs_gcd_existscommonentry. ff_h_pvs_gcd_existscommonentry + S (ppf_entry_gcd_existscommon) = S ((S (ppf_index_gcd_existscommon)) * c)) /\ exists ff_q_pvs_gcd_existscommonentry. b = ff_q_pvs_gcd_existscommonentry * S ((S (ppf_index_gcd_existscommon)) * c) + (ppf_entry_gcd_existscommon))) -> (exists pvs_factor_gcd_existscommondivisor. (ppf_entry_gcd_existscommon) = (g) * pvs_factor_gcd_existscommondivisor)) /\ (forall ppf_common_gcd_exists. (forall ppf_index_gcd_existsother ppf_entry_gcd_existsother. (exists pvs_gap_gcd_existsotherbound. pvs_gap_gcd_existsotherbound + S (ppf_index_gcd_existsother) = (l)) -> (((exists ff_h_pvs_gcd_existsotherentry. ff_h_pvs_gcd_existsotherentry + S (ppf_entry_gcd_existsother) = S ((S (ppf_index_gcd_existsother)) * c)) /\ exists ff_q_pvs_gcd_existsotherentry. b = ff_q_pvs_gcd_existsotherentry * S ((S (ppf_index_gcd_existsother)) * c) + (ppf_entry_gcd_existsother))) -> (exists pvs_factor_gcd_existsotherdivisor. (ppf_entry_gcd_existsother) = (ppf_common_gcd_exists) * pvs_factor_gcd_existsotherdivisor)) -> (exists pvs_factor_gcd_existsgreatest. (g) = (ppf_common_gcd_exists) * pvs_factor_gcd_existsgreatest))))

Complete tactic proof in conservative notation

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

37 script commands · 13 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)
prime exponent prefix gcd emptyprime exponent prefix gcd successor
01Fix variables and assumptionsL1–1

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

  1. L1
    intro l
02Induction on lL2–4

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 b
  3. L4
    intro c
03Construct an explicit witnessL5–5

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

  1. L5
    exists 0
04Use earlier factsL6–8

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

  1. L6
    specialize prime_exponent_prefix_gcd_empty (b)
  2. L7
    specialize prime_exponent_prefix_gcd_empty (c)
  3. L8
    apply prime_exponent_prefix_gcd_empty
05Fix variables and assumptionsL9–10

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

  1. L9
    intro b
  2. L10
    intro c
06Establish hprevL11–14

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

  1. L11
    have hprev : ∃ g. PrimeExponentPrefixGCD(b,c,l,g)Definitions: PrimeExponentPrefixGCD(b,c,l,g)Original native command in the exact edition
  2. L12
    specialize IH (b)
  3. L13
    specialize IH (c)
  4. L14
    apply IH
07Separate the logical casesL15–15

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

  1. L15
    cases hprev
08Establish hlastL16–20

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

  1. L16
    have hlast : ∃ v. BetaAt(b,c,l,v)Definitions: BetaAt(b,c,l,v)Original native command in the exact edition
  2. L17
    specialize beta_at_exists (b)
  3. L18
    specialize beta_at_exists (c)
  4. L19
    specialize beta_at_exists (l)
  5. L20
    apply beta_at_exists
09Separate the logical casesL21–21

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

  1. L21
    cases hlast
10Establish hmergeL22–25

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

  1. L22
    have hmerge : ∃ h. Dvd(h,x) ∧ Dvd(h,x1) ∧ (∀ y. Dvd(y,x) → Dvd(y,x1) → Dvd(y,h))Definitions: Dvd(h,x)Dvd(h,x1)Dvd(y,x)Dvd(y,x1)Dvd(y,h)Original native command in the exact edition
  2. L23
    specialize canonical_gcd_exists (x)
  3. L24
    specialize canonical_gcd_exists (x1)
  4. L25
    apply canonical_gcd_exists
11Separate the logical casesL26–26

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

  1. L26
    cases hmerge
12Construct an explicit witnessL27–27

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

  1. L27
    exists x2
13Use earlier factsL28–37

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

  1. L28
    specialize prime_exponent_prefix_gcd_successor (b)
  2. L29
    specialize prime_exponent_prefix_gcd_successor (c)
  3. L30
    specialize prime_exponent_prefix_gcd_successor (l)
  4. L31
    specialize prime_exponent_prefix_gcd_successor (x)
  5. L32
    specialize prime_exponent_prefix_gcd_successor (x1)
  6. L33
    specialize prime_exponent_prefix_gcd_successor (x2)
  7. L34
    apply prime_exponent_prefix_gcd_successor
  8. L35
    exact hprev_witness
  9. L36
    exact hlast_witness
  10. L37
    exact hmerge_witness

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro l
  2. 0002induction l
  3. 0003intro b
  4. 0004intro c
  5. 0005exists 0
  6. 0006specialize prime_exponent_prefix_gcd_empty (b)
  7. 0007specialize prime_exponent_prefix_gcd_empty (c)
  8. 0008apply prime_exponent_prefix_gcd_empty
  9. 0009intro b
  10. 0010intro c
  11. 0011have hprev : ∃ g. PrimeExponentPrefixGCD(b,c,l,g)
  12. 0012specialize IH (b)
  13. 0013specialize IH (c)
  14. 0014apply IH
  15. 0015cases hprev
  16. 0016have hlast : ∃ v. BetaAt(b,c,l,v)
  17. 0017specialize beta_at_exists (b)
  18. 0018specialize beta_at_exists (c)
  19. 0019specialize beta_at_exists (l)
  20. 0020apply beta_at_exists
  21. 0021cases hlast
  22. 0022have hmerge : ∃ h. Dvd(h,x) ∧ Dvd(h,x1) ∧ (∀ y. Dvd(y,x) → Dvd(y,x1) → Dvd(y,h))
  23. 0023specialize canonical_gcd_exists (x)
  24. 0024specialize canonical_gcd_exists (x1)
  25. 0025apply canonical_gcd_exists
  26. 0026cases hmerge
  27. 0027exists x2
  28. 0028specialize prime_exponent_prefix_gcd_successor (b)
  29. 0029specialize prime_exponent_prefix_gcd_successor (c)
  30. 0030specialize prime_exponent_prefix_gcd_successor (l)
  31. 0031specialize prime_exponent_prefix_gcd_successor (x)
  32. 0032specialize prime_exponent_prefix_gcd_successor (x1)
  33. 0033specialize prime_exponent_prefix_gcd_successor (x2)
  34. 0034apply prime_exponent_prefix_gcd_successor
  35. 0035exact hprev_witness
  36. 0036exact hlast_witness
  37. 0037exact hmerge_witness