SK001F — prime_exponent_prefix_gcd_successor

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 v h. (((forall ppf_index_gcd_prefixcommon ppf_entry_gcd_prefixcommon. (exists pvs_gap_gcd_prefixcommonbound. pvs_gap_gcd_prefixcommonbound + S (ppf_index_gcd_prefixcommon) = (l)) -> (((exists ff_h_pvs_gcd_prefixcommonentry. ff_h_pvs_gcd_prefixcommonentry + S (ppf_entry_gcd_prefixcommon) = S ((S (ppf_index_gcd_prefixcommon)) * c)) /\ exists ff_q_pvs_gcd_prefixcommonentry. b = ff_q_pvs_gcd_prefixcommonentry * S ((S (ppf_index_gcd_prefixcommon)) * c) + (ppf_entry_gcd_prefixcommon))) -> (exists pvs_factor_gcd_prefixcommondivisor. (ppf_entry_gcd_prefixcommon) = (g) * pvs_factor_gcd_prefixcommondivisor)) /\ (forall ppf_common_gcd_prefix. (forall ppf_index_gcd_prefixother ppf_entry_gcd_prefixother. (exists pvs_gap_gcd_prefixotherbound. pvs_gap_gcd_prefixotherbound + S (ppf_index_gcd_prefixother) = (l)) -> (((exists ff_h_pvs_gcd_prefixotherentry. ff_h_pvs_gcd_prefixotherentry + S (ppf_entry_gcd_prefixother) = S ((S (ppf_index_gcd_prefixother)) * c)) /\ exists ff_q_pvs_gcd_prefixotherentry. b = ff_q_pvs_gcd_prefixotherentry * S ((S (ppf_index_gcd_prefixother)) * c) + (ppf_entry_gcd_prefixother))) -> (exists pvs_factor_gcd_prefixotherdivisor. (ppf_entry_gcd_prefixother) = (ppf_common_gcd_prefix) * pvs_factor_gcd_prefixotherdivisor)) -> (exists pvs_factor_gcd_prefixgreatest. (g) = (ppf_common_gcd_prefix) * pvs_factor_gcd_prefixgreatest)))) -> (((exists ff_h_pvs_gcd_last. ff_h_pvs_gcd_last + S (v) = S ((S (l)) * c)) /\ exists ff_q_pvs_gcd_last. b = ff_q_pvs_gcd_last * S ((S (l)) * c) + (v))) -> ((((exists hag_left_factor_ppf_gcd_merge. g = h * hag_left_factor_ppf_gcd_merge) /\ (exists hag_right_factor_ppf_gcd_merge. v = h * hag_right_factor_ppf_gcd_merge)) /\ forall hag_divisor_ppf_gcd_merge. (exists hag_common_left_ppf_gcd_merge. g = hag_divisor_ppf_gcd_merge * hag_common_left_ppf_gcd_merge) -> (exists hag_common_right_ppf_gcd_merge. v = hag_divisor_ppf_gcd_merge * hag_common_right_ppf_gcd_merge) -> exists hag_greatest_factor_ppf_gcd_merge. h = hag_divisor_ppf_gcd_merge * hag_greatest_factor_ppf_gcd_merge)) -> (((forall ppf_index_gcd_successorcommon ppf_entry_gcd_successorcommon. (exists pvs_gap_gcd_successorcommonbound. pvs_gap_gcd_successorcommonbound + S (ppf_index_gcd_successorcommon) = (S l)) -> (((exists ff_h_pvs_gcd_successorcommonentry. ff_h_pvs_gcd_successorcommonentry + S (ppf_entry_gcd_successorcommon) = S ((S (ppf_index_gcd_successorcommon)) * c)) /\ exists ff_q_pvs_gcd_successorcommonentry. b = ff_q_pvs_gcd_successorcommonentry * S ((S (ppf_index_gcd_successorcommon)) * c) + (ppf_entry_gcd_successorcommon))) -> (exists pvs_factor_gcd_successorcommondivisor. (ppf_entry_gcd_successorcommon) = (h) * pvs_factor_gcd_successorcommondivisor)) /\ (forall ppf_common_gcd_successor. (forall ppf_index_gcd_successorother ppf_entry_gcd_successorother. (exists pvs_gap_gcd_successorotherbound. pvs_gap_gcd_successorotherbound + S (ppf_index_gcd_successorother) = (S l)) -> (((exists ff_h_pvs_gcd_successorotherentry. ff_h_pvs_gcd_successorotherentry + S (ppf_entry_gcd_successorother) = S ((S (ppf_index_gcd_successorother)) * c)) /\ exists ff_q_pvs_gcd_successorotherentry. b = ff_q_pvs_gcd_successorotherentry * S ((S (ppf_index_gcd_successorother)) * c) + (ppf_entry_gcd_successorother))) -> (exists pvs_factor_gcd_successorotherdivisor. (ppf_entry_gcd_successorother) = (ppf_common_gcd_successor) * pvs_factor_gcd_successorotherdivisor)) -> (exists pvs_factor_gcd_successorgreatest. (h) = (ppf_common_gcd_successor) * pvs_factor_gcd_successorgreatest))))

Constructive proof overview

Generated structural guide

The canonical gcd of the old actual prefix gcd and final decoded exponent is the gcd of the successor prefix.

The unchanged tactic script uses 7 declared prerequisites and contains 57 exact native proof lines.

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

Proof neighborhood

Direct dependencies

is_gcd_dvd_left Stable theorem; checked-use authorized is_gcd_dvd_right Stable theorem; checked-use authorized SK001D prime_exponent_common_divisor_factor SK001C prime_exponent_common_divisor_successor is_gcd_greatest Stable theorem; checked-use authorized SK001B prime_exponent_common_divisor_drop le_refl Stable 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

57 script commands · 8 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.

Named ingredients (3)

prime exponent common divisor factor prime exponent common divisor successor prime exponent common divisor drop

01Fix variables and assumptionsL1–9

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

L1
intro b
L2
intro c
L3
intro l
L4
intro g
L5
intro v
L6
intro h
L7
intro hprefix
L8
intro hlast
L9
intro hmerge

02Separate the logical casesL10–11

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

L10
cases hprefix
L11
split

03Use earlier factsL12–21