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 n. exists b c. (((forall espo_position_zero_state_closed espo_source_zero_state_closed espo_mate_zero_state_closed. (exists wpo_gap_zero_state_closed_position_bound. wpo_gap_zero_state_closed_position_bound + S (espo_position_zero_state_closed) = 0) -> (((exists wpo_beta_height_zero_state_closed_source_entry. wpo_beta_height_zero_state_closed_source_entry + S (espo_source_zero_state_closed) = S ((S (espo_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_source_entry. b = wpo_beta_quotient_zero_state_closed_source_entry * S ((S (espo_position_zero_state_closed)) * c) + (espo_source_zero_state_closed))) -> (((exists wpo_beta_height_zero_state_closed_scaled_entry. wpo_beta_height_zero_state_closed_scaled_entry + S (S espo_mate_zero_state_closed) = S ((S (espo_source_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_zero_state_closed_scaled_entry. u = wpo_beta_quotient_zero_state_closed_scaled_entry * S ((S (espo_source_zero_state_closed)) * v) + (S espo_mate_zero_state_closed))) -> exists espo_mate_position_zero_state_closed. ((exists wpo_gap_zero_state_closed_mate_bound. wpo_gap_zero_state_closed_mate_bound + S (espo_mate_position_zero_state_closed) = 0) /\ (((exists wpo_beta_height_zero_state_closed_mate_entry. wpo_beta_height_zero_state_closed_mate_entry + S (espo_mate_zero_state_closed) = S ((S (espo_mate_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_mate_entry. b = wpo_beta_quotient_zero_state_closed_mate_entry * S ((S (espo_mate_position_zero_state_closed)) * c) + (espo_mate_zero_state_closed))))) /\ (((forall fom_index_zero_state_bounded. (exists fom_gap_zero_state_bounded_index_bound. fom_gap_zero_state_bounded_index_bound + S (fom_index_zero_state_bounded) = 0) -> exists fom_value_zero_state_bounded. ((((exists fom_beta_height_zero_state_bounded_entry. fom_beta_height_zero_state_bounded_entry + S (fom_value_zero_state_bounded) = S ((S (fom_index_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_zero_state_bounded_entry. b = fom_beta_quotient_zero_state_bounded_entry * S ((S (fom_index_zero_state_bounded)) * c) + (fom_value_zero_state_bounded))) /\ (exists fom_gap_zero_state_bounded_value_bound. fom_gap_zero_state_bounded_value_bound + S (fom_value_zero_state_bounded) = n))) /\ (forall wpo_injective_left_zero_state_injective wpo_injective_right_zero_state_injective wpo_injective_value_zero_state_injective. (exists wpo_gap_zero_state_injective_left_bound. wpo_gap_zero_state_injective_left_bound + S (wpo_injective_left_zero_state_injective) = 0) -> (exists wpo_gap_zero_state_injective_right_bound. wpo_gap_zero_state_injective_right_bound + S (wpo_injective_right_zero_state_injective) = 0) -> (((exists wpo_beta_height_zero_state_injective_left_entry. wpo_beta_height_zero_state_injective_left_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_left_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_left_entry. b = wpo_beta_quotient_zero_state_injective_left_entry * S ((S (wpo_injective_left_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> (((exists wpo_beta_height_zero_state_injective_right_entry. wpo_beta_height_zero_state_injective_right_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_right_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_right_entry. b = wpo_beta_quotient_zero_state_injective_right_entry * S ((S (wpo_injective_right_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> wpo_injective_left_zero_state_injective = wpo_injective_right_zero_state_injective)))))Structural proof guide
Generated structural guide
Zero codes witness the empty shifted, bounded, injective state.
Use the direct prerequisites scaled_orbit_closed_prefix_zero, bounded_into_zero, injective_prefix_zero as previously established PA formulas.
The proof proceeds by direct introduction and elimination.
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 (3)
01Fix variables and assumptionsL1–3
02Construct an explicit witnessL4–5
03Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
split
04Use earlier factsL7–11
Instantiate or apply named facts and discharge the corresponding proof obligations.
05Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
split
06Use earlier factsL13–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 19 lines
- 0001
intro u - 0002
intro v - 0003
intro n - 0004
exists 0 - 0005
exists 0 - 0006
split - 0007
specialize scaled_orbit_closed_prefix_zero u - 0008
specialize scaled_orbit_closed_prefix_zero v - 0009
specialize scaled_orbit_closed_prefix_zero 0 - 0010
specialize scaled_orbit_closed_prefix_zero 0 - 0011
exact scaled_orbit_closed_prefix_zero - 0012
split - 0013
specialize bounded_into_zero 0 - 0014
specialize bounded_into_zero 0 - 0015
specialize bounded_into_zero n - 0016
exact bounded_into_zero - 0017
specialize injective_prefix_zero 0 - 0018
specialize injective_prefix_zero 0 - 0019
exact injective_prefix_zero