TS000L

finite_bounded_into_oversized_not_injective

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

An explicitly bounded beta-coded map from a larger finite domain cannot be injective.

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 l n. (forall fom_index_ftsp_full_bounded. (exists fom_gap_ftsp_full_bounded_index_bound. fom_gap_ftsp_full_bounded_index_bound + S (fom_index_ftsp_full_bounded) = l) -> exists fom_value_ftsp_full_bounded. ((((exists fom_beta_height_ftsp_full_bounded_entry. fom_beta_height_ftsp_full_bounded_entry + S (fom_value_ftsp_full_bounded) = S ((S (fom_index_ftsp_full_bounded)) * c)) /\ exists fom_beta_quotient_ftsp_full_bounded_entry. b = fom_beta_quotient_ftsp_full_bounded_entry * S ((S (fom_index_ftsp_full_bounded)) * c) + (fom_value_ftsp_full_bounded))) /\ (exists fom_gap_ftsp_full_bounded_value_bound. fom_gap_ftsp_full_bounded_value_bound + S (fom_value_ftsp_full_bounded) = n))) -> (exists ftsp_gap_domain_overflow. ftsp_gap_domain_overflow + S (n) = l) -> ~(forall fp_i_ftsp_full_injective fp_j_ftsp_full_injective fp_value_ftsp_full_injective. (exists fp_gap_ftsp_full_injective_i. fp_gap_ftsp_full_injective_i + S fp_i_ftsp_full_injective = l) -> (exists fp_gap_ftsp_full_injective_j. fp_gap_ftsp_full_injective_j + S fp_j_ftsp_full_injective = l) -> (((exists ff_h_ftsp_full_injective_left. ff_h_ftsp_full_injective_left + S (fp_value_ftsp_full_injective) = S ((S (fp_i_ftsp_full_injective)) * c)) /\ exists ff_q_ftsp_full_injective_left. b = ff_q_ftsp_full_injective_left * S ((S (fp_i_ftsp_full_injective)) * c) + (fp_value_ftsp_full_injective))) -> (((exists ff_h_ftsp_full_injective_right. ff_h_ftsp_full_injective_right + S (fp_value_ftsp_full_injective) = S ((S (fp_j_ftsp_full_injective)) * c)) /\ exists ff_q_ftsp_full_injective_right. b = ff_q_ftsp_full_injective_right * S ((S (fp_j_ftsp_full_injective)) * c) + (fp_value_ftsp_full_injective))) -> fp_i_ftsp_full_injective = fp_j_ftsp_full_injective)

Constructive proof overview

Generated structural guide

An explicitly bounded beta-coded map from a larger finite domain cannot be injective.

The unchanged tactic script uses 4 declared prerequisites and contains 88 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

lt_to_le Stable theorem; checked-use authorized lt_of_lt_of_le Stable theorem; checked-use authorized finite_bounded_injective_surjective Stable theorem; checked-use authorized lt_irrefl_expanded Stable theorem; checked-use authorized

Direct dependents

TS000M floor_square_oversized_bounded_grid_not_injective TS000N finite_bounded_into_collision_from_constructive_decision

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

88 script commands · 16 reading checkpoints · 8 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hbounded
  6. L6
    intro hoverflow
  7. L7
    intro hinjective
02Establish hweakL8–12

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

  1. L8
    have hweak : exists k. k + n = l
  2. L9
    specialize lt_to_le n
  3. L10
    specialize lt_to_le l
  4. L11
    apply lt_to_le
  5. L12
    exact hoverflow
03Establish hsquareboundedL13–15

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hsquarebounded : BoundedPrefix(b,c,n)Definitions: BoundedPrefix
  2. L14
    intro i
  3. L15
    intro hi
04Establish hlargeL16–25

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

  1. L16
    have hlarge : exists k. k + S i = l
  2. L17
    specialize lt_of_lt_of_le i
  3. L18
    specialize lt_of_lt_of_le n
  4. L19
    specialize lt_of_lt_of_le l
  5. L20
    apply lt_of_lt_of_le
  6. L21
    exact hi
  7. L22
    exact hweak
  8. L23
    specialize hbounded i
  9. L24
    apply hbounded
  10. L25
    exact hlarge
05Establish hsquareinjectiveL26–35

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hsquareinjective : InjectivePrefix(b,c,n)Definitions: InjectivePrefix
  2. L27
    intro i
  3. L28
    intro j
  4. L29
    intro v
  5. L30
    intro hi
  6. L31
    intro hj
  7. L32
    intro hleft
  8. L33
    intro hright
  9. L34
    specialize hinjective i
  10. L35
    specialize hinjective j
06Use earlier factsL36–45

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

  1. L36
    specialize hinjective v
  2. L37
    apply hinjective
  3. L38
    specialize lt_of_lt_of_le i
  4. L39
    specialize lt_of_lt_of_le n
  5. L40
    specialize lt_of_lt_of_le l
  6. L41
    apply lt_of_lt_of_le
  7. L42
    exact hi
  8. L43
    exact hweak
  9. L44
    specialize lt_of_lt_of_le j
  10. L45
    specialize lt_of_lt_of_le n
