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 expanded first-order arithmetic statement
forall p b c L d. (((~((L) = 0)) /\ (((forall fom_index_pfp_monic_degree_sourcecoefficients. (exists fom_gap_pfp_monic_degree_sourcecoefficients_index_bound. fom_gap_pfp_monic_degree_sourcecoefficients_index_bound + S (fom_index_pfp_monic_degree_sourcecoefficients) = L) -> exists fom_value_pfp_monic_degree_sourcecoefficients. ((((exists fom_beta_height_pfp_monic_degree_sourcecoefficients_entry. fom_beta_height_pfp_monic_degree_sourcecoefficients_entry + S (fom_value_pfp_monic_degree_sourcecoefficients) = S ((S (fom_index_pfp_monic_degree_sourcecoefficients)) * c)) /\ exists fom_beta_quotient_pfp_monic_degree_sourcecoefficients_entry. b = fom_beta_quotient_pfp_monic_degree_sourcecoefficients_entry * S ((S (fom_index_pfp_monic_degree_sourcecoefficients)) * c) + (fom_value_pfp_monic_degree_sourcecoefficients))) /\ (exists fom_gap_pfp_monic_degree_sourcecoefficients_value_bound. fom_gap_pfp_monic_degree_sourcecoefficients_value_bound + S (fom_value_pfp_monic_degree_sourcecoefficients) = p))) /\ ((((exists ff_h_pfp_monic_degree_sourceleading. ff_h_pfp_monic_degree_sourceleading + S (1) = S ((S (0)) * c)) /\ exists ff_q_pfp_monic_degree_sourceleading. b = ff_q_pfp_monic_degree_sourceleading * S ((S (0)) * c) + (1)))))))) -> L=S d -> ((((L)=S (d)) /\ (((forall fom_index_pfp_monic_degree_resultcoefficients. (exists fom_gap_pfp_monic_degree_resultcoefficients_index_bound. fom_gap_pfp_monic_degree_resultcoefficients_index_bound + S (fom_index_pfp_monic_degree_resultcoefficients) = L) -> exists fom_value_pfp_monic_degree_resultcoefficients. ((((exists fom_beta_height_pfp_monic_degree_resultcoefficients_entry. fom_beta_height_pfp_monic_degree_resultcoefficients_entry + S (fom_value_pfp_monic_degree_resultcoefficients) = S ((S (fom_index_pfp_monic_degree_resultcoefficients)) * c)) /\ exists fom_beta_quotient_pfp_monic_degree_resultcoefficients_entry. b = fom_beta_quotient_pfp_monic_degree_resultcoefficients_entry * S ((S (fom_index_pfp_monic_degree_resultcoefficients)) * c) + (fom_value_pfp_monic_degree_resultcoefficients))) /\ (exists fom_gap_pfp_monic_degree_resultcoefficients_value_bound. fom_gap_pfp_monic_degree_resultcoefficients_value_bound + S (fom_value_pfp_monic_degree_resultcoefficients) = p))) /\ ((exists pfd_leading_monic_degree_result. ((((exists ff_h_pfp_monic_degree_resultentry. ff_h_pfp_monic_degree_resultentry + S (pfd_leading_monic_degree_result) = S ((S (0)) * c)) /\ exists ff_q_pfp_monic_degree_resultentry. b = ff_q_pfp_monic_degree_resultentry * S ((S (0)) * c) + (pfd_leading_monic_degree_result))) /\ ((~(pfd_leading_monic_degree_result=0))))))))))Constructive proof overview
Generated structural guide
A monic prefix of annotated length S d has represented degree d, also for d=0.
The unchanged tactic script uses 1 declared prerequisite and contains 20 exact native proof lines.
Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
succ_ne_zero Stable theorem; checked-use authorizedDirect dependents
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
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–7
02Separate the logical casesL8–10
03Use earlier factsL11–11
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L11
exact hlen
04Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
split
05Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact h_right_left
06Construct an explicit witnessL14–14
Supply the displayed value, then prove that it has the required property.
- L14
exists 1
07Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
08Use earlier factsL16–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
exact h_right_right
09Fix variables and assumptionsL17–17
Work with arbitrary variables or the premises of the current implication.
- L17
intro hz