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 espo_position_zero_closed espo_source_zero_closed espo_mate_zero_closed. (exists wpo_gap_zero_closed_position_bound. wpo_gap_zero_closed_position_bound + S (espo_position_zero_closed) = 0) -> (((exists wpo_beta_height_zero_closed_source_entry. wpo_beta_height_zero_closed_source_entry + S (espo_source_zero_closed) = S ((S (espo_position_zero_closed)) * c)) /\ exists wpo_beta_quotient_zero_closed_source_entry. b = wpo_beta_quotient_zero_closed_source_entry * S ((S (espo_position_zero_closed)) * c) + (espo_source_zero_closed))) -> (((exists wpo_beta_height_zero_closed_scaled_entry. wpo_beta_height_zero_closed_scaled_entry + S (S espo_mate_zero_closed) = S ((S (espo_source_zero_closed)) * v)) /\ exists wpo_beta_quotient_zero_closed_scaled_entry. u = wpo_beta_quotient_zero_closed_scaled_entry * S ((S (espo_source_zero_closed)) * v) + (S espo_mate_zero_closed))) -> exists espo_mate_position_zero_closed. ((exists wpo_gap_zero_closed_mate_bound. wpo_gap_zero_closed_mate_bound + S (espo_mate_position_zero_closed) = 0) /\ (((exists wpo_beta_height_zero_closed_mate_entry. wpo_beta_height_zero_closed_mate_entry + S (espo_mate_zero_closed) = S ((S (espo_mate_position_zero_closed)) * c)) /\ exists wpo_beta_quotient_zero_closed_mate_entry. b = wpo_beta_quotient_zero_closed_mate_entry * S ((S (espo_mate_position_zero_closed)) * c) + (espo_mate_zero_closed)))))Structural proof guide
Generated structural guide
Shifted orbit closure is vacuous on an empty order prefix.
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–10
02Separate the logical casesL11–12
03Establish hsqL13–20
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 · 20 lines
- 0001
intro u - 0002
intro v - 0003
intro b - 0004
intro c - 0005
intro q - 0006
intro s - 0007
intro t - 0008
intro hq - 0009
intro hsource - 0010
intro hscaled - 0011
exfalso - 0012
cases hq - 0013
have hsq : S q = 0 - 0014
specialize add_eq_zero_right x - 0015
specialize add_eq_zero_right (S q) - 0016
apply add_eq_zero_right - 0017
exact hq_witness - 0018
specialize succ_ne_zero q - 0019
apply succ_ne_zero - 0020
exact hsq