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 a. (((~((L) = 0)) /\ (((forall fom_index_pfp_monic_value_sourcecoefficients. (exists fom_gap_pfp_monic_value_sourcecoefficients_index_bound. fom_gap_pfp_monic_value_sourcecoefficients_index_bound + S (fom_index_pfp_monic_value_sourcecoefficients) = L) -> exists fom_value_pfp_monic_value_sourcecoefficients. ((((exists fom_beta_height_pfp_monic_value_sourcecoefficients_entry. fom_beta_height_pfp_monic_value_sourcecoefficients_entry + S (fom_value_pfp_monic_value_sourcecoefficients) = S ((S (fom_index_pfp_monic_value_sourcecoefficients)) * c)) /\ exists fom_beta_quotient_pfp_monic_value_sourcecoefficients_entry. b = fom_beta_quotient_pfp_monic_value_sourcecoefficients_entry * S ((S (fom_index_pfp_monic_value_sourcecoefficients)) * c) + (fom_value_pfp_monic_value_sourcecoefficients))) /\ (exists fom_gap_pfp_monic_value_sourcecoefficients_value_bound. fom_gap_pfp_monic_value_sourcecoefficients_value_bound + S (fom_value_pfp_monic_value_sourcecoefficients) = p))) /\ ((((exists ff_h_pfp_monic_value_sourceleading. ff_h_pfp_monic_value_sourceleading + S (1) = S ((S (0)) * c)) /\ exists ff_q_pfp_monic_value_sourceleading. b = ff_q_pfp_monic_value_sourceleading * S ((S (0)) * c) + (1)))))))) -> (((exists ff_h_pfp_monic_value_entry. ff_h_pfp_monic_value_entry + S (a) = S ((S (0)) * c)) /\ exists ff_q_pfp_monic_value_entry. b = ff_q_pfp_monic_value_entry * S ((S (0)) * c) + (a))) -> a=1Constructive proof overview
Generated structural guide
Every actual decoding of a monic leading coefficient is canonical one.
The unchanged tactic script uses 1 declared prerequisite and contains 17 exact native proof lines.
Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
beta_at_unique 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–9
03Use earlier factsL10–17
Original exact command ledger · 17 lines
- 0001
intro p - 0002
intro b - 0003
intro c - 0004
intro L - 0005
intro a - 0006
intro h - 0007
intro ha - 0008
cases h - 0009
cases h_right - 0010
specialize beta_at_unique (b) - 0011
specialize beta_at_unique (c) - 0012
specialize beta_at_unique (0) - 0013
specialize beta_at_unique (a) - 0014
specialize beta_at_unique (1) - 0015
apply beta_at_unique - 0016
exact ha - 0017
exact h_right_right