SK001D

prime_exponent_common_divisor_factor

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

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. ∀ d. (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → Dvd(g,y)) → Dvd(d,g) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → Dvd(d,y)

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

Definition DAG

Lt(a,b) · 2Dvd(d,n) · 3BetaAt(b,c,i,x) · 2

Actual proof prerequisites

multiple_trans · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

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

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.

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 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 defined 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