07Use earlier factsL46–51

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

  1. L46
    specialize lt_of_lt_of_le l
  2. L47
    apply lt_of_lt_of_le
  3. L48
    exact hj
  4. L49
    exact hweak
  5. L50
    exact hleft
  6. L51
    exact hright
08Establish hsurjectiveL52–58

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

  1. L52
    have hsurjective : SurjectivePrefix(b,c,n)Definitions: SurjectivePrefix
  2. L53
    specialize finite_bounded_injective_surjective n
  3. L54
    specialize finite_bounded_injective_surjective b
  4. L55
    specialize finite_bounded_injective_surjective c
  5. L56
    apply finite_bounded_injective_surjective
  6. L57
    exact hsquarebounded
  7. L58
    exact hsquareinjective
09Establish hlastL59–62

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

  1. L59
    have hlast : exists v. ((((exists ff_h_ftsp_last_entry. ff_h_ftsp_last_entry + S (v) = S ((S (n)) * c)) /\ exists ff_q_ftsp_last_entry. b = ff_q_ftsp_last_entry * S ((S (n)) * c) + (v))) /\ (exists ftsp_gap_last_value. ftsp_gap_last_value + S (v) = n))
  2. L60
    specialize hbounded n
  3. L61
    apply hbounded
  4. L62
    exact hoverflow
10Separate the logical casesL63–64

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

  1. L63
    cases hlast
  2. L64
    cases hlast_witness
