SK001E

prime_exponent_prefix_gcd_empty

The empty exponent prefix has greatest common divisor zero, including all common divisors of the empty family.

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. PrimeExponentPrefixGCD(b,c,0,0)

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

Definition DAG

PrimeExponentPrefixGCD(b,c,l,g) · 1

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisite
Original expanded first-order statement 
forall b c. (((forall ppf_index_empty_gcdcommon ppf_entry_empty_gcdcommon. (exists pvs_gap_empty_gcdcommonbound. pvs_gap_empty_gcdcommonbound + S (ppf_index_empty_gcdcommon) = (0)) -> (((exists ff_h_pvs_empty_gcdcommonentry. ff_h_pvs_empty_gcdcommonentry + S (ppf_entry_empty_gcdcommon) = S ((S (ppf_index_empty_gcdcommon)) * c)) /\ exists ff_q_pvs_empty_gcdcommonentry. b = ff_q_pvs_empty_gcdcommonentry * S ((S (ppf_index_empty_gcdcommon)) * c) + (ppf_entry_empty_gcdcommon))) -> (exists pvs_factor_empty_gcdcommondivisor. (ppf_entry_empty_gcdcommon) = (0) * pvs_factor_empty_gcdcommondivisor)) /\ (forall ppf_common_empty_gcd. (forall ppf_index_empty_gcdother ppf_entry_empty_gcdother. (exists pvs_gap_empty_gcdotherbound. pvs_gap_empty_gcdotherbound + S (ppf_index_empty_gcdother) = (0)) -> (((exists ff_h_pvs_empty_gcdotherentry. ff_h_pvs_empty_gcdotherentry + S (ppf_entry_empty_gcdother) = S ((S (ppf_index_empty_gcdother)) * c)) /\ exists ff_q_pvs_empty_gcdotherentry. b = ff_q_pvs_empty_gcdotherentry * S ((S (ppf_index_empty_gcdother)) * c) + (ppf_entry_empty_gcdother))) -> (exists pvs_factor_empty_gcdotherdivisor. (ppf_entry_empty_gcdother) = (ppf_common_empty_gcd) * pvs_factor_empty_gcdotherdivisor)) -> (exists pvs_factor_empty_gcdgreatest. (0) = (ppf_common_empty_gcd) * pvs_factor_empty_gcdgreatest))))

Complete tactic proof in conservative notation

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

16 script commands · 9 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–2

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

  1. L1
    intro b
  2. L2
    intro c
02Separate the logical casesL3–3

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

  1. L3
    split
03Fix variables and assumptionsL4–7

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

  1. L4
    intro i
  2. L5
    intro e
  3. L6
    intro hi
  4. L7
    intro hat
04Separate the logical casesL8–8

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

  1. L8
    exfalso
05Use earlier factsL9–11

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

  1. L9
    specialize factor_permutation_below_zero_impossible (i)
  2. L10
    apply factor_permutation_below_zero_impossible
  3. L11
    exact hi
06Fix variables and assumptionsL12–13

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

  1. L12
    intro d
  2. L13
    intro hcommon
07Construct an explicit witnessL14–14

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

  1. L14
    exists 0
08Calculate and transport equalitiesL15–15

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L15
    symm
09Use earlier factsL16–16

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

  1. L16
    apply PA5

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003split
  4. 0004intro i
  5. 0005intro e
  6. 0006intro hi
  7. 0007intro hat
  8. 0008exfalso
  9. 0009specialize factor_permutation_below_zero_impossible (i)
  10. 0010apply factor_permutation_below_zero_impossible
  11. 0011exact hi
  12. 0012intro d
  13. 0013intro hcommon
  14. 0014exists 0
  15. 0015symm
  16. 0016apply PA5