TS000Q

finite_prefix_injective_extend_fresh

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

An injective decoded prefix stays injective when its new final value has no earlier occurrence.

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 first-order arithmetic statement

forall b c n v. (forall fp_i_fpcd_old fp_j_fpcd_old fp_value_fpcd_old. (exists fp_gap_fpcd_old_i. fp_gap_fpcd_old_i + S fp_i_fpcd_old = n) -> (exists fp_gap_fpcd_old_j. fp_gap_fpcd_old_j + S fp_j_fpcd_old = n) -> (((exists ff_h_fpcd_old_left. ff_h_fpcd_old_left + S (fp_value_fpcd_old) = S ((S (fp_i_fpcd_old)) * c)) /\ exists ff_q_fpcd_old_left. b = ff_q_fpcd_old_left * S ((S (fp_i_fpcd_old)) * c) + (fp_value_fpcd_old))) -> (((exists ff_h_fpcd_old_right. ff_h_fpcd_old_right + S (fp_value_fpcd_old) = S ((S (fp_j_fpcd_old)) * c)) /\ exists ff_q_fpcd_old_right. b = ff_q_fpcd_old_right * S ((S (fp_j_fpcd_old)) * c) + (fp_value_fpcd_old))) -> fp_i_fpcd_old = fp_j_fpcd_old) -> (((exists ff_h_fpcd_last. ff_h_fpcd_last + S (v) = S ((S (n)) * c)) /\ exists ff_q_fpcd_last. b = ff_q_fpcd_last * S ((S (n)) * c) + (v))) -> ~(exists fp_i_fpcd_contains. ((exists fp_gap_fpcd_contains_index. fp_gap_fpcd_contains_index + S fp_i_fpcd_contains = n) /\ (((exists ff_h_fpcd_contains_entry. ff_h_fpcd_contains_entry + S (v) = S ((S (fp_i_fpcd_contains)) * c)) /\ exists ff_q_fpcd_contains_entry. b = ff_q_fpcd_contains_entry * S ((S (fp_i_fpcd_contains)) * c) + (v))))) -> (forall fp_i_fpcd_next fp_j_fpcd_next fp_value_fpcd_next. (exists fp_gap_fpcd_next_i. fp_gap_fpcd_next_i + S fp_i_fpcd_next = S n) -> (exists fp_gap_fpcd_next_j. fp_gap_fpcd_next_j + S fp_j_fpcd_next = S n) -> (((exists ff_h_fpcd_next_left. ff_h_fpcd_next_left + S (fp_value_fpcd_next) = S ((S (fp_i_fpcd_next)) * c)) /\ exists ff_q_fpcd_next_left. b = ff_q_fpcd_next_left * S ((S (fp_i_fpcd_next)) * c) + (fp_value_fpcd_next))) -> (((exists ff_h_fpcd_next_right. ff_h_fpcd_next_right + S (fp_value_fpcd_next) = S ((S (fp_j_fpcd_next)) * c)) /\ exists ff_q_fpcd_next_right. b = ff_q_fpcd_next_right * S ((S (fp_j_fpcd_next)) * c) + (fp_value_fpcd_next))) -> fp_i_fpcd_next = fp_j_fpcd_next)

Constructive proof overview

Generated structural guide

An injective decoded prefix stays injective when its new final value has no earlier occurrence.

The unchanged tactic script uses 2 declared prerequisites and contains 77 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

TS000R finite_prefix_collision_or_injective

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

77 script commands · 27 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.

01Fix variables and assumptionsL1–10

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 v
  5. L5
    intro holdinjective
  6. L6
    intro hlast
  7. L7
    intro hfresh
  8. L8
    intro i
  9. L9
    intro j
  10. L10
    intro y
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hibound
  2. L12
    intro hjbound
  3. L13
    intro hleft
  4. L14
    intro hright
03Establish hiL15–19

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. L15
    have hi : i = n \/ exists gap. gap + S i = n
  2. L16
    specialize finite_lt_succ_eq_or_lt n
  3. L17
    specialize finite_lt_succ_eq_or_lt i
  4. L18
    apply finite_lt_succ_eq_or_lt
  5. L19
    exact hibound
04Establish hjL20–24

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. L20
    have hj : j = n \/ exists gap. gap + S j = n
  2. L21
    specialize finite_lt_succ_eq_or_lt n
  3. L22
    specialize finite_lt_succ_eq_or_lt j
  4. L23
    apply finite_lt_succ_eq_or_lt
  5. L24
    exact hjbound
05Separate the logical casesL25–26

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

  1. L25
    cases hi
  2. L26
    cases hj
06Calculate and transport equalitiesL27–27

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

  1. L27
    trans n
07Use earlier factsL28–28

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

  1. L28
    exact hi_left
08Calculate and transport equalitiesL29–29

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

  1. L29
    symm
09Use earlier factsL30–30

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

  1. L30
    exact hj_left
10Separate the logical casesL31–31

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

  1. L31
    exfalso
11Use earlier factsL32–32

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

  1. L32
    apply hfresh
12Construct an explicit witnessL33–33

Supply the displayed value, then prove that it has the required property.

  1. L33
    exists j
