SK001E

prime_exponent_prefix_gcd_empty

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

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

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. (((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))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

factor_permutation_below_zero_impossible Alpha theorem; checked-use authorized

Direct dependents

SK0020 prime_exponent_prefix_gcd_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

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.

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