SK001D

prime_exponent_common_divisor_factor

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

Every divisor of a common divisor is an actual common divisor of the same finite exponent list.

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 b c l g d. (forall ppf_index_common_multiple ppf_entry_common_multiple. (exists pvs_gap_common_multiplebound. pvs_gap_common_multiplebound + S (ppf_index_common_multiple) = (l)) -> (((exists ff_h_pvs_common_multipleentry. ff_h_pvs_common_multipleentry + S (ppf_entry_common_multiple) = S ((S (ppf_index_common_multiple)) * c)) /\ exists ff_q_pvs_common_multipleentry. b = ff_q_pvs_common_multipleentry * S ((S (ppf_index_common_multiple)) * c) + (ppf_entry_common_multiple))) -> (exists pvs_factor_common_multipledivisor. (ppf_entry_common_multiple) = (g) * pvs_factor_common_multipledivisor)) -> (exists pvs_factor_common_factor. (g) = (d) * pvs_factor_common_factor) -> (forall ppf_index_common_factored ppf_entry_common_factored. (exists pvs_gap_common_factoredbound. pvs_gap_common_factoredbound + S (ppf_index_common_factored) = (l)) -> (((exists ff_h_pvs_common_factoredentry. ff_h_pvs_common_factoredentry + S (ppf_entry_common_factored) = S ((S (ppf_index_common_factored)) * c)) /\ exists ff_q_pvs_common_factoredentry. b = ff_q_pvs_common_factoredentry * S ((S (ppf_index_common_factored)) * c) + (ppf_entry_common_factored))) -> (exists pvs_factor_common_factoreddivisor. (ppf_entry_common_factored) = (d) * pvs_factor_common_factoreddivisor))

Constructive proof overview

Generated structural guide

Every divisor of a common divisor is an actual common divisor of the same finite exponent list.

The unchanged tactic script uses 1 declared prerequisite and contains 21 exact native proof lines.

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

Proof neighborhood

Direct dependencies

multiple_trans Stable theorem; checked-use authorized

Direct dependents

SK001F prime_exponent_prefix_gcd_successor SK0027 prime_support_exponent_gcd_divisor_criterion

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

21 script commands · 3 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.

01Fix variables and assumptionsL1–10

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 d
  6. L6
    intro hcommon
  7. L7
    intro hdiv
  8. L8
    intro i
  9. L9
    intro e
  10. L10
    intro hi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hat
03Use earlier factsL12–21

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

  1. L12
    specialize multiple_trans (g)
  2. L13
    specialize multiple_trans (d)
  3. L14
    specialize multiple_trans (e)
  4. L15
    apply multiple_trans
  5. L16
    specialize hcommon (i)
  6. L17
    specialize hcommon (e)
  7. L18
    apply hcommon
  8. L19
    exact hi
  9. L20
    exact hat
  10. L21
    exact hdiv

Library-wide reading audit

Original exact command ledger · 21 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro g
  5. 0005intro d
  6. 0006intro hcommon
  7. 0007intro hdiv
  8. 0008intro i
  9. 0009intro e
  10. 0010intro hi
  11. 0011intro hat
  12. 0012specialize multiple_trans (g)
  13. 0013specialize multiple_trans (d)
  14. 0014specialize multiple_trans (e)
  15. 0015apply multiple_trans
  16. 0016specialize hcommon (i)
  17. 0017specialize hcommon (e)
  18. 0018apply hcommon
  19. 0019exact hi
  20. 0020exact hat
  21. 0021exact hdiv