PA004R

finite_last_is_top_from_prefix_surjective

Stable checked-use theorem · independently closed

A bounded injective successor sequence must place the new value last once its prefix is surjective.

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 b c n sn. sn = S n -> (forall fp_i_bounded_succ. (exists fp_gap_bounded_succ_index. fp_gap_bounded_succ_index + S fp_i_bounded_succ = sn) -> exists fp_value_bounded_succ. ((((exists ff_h_bounded_succ_entry. ff_h_bounded_succ_entry + S (fp_value_bounded_succ) = S ((S (fp_i_bounded_succ)) * c)) /\ exists ff_q_bounded_succ_entry. b = ff_q_bounded_succ_entry * S ((S (fp_i_bounded_succ)) * c) + (fp_value_bounded_succ))) /\ (exists fp_gap_bounded_succ_value. fp_gap_bounded_succ_value + S fp_value_bounded_succ = sn))) -> (forall fp_i_inj_succ fp_j_inj_succ fp_value_inj_succ. (exists fp_gap_inj_succ_i. fp_gap_inj_succ_i + S fp_i_inj_succ = sn) -> (exists fp_gap_inj_succ_j. fp_gap_inj_succ_j + S fp_j_inj_succ = sn) -> (((exists ff_h_inj_succ_left. ff_h_inj_succ_left + S (fp_value_inj_succ) = S ((S (fp_i_inj_succ)) * c)) /\ exists ff_q_inj_succ_left. b = ff_q_inj_succ_left * S ((S (fp_i_inj_succ)) * c) + (fp_value_inj_succ))) -> (((exists ff_h_inj_succ_right. ff_h_inj_succ_right + S (fp_value_inj_succ) = S ((S (fp_j_inj_succ)) * c)) /\ exists ff_q_inj_succ_right. b = ff_q_inj_succ_right * S ((S (fp_j_inj_succ)) * c) + (fp_value_inj_succ))) -> fp_i_inj_succ = fp_j_inj_succ) -> (forall fp_value_surj_n. (exists fp_gap_surj_n_value. fp_gap_surj_n_value + S fp_value_surj_n = n) -> exists fp_i_surj_n. ((exists fp_gap_surj_n_index. fp_gap_surj_n_index + S fp_i_surj_n = n) /\ (((exists ff_h_surj_n_entry. ff_h_surj_n_entry + S (fp_value_surj_n) = S ((S (fp_i_surj_n)) * c)) /\ exists ff_q_surj_n_entry. b = ff_q_surj_n_entry * S ((S (fp_i_surj_n)) * c) + (fp_value_surj_n))))) -> (((exists ff_h_last_n. ff_h_last_n + S (n) = S ((S (n)) * c)) /\ exists ff_q_last_n. b = ff_q_last_n * S ((S (n)) * c) + (n)))

Structural proof guide

Generated structural guide

A bounded injective successor sequence must place the new value last once its prefix is surjective.

Use the direct prerequisites finite_bounded_last_succ, finite_lt_succ_eq_or_lt, le_refl, le_succ, lt_irrefl_expanded as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (4), equality transport (5).

Referenced ingredients

PA004I finite_bounded_last_succ PA003D finite_lt_succ_eq_or_lt PA001A le_refl PA002O le_succ PA0010 lt_irrefl_expanded

Proof neighborhood

Direct dependencies

PA004I finite_bounded_last_succ PA003D finite_lt_succ_eq_or_lt PA001A le_refl PA002O le_succ PA0010 lt_irrefl_expanded

Direct dependents

PA004T finite_surjective_succ_from_prefix

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

53 script commands · 16 reading checkpoints · 4 local claims

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 (5)
finite bounded last succfinite lt succ eq or ltle reflle succlt irrefl expanded
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro n
  4. L4
    intro sn
  5. L5
    intro hsn
  6. L6
    intro hbounded
  7. L7
    intro hinj
  8. L8
    intro hsurj
02Calculate and transport equalitiesL9–10

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L9
    rewrite hsn at hinj
  2. L10
    rewrite hsn at hinj
03Establish hlastL11–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bounded last succ.

  1. L11
    have hlast : exists x. (((exists h. h + S x = S ((S n) * c)) /\ exists q. b = q * S ((S n) * c) + x) /\ exists h. h + S x = S n)
  2. L12
    specialize finite_bounded_last_succ b
  3. L13
    specialize finite_bounded_last_succ c
  4. L14
    specialize finite_bounded_last_succ n
  5. L15
    specialize finite_bounded_last_succ sn
  6. L16
    apply finite_bounded_last_succ
  7. L17
    exact hsn
  8. L18
    exact hbounded
