SK0020

prime_exponent_prefix_gcd_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 37 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

SK001E prime_exponent_prefix_gcd_empty beta_at_exists Stable theorem; checked-use authorized canonical_gcd_exists Alpha theorem; checked-use authorized SK001F prime_exponent_prefix_gcd_successor

Direct dependents

SK002F perfect_power_profile_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (2)
prime exponent prefix gcd emptyprime exponent prefix gcd successor

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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 : exists v. (((exists ff_h_pvs_gcd_terminal. ff_h_pvs_gcd_terminal + S (v) = S ((S (l)) * c)) /\ exists ff_q_pvs_gcd_terminal. b = ff_q_pvs_gcd_terminal * S ((S (l)) * c) + (v)))
  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
  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 exact 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 : exists g. (((forall ppf_index_gcd_previouscommon ppf_entry_gcd_previouscommon. (exists pvs_gap_gcd_previouscommonbound. pvs_gap_gcd_previouscommonbound + S (ppf_index_gcd_previouscommon) = (l)) -> (((exists ff_h_pvs_gcd_previouscommonentry. ff_h_pvs_gcd_previouscommonentry + S (ppf_entry_gcd_previouscommon) = S ((S (ppf_index_gcd_previouscommon)) * c)) /\ exists ff_q_pvs_gcd_previouscommonentry. b = ff_q_pvs_gcd_previouscommonentry * S ((S (ppf_index_gcd_previouscommon)) * c) + (ppf_entry_gcd_previouscommon))) -> (exists pvs_factor_gcd_previouscommondivisor. (ppf_entry_gcd_previouscommon) = (g) * pvs_factor_gcd_previouscommondivisor)) /\ (forall ppf_common_gcd_previous. (forall ppf_index_gcd_previousother ppf_entry_gcd_previousother. (exists pvs_gap_gcd_previousotherbound. pvs_gap_gcd_previousotherbound + S (ppf_index_gcd_previousother) = (l)) -> (((exists ff_h_pvs_gcd_previousotherentry. ff_h_pvs_gcd_previousotherentry + S (ppf_entry_gcd_previousother) = S ((S (ppf_index_gcd_previousother)) * c)) /\ exists ff_q_pvs_gcd_previousotherentry. b = ff_q_pvs_gcd_previousotherentry * S ((S (ppf_index_gcd_previousother)) * c) + (ppf_entry_gcd_previousother))) -> (exists pvs_factor_gcd_previousotherdivisor. (ppf_entry_gcd_previousother) = (ppf_common_gcd_previous) * pvs_factor_gcd_previousotherdivisor)) -> (exists pvs_factor_gcd_previousgreatest. (g) = (ppf_common_gcd_previous) * pvs_factor_gcd_previousgreatest))))
  12. 0012specialize IH (b)
  13. 0013specialize IH (c)
  14. 0014apply IH
  15. 0015cases hprev
  16. 0016have hlast : exists v. (((exists ff_h_pvs_gcd_terminal. ff_h_pvs_gcd_terminal + S (v) = S ((S (l)) * c)) /\ exists ff_q_pvs_gcd_terminal. b = ff_q_pvs_gcd_terminal * S ((S (l)) * c) + (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 : exists h. ((((exists hag_left_factor_ppf_gcd_construct. x = h * hag_left_factor_ppf_gcd_construct) /\ (exists hag_right_factor_ppf_gcd_construct. x1 = h * hag_right_factor_ppf_gcd_construct)) /\ forall hag_divisor_ppf_gcd_construct. (exists hag_common_left_ppf_gcd_construct. x = hag_divisor_ppf_gcd_construct * hag_common_left_ppf_gcd_construct) -> (exists hag_common_right_ppf_gcd_construct. x1 = hag_divisor_ppf_gcd_construct * hag_common_right_ppf_gcd_construct) -> exists hag_greatest_factor_ppf_gcd_construct. h = hag_divisor_ppf_gcd_construct * hag_greatest_factor_ppf_gcd_construct))
  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