11Establish hearlierL65–68

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

  1. L65
    have hearlier : exists i. ((exists ftsp_gap_earlier_index. ftsp_gap_earlier_index + S (i) = n) /\ (((exists ff_h_ftsp_earlier_entry. ff_h_ftsp_earlier_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_ftsp_earlier_entry. b = ff_q_ftsp_earlier_entry * S ((S (i)) * c) + (x))))
  2. L66
    specialize hsurjective x
  3. L67
    apply hsurjective
  4. L68
    exact hlast_witness_right
12Separate the logical casesL69–70

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

  1. L69
    cases hearlier
  2. L70
    cases hearlier_witness
13Establish hequalL71–80

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

  1. L71
    have hequal : x1 = n
  2. L72
    specialize hinjective x1
  3. L73
    specialize hinjective n
  4. L74
    specialize hinjective x
  5. L75
    apply hinjective
  6. L76
    specialize lt_of_lt_of_le x1
  7. L77
    specialize lt_of_lt_of_le n
  8. L78
    specialize lt_of_lt_of_le l
  9. L79
    apply lt_of_lt_of_le
  10. L80
    exact hearlier_witness_left
14Use earlier factsL81–84

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

  1. L81
    exact hweak
  2. L82
    exact hoverflow
  3. L83
    exact hearlier_witness_right
  4. L84
    exact hlast_witness_left
15Calculate and transport equalitiesL85–85

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

  1. L85
    rewrite hequal at hearlier_witness_left
16Use earlier factsL86–88

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

  1. L86
    specialize lt_irrefl_expanded n
  2. L87
    apply lt_irrefl_expanded
  3. L88
    exact hearlier_witness_left

Library-wide reading audit

Original exact command ledger · 88 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hbounded
  6. 0006intro hoverflow
  7. 0007intro hinjective
  8. 0008have hweak : exists k. k + n = l
  9. 0009specialize lt_to_le n
  10. 0010specialize lt_to_le l
  11. 0011apply lt_to_le
  12. 0012exact hoverflow
  13. 0013have hsquarebounded : forall fp_i_ftsp_square_bounded. (exists fp_gap_ftsp_square_bounded_index. fp_gap_ftsp_square_bounded_index + S fp_i_ftsp_square_bounded = n) -> exists fp_value_ftsp_square_bounded. ((((exists ff_h_ftsp_square_bounded_entry. ff_h_ftsp_square_bounded_entry + S (fp_value_ftsp_square_bounded) = S ((S (fp_i_ftsp_square_bounded)) * c)) /\ exists ff_q_ftsp_square_bounded_entry. b = ff_q_ftsp_square_bounded_entry * S ((S (fp_i_ftsp_square_bounded)) * c) + (fp_value_ftsp_square_bounded))) /\ (exists fp_gap_ftsp_square_bounded_value. fp_gap_ftsp_square_bounded_value + S fp_value_ftsp_square_bounded = n))
  14. 0014intro i
  15. 0015intro hi
  16. 0016have hlarge : exists k. k + S i = l
  17. 0017specialize lt_of_lt_of_le i
  18. 0018specialize lt_of_lt_of_le n
  19. 0019specialize lt_of_lt_of_le l
  20. 0020apply lt_of_lt_of_le
  21. 0021exact hi
  22. 0022exact hweak
  23. 0023specialize hbounded i
  24. 0024apply hbounded
  25. 0025exact hlarge
  26. 0026have hsquareinjective : forall fp_i_ftsp_square_injective fp_j_ftsp_square_injective fp_value_ftsp_square_injective. (exists fp_gap_ftsp_square_injective_i. fp_gap_ftsp_square_injective_i + S fp_i_ftsp_square_injective = n) -> (exists fp_gap_ftsp_square_injective_j. fp_gap_ftsp_square_injective_j + S fp_j_ftsp_square_injective = n) -> (((exists ff_h_ftsp_square_injective_left. ff_h_ftsp_square_injective_left + S (fp_value_ftsp_square_injective) = S ((S (fp_i_ftsp_square_injective)) * c)) /\ exists ff_q_ftsp_square_injective_left. b = ff_q_ftsp_square_injective_left * S ((S (fp_i_ftsp_square_injective)) * c) + (fp_value_ftsp_square_injective))) -> (((exists ff_h_ftsp_square_injective_right. ff_h_ftsp_square_injective_right + S (fp_value_ftsp_square_injective) = S ((S (fp_j_ftsp_square_injective)) * c)) /\ exists ff_q_ftsp_square_injective_right. b = ff_q_ftsp_square_injective_right * S ((S (fp_j_ftsp_square_injective)) * c) + (fp_value_ftsp_square_injective))) -> fp_i_ftsp_square_injective = fp_j_ftsp_square_injective
  27. 0027intro i
  28. 0028intro j
  29. 0029intro v
  30. 0030intro hi
  31. 0031intro hj
  32. 0032intro hleft
  33. 0033intro hright
  34. 0034specialize hinjective i
  35. 0035specialize hinjective j
  36. 0036specialize hinjective v
  37. 0037apply hinjective
  38. 0038specialize lt_of_lt_of_le i
  39. 0039specialize lt_of_lt_of_le n
  40. 0040specialize lt_of_lt_of_le l
  41. 0041apply lt_of_lt_of_le
  42. 0042exact hi
  43. 0043exact hweak
  44. 0044specialize lt_of_lt_of_le j
  45. 0045specialize lt_of_lt_of_le n
  46. 0046specialize lt_of_lt_of_le l
  47. 0047apply lt_of_lt_of_le
  48. 0048exact hj
  49. 0049exact hweak
  50. 0050exact hleft
  51. 0051exact hright
  52. 0052have hsurjective : forall fp_value_ftsp_square_surjective. (exists fp_gap_ftsp_square_surjective_value. fp_gap_ftsp_square_surjective_value + S fp_value_ftsp_square_surjective = n) -> exists fp_i_ftsp_square_surjective. ((exists fp_gap_ftsp_square_surjective_index. fp_gap_ftsp_square_surjective_index + S fp_i_ftsp_square_surjective = n) /\ (((exists ff_h_ftsp_square_surjective_entry. ff_h_ftsp_square_surjective_entry + S (fp_value_ftsp_square_surjective) = S ((S (fp_i_ftsp_square_surjective)) * c)) /\ exists ff_q_ftsp_square_surjective_entry. b = ff_q_ftsp_square_surjective_entry * S ((S (fp_i_ftsp_square_surjective)) * c) + (fp_value_ftsp_square_surjective))))
  53. 0053specialize finite_bounded_injective_surjective n
  54. 0054specialize finite_bounded_injective_surjective b
  55. 0055specialize finite_bounded_injective_surjective c
  56. 0056apply finite_bounded_injective_surjective
  57. 0057exact hsquarebounded
  58. 0058exact hsquareinjective
  59. 0059have hlast : exists v. ((((exists ff_h_ftsp_last_entry. ff_h_ftsp_last_entry + S (v) = S ((S (n)) * c)) /\ exists ff_q_ftsp_last_entry. b = ff_q_ftsp_last_entry * S ((S (n)) * c) + (v))) /\ (exists ftsp_gap_last_value. ftsp_gap_last_value + S (v) = n))
  60. 0060specialize hbounded n
  61. 0061apply hbounded
  62. 0062exact hoverflow
  63. 0063cases hlast
  64. 0064cases hlast_witness
  65. 0065have hearlier : exists i. ((exists ftsp_gap_earlier_index. ftsp_gap_earlier_index + S (i) = n) /\ (((exists ff_h_ftsp_earlier_entry. ff_h_ftsp_earlier_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_ftsp_earlier_entry. b = ff_q_ftsp_earlier_entry * S ((S (i)) * c) + (x))))
  66. 0066specialize hsurjective x
  67. 0067apply hsurjective
  68. 0068exact hlast_witness_right
  69. 0069cases hearlier
  70. 0070cases hearlier_witness
  71. 0071have hequal : x1 = n
  72. 0072specialize hinjective x1
  73. 0073specialize hinjective n
  74. 0074specialize hinjective x
  75. 0075apply hinjective
  76. 0076specialize lt_of_lt_of_le x1
  77. 0077specialize lt_of_lt_of_le n
  78. 0078specialize lt_of_lt_of_le l
  79. 0079apply lt_of_lt_of_le
  80. 0080exact hearlier_witness_left
  81. 0081exact hweak
  82. 0082exact hoverflow
  83. 0083exact hearlier_witness_right
  84. 0084exact hlast_witness_left
  85. 0085rewrite hequal at hearlier_witness_left
  86. 0086specialize lt_irrefl_expanded n
  87. 0087apply lt_irrefl_expanded
  88. 0088exact hearlier_witness_left