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 PA statement
forall u v b c. (forall wpop_pair_wpop_zero_pairs. (exists wpo_gap_wpop_zero_pairs_pair_bound. wpo_gap_wpop_zero_pairs_pair_bound + S (wpop_pair_wpop_zero_pairs) = 0) -> exists wpop_left_wpop_zero_pairs wpop_right_wpop_zero_pairs. ((((exists wpo_beta_height_wpop_zero_pairs_left_entry. wpo_beta_height_wpop_zero_pairs_left_entry + S (wpop_left_wpop_zero_pairs) = S ((S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs)) * c)) /\ exists wpo_beta_quotient_wpop_zero_pairs_left_entry. b = wpo_beta_quotient_wpop_zero_pairs_left_entry * S ((S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs)) * c) + (wpop_left_wpop_zero_pairs))) /\ ((((exists wpo_beta_height_wpop_zero_pairs_right_entry. wpo_beta_height_wpop_zero_pairs_right_entry + S (wpop_right_wpop_zero_pairs) = S ((S (S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs))) * c)) /\ exists wpo_beta_quotient_wpop_zero_pairs_right_entry. b = wpo_beta_quotient_wpop_zero_pairs_right_entry * S ((S (S (wpop_pair_wpop_zero_pairs + wpop_pair_wpop_zero_pairs))) * c) + (wpop_right_wpop_zero_pairs))) /\ (((exists wpo_beta_height_wpop_zero_pairs_inverse_entry. wpo_beta_height_wpop_zero_pairs_inverse_entry + S (wpop_right_wpop_zero_pairs) = S ((S (wpop_left_wpop_zero_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_zero_pairs_inverse_entry. u = wpo_beta_quotient_wpop_zero_pairs_inverse_entry * S ((S (wpop_left_wpop_zero_pairs)) * v) + (wpop_right_wpop_zero_pairs))))))Structural proof guide
Generated structural guide
The adjacent inverse-pair witness invariant is vacuous at zero.
Use the direct prerequisites add_eq_zero_right, succ_ne_zero as previously established PA formulas.
The proof proceeds by case analysis (1), intermediate claims (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
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.
Named ingredients (2)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–8
03Establish hstL9–16
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.
Original exact command ledger · 16 lines
- 0001
intro u - 0002
intro v - 0003
intro b - 0004
intro c - 0005
intro t - 0006
intro ht - 0007
exfalso - 0008
cases ht - 0009
have hst : S t = 0 - 0010
specialize add_eq_zero_right x - 0011
specialize add_eq_zero_right (S t) - 0012
apply add_eq_zero_right - 0013
exact ht_witness - 0014
specialize succ_ne_zero t - 0015
apply succ_ne_zero - 0016
exact hst