04Separate the logical casesL19–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hlast
  2. L20
    cases hlast_witness
05Establish hsplitL21–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L21
    have hsplit : x = n \/ exists h. h + S x = n
  2. L22
    specialize finite_lt_succ_eq_or_lt n
  3. L23
    specialize finite_lt_succ_eq_or_lt x
  4. L24
    apply finite_lt_succ_eq_or_lt
  5. L25
    exact hlast_witness_right
06Separate the logical casesL26–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L26
    cases hsplit
07Calculate and transport equalitiesL27–28

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    rewrite hsplit_left at hlast_witness_left
  2. L28
    rewrite hsplit_left at hlast_witness_left
08Use earlier factsL29–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    exact hlast_witness_left
  2. L30
    specialize hsurj x
09Establish hpreL31–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsurj.

  1. L31
    have hpre : exists i. ((exists h. h + S i = n) /\ ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x))
  2. L32
    apply hsurj
  3. L33
    exact hsplit_right
10Separate the logical casesL34–35

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L34
    cases hpre
  2. L35
    cases hpre_witness
11Establish hniL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinj.

  1. L36
    have hni : n = x1
  2. L37
    specialize hinj n
  3. L38
    specialize hinj x1
  4. L39
    specialize hinj x
  5. L40
    apply hinj
  6. L41
    specialize le_refl (S n)
  7. L42
    exact le_refl
  8. L43
    specialize le_succ (S x1)
  9. L44
    specialize le_succ n
  10. L45
    apply le_succ
12Use earlier factsL46–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L46
    exact hpre_witness_left
  2. L47
    exact hlast_witness_left
  3. L48
    exact hpre_witness_right
13Separate the logical casesL49–49

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L49
    exfalso
14Use earlier factsL50–51

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    specialize lt_irrefl_expanded n
  2. L51
    apply lt_irrefl_expanded
15Calculate and transport equalitiesL52–52

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L52
    rewrite hni
16Use earlier factsL53–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L53
    exact hpre_witness_left

Library-wide reading audit

Original exact command ledger · 53 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro sn
  5. 0005intro hsn
  6. 0006intro hbounded
  7. 0007intro hinj
  8. 0008intro hsurj
  9. 0009rewrite hsn at hinj
  10. 0010rewrite hsn at hinj
  11. 0011have hlast : exists x. (((exists h. h + S x = S ((S n) * c)) /\ exists q. b = q * S ((S n) * c) + x) /\ exists h. h + S x = S n)
  12. 0012specialize finite_bounded_last_succ b
  13. 0013specialize finite_bounded_last_succ c
  14. 0014specialize finite_bounded_last_succ n
  15. 0015specialize finite_bounded_last_succ sn
  16. 0016apply finite_bounded_last_succ
  17. 0017exact hsn
  18. 0018exact hbounded
  19. 0019cases hlast
  20. 0020cases hlast_witness
  21. 0021have hsplit : x = n \/ exists h. h + S x = n
  22. 0022specialize finite_lt_succ_eq_or_lt n
  23. 0023specialize finite_lt_succ_eq_or_lt x
  24. 0024apply finite_lt_succ_eq_or_lt
  25. 0025exact hlast_witness_right
  26. 0026cases hsplit
  27. 0027rewrite hsplit_left at hlast_witness_left
  28. 0028rewrite hsplit_left at hlast_witness_left
  29. 0029exact hlast_witness_left
  30. 0030specialize hsurj x
  31. 0031have hpre : exists i. ((exists h. h + S i = n) /\ ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x))
  32. 0032apply hsurj
  33. 0033exact hsplit_right
  34. 0034cases hpre
  35. 0035cases hpre_witness
  36. 0036have hni : n = x1
  37. 0037specialize hinj n
  38. 0038specialize hinj x1
  39. 0039specialize hinj x
  40. 0040apply hinj
  41. 0041specialize le_refl (S n)
  42. 0042exact le_refl
  43. 0043specialize le_succ (S x1)
  44. 0044specialize le_succ n
  45. 0045apply le_succ
  46. 0046exact hpre_witness_left
  47. 0047exact hlast_witness_left
  48. 0048exact hpre_witness_right
  49. 0049exfalso
  50. 0050specialize lt_irrefl_expanded n
  51. 0051apply lt_irrefl_expanded
  52. 0052rewrite hni
  53. 0053exact hpre_witness_left