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 p n k b c. p = S n -> n = S k -> (forall wip_index_last_prefix. (exists wip_gap_last_prefix_prefix_bound. wip_gap_last_prefix_prefix_bound + S wip_index_last_prefix = n) -> exists wip_mate_last_prefix. ((((exists wip_beta_height_last_prefix_decoded. wip_beta_height_last_prefix_decoded + S (wip_mate_last_prefix) = S ((S (wip_index_last_prefix)) * c)) /\ exists wip_beta_quotient_last_prefix_decoded. b = wip_beta_quotient_last_prefix_decoded * S ((S (wip_index_last_prefix)) * c) + (wip_mate_last_prefix))) /\ ((exists wip_gap_last_prefix_inverse_index_bound. wip_gap_last_prefix_inverse_index_bound + S wip_index_last_prefix = n) /\ ((exists wip_gap_last_prefix_inverse_mate_bound. wip_gap_last_prefix_inverse_mate_bound + S wip_mate_last_prefix = n) /\ (exists wip_mod_left_last_prefix_inverse_mod wip_mod_right_last_prefix_inverse_mod. ((S wip_index_last_prefix) * S wip_mate_last_prefix) + p * wip_mod_left_last_prefix_inverse_mod = 1 + p * wip_mod_right_last_prefix_inverse_mod))))) -> (((exists wip_beta_height_last_result. wip_beta_height_last_result + S (k) = S ((S (k)) * c)) /\ exists wip_beta_quotient_last_result. b = wip_beta_quotient_last_result * S ((S (k)) * c) + (k)))Structural proof guide
Generated structural guide
The last index, representing the predecessor of p, is fixed by the full inverse prefix.
Use the direct prerequisites zero_add, predecessor_square_mod_one, inverse_prefix_extensional as previously established PA formulas.
The proof proceeds by intermediate claims (4), equality transport (3).
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–8
02Establish hlast_boundL9–10
03Construct an explicit witnessL11–11
Supply the displayed value, then prove that it has the required property.
- L11
exists 0
04Use earlier factsL12–13
05Establish hpredecessor_modL14–18
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply predecessor square mod one.
06Establish hlast_modL19–22
07Establish hlast_relationL23–23
Establish this local claim before using it. It is not an additional assumption.
- L23
have hlast_relation : (exists wip_gap_last_relation_index_bound. wip_gap_last_relation_index_bound + S k = n) /\ ((exists wip_gap_last_relation_mate_bound. wip_gap_last_relation_mate_bound + S k = n) /\ (exists wip_mod_left_last_relation_mod wip_mod_right_last_relation_mod. ((S k) * S k) + p * wip_mod_left_last_relation_mod = 1 + p * wip_mod_right_last_relation_mod))
08Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
split
09Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hlast_bound
10Separate the logical casesL26–26
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L26
split
11Use earlier factsL27–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L27
exact hlast_bound - L28
exact hlast_mod - L29
specialize inverse_prefix_extensional p - L30
specialize inverse_prefix_extensional n - L31
specialize inverse_prefix_extensional b - L32
specialize inverse_prefix_extensional c - L33
specialize inverse_prefix_extensional n - L34
specialize inverse_prefix_extensional k - L35
specialize inverse_prefix_extensional k - L36
apply inverse_prefix_extensional
Original exact command ledger · 40 lines
- 0001
intro p - 0002
intro n - 0003
intro k - 0004
intro b - 0005
intro c - 0006
intro hpn - 0007
intro hnk - 0008
intro hprefix - 0009
have hlast_bound : exists wip_gap_last_bound. wip_gap_last_bound + S k = n - 0010
rewrite hnk - 0011
exists 0 - 0012
specialize zero_add (S k) - 0013
exact zero_add - 0014
have hpredecessor_mod : exists wie_mod_left_predecessor wie_mod_right_predecessor. (n * n) + p * wie_mod_left_predecessor = (1) + p * wie_mod_right_predecessor - 0015
specialize predecessor_square_mod_one p - 0016
specialize predecessor_square_mod_one n - 0017
apply predecessor_square_mod_one - 0018
exact hpn - 0019
have hlast_mod : exists wie_mod_left_last wie_mod_right_last. ((S k) * S k) + p * wie_mod_left_last = (1) + p * wie_mod_right_last - 0020
rewrite <- hnk - 0021
rewrite <- hnk - 0022
exact hpredecessor_mod - 0023
have hlast_relation : (exists wip_gap_last_relation_index_bound. wip_gap_last_relation_index_bound + S k = n) /\ ((exists wip_gap_last_relation_mate_bound. wip_gap_last_relation_mate_bound + S k = n) /\ (exists wip_mod_left_last_relation_mod wip_mod_right_last_relation_mod. ((S k) * S k) + p * wip_mod_left_last_relation_mod = 1 + p * wip_mod_right_last_relation_mod)) - 0024
split - 0025
exact hlast_bound - 0026
split - 0027
exact hlast_bound - 0028
exact hlast_mod - 0029
specialize inverse_prefix_extensional p - 0030
specialize inverse_prefix_extensional n - 0031
specialize inverse_prefix_extensional b - 0032
specialize inverse_prefix_extensional c - 0033
specialize inverse_prefix_extensional n - 0034
specialize inverse_prefix_extensional k - 0035
specialize inverse_prefix_extensional k - 0036
apply inverse_prefix_extensional - 0037
exact hpn - 0038
exact hprefix - 0039
exact hlast_bound - 0040
exact hlast_relation