13Separate the logical casesL34–34

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

  1. L34
    split
14Use earlier factsL35–35

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

  1. L35
    exact hj_right
15Establish hsameL36–45

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

  1. L36
    have hsame : y = v
  2. L37
    specialize beta_at_unique b
  3. L38
    specialize beta_at_unique c
  4. L39
    specialize beta_at_unique n
  5. L40
    specialize beta_at_unique y
  6. L41
    specialize beta_at_unique v
  7. L42
    apply beta_at_unique
  8. L43
    rewrite hi_left at hleft
  9. L44
    rewrite hi_left at hleft
  10. L45
    exact hleft
16Use earlier factsL46–46

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

  1. L46
    exact hlast
17Calculate and transport equalitiesL47–48

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

  1. L47
    rewrite hsame at hright
  2. L48
    rewrite hsame at hright
18Use earlier factsL49–49

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

  1. L49
    exact hright
19Separate the logical casesL50–51

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

  1. L50
    cases hj
  2. L51
    exfalso
20Use earlier factsL52–52

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

  1. L52
    apply hfresh
21Construct an explicit witnessL53–53

Supply the displayed value, then prove that it has the required property.

  1. L53
    exists i
22Separate the logical casesL54–54

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

  1. L54
    split
23Use earlier factsL55–55

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

  1. L55
    exact hi_right
24Establish hsameL56–65

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

  1. L56
    have hsame : y = v
  2. L57
    specialize beta_at_unique b
  3. L58
    specialize beta_at_unique c
  4. L59
    specialize beta_at_unique n
  5. L60
    specialize beta_at_unique y
  6. L61
    specialize beta_at_unique v
  7. L62
    apply beta_at_unique
  8. L63
    rewrite hj_left at hright
  9. L64
    rewrite hj_left at hright
  10. L65
    exact hright
25Use earlier factsL66–66

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

  1. L66
    exact hlast
26Calculate and transport equalitiesL67–68

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

  1. L67
    rewrite hsame at hleft
  2. L68
    rewrite hsame at hleft
27Use earlier factsL69–77

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

  1. L69
    exact hleft
  2. L70
    specialize holdinjective i
  3. L71
    specialize holdinjective j
  4. L72
    specialize holdinjective y
  5. L73
    apply holdinjective
  6. L74
    exact hi_right
  7. L75
    exact hj_right
  8. L76
    exact hleft
  9. L77
    exact hright

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro v
  5. 0005intro holdinjective
  6. 0006intro hlast
  7. 0007intro hfresh
  8. 0008intro i
  9. 0009intro j
  10. 0010intro y
  11. 0011intro hibound
  12. 0012intro hjbound
  13. 0013intro hleft
  14. 0014intro hright
  15. 0015have hi : i = n \/ exists gap. gap + S i = n
  16. 0016specialize finite_lt_succ_eq_or_lt n
  17. 0017specialize finite_lt_succ_eq_or_lt i
  18. 0018apply finite_lt_succ_eq_or_lt
  19. 0019exact hibound
  20. 0020have hj : j = n \/ exists gap. gap + S j = n
  21. 0021specialize finite_lt_succ_eq_or_lt n
  22. 0022specialize finite_lt_succ_eq_or_lt j
  23. 0023apply finite_lt_succ_eq_or_lt
  24. 0024exact hjbound
  25. 0025cases hi
  26. 0026cases hj
  27. 0027trans n
  28. 0028exact hi_left
  29. 0029symm
  30. 0030exact hj_left
  31. 0031exfalso
  32. 0032apply hfresh
  33. 0033exists j
  34. 0034split
  35. 0035exact hj_right
  36. 0036have hsame : y = v
  37. 0037specialize beta_at_unique b
  38. 0038specialize beta_at_unique c
  39. 0039specialize beta_at_unique n
  40. 0040specialize beta_at_unique y
  41. 0041specialize beta_at_unique v
  42. 0042apply beta_at_unique
  43. 0043rewrite hi_left at hleft
  44. 0044rewrite hi_left at hleft
  45. 0045exact hleft
  46. 0046exact hlast
  47. 0047rewrite hsame at hright
  48. 0048rewrite hsame at hright
  49. 0049exact hright
  50. 0050cases hj
  51. 0051exfalso
  52. 0052apply hfresh
  53. 0053exists i
  54. 0054split
  55. 0055exact hi_right
  56. 0056have hsame : y = v
  57. 0057specialize beta_at_unique b
  58. 0058specialize beta_at_unique c
  59. 0059specialize beta_at_unique n
  60. 0060specialize beta_at_unique y
  61. 0061specialize beta_at_unique v
  62. 0062apply beta_at_unique
  63. 0063rewrite hj_left at hright
  64. 0064rewrite hj_left at hright
  65. 0065exact hright
  66. 0066exact hlast
  67. 0067rewrite hsame at hleft
  68. 0068rewrite hsame at hleft
  69. 0069exact hleft
  70. 0070specialize holdinjective i
  71. 0071specialize holdinjective j
  72. 0072specialize holdinjective y
  73. 0073apply holdinjective
  74. 0074exact hi_right
  75. 0075exact hj_right
  76. 0076exact hleft
  77. 0077exact hright