TS000L · theorem body

finite_bounded_into_oversized_not_injective

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

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

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. ∀ n. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) → Lt(n,l) → ¬InjectivePrefix(b,c,l)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix PD0025 InjectivePrefix PD0026 SurjectivePrefix PD0027 ContainsPrefix
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

lt_to_le · Stable closed lt_of_lt_of_le · Stable closed finite_bounded_injective_surjective · Stable closed lt_irrefl_expanded · Stable closed

Direct theorem dependents

TS000M floor_square_oversized_bounded_grid_not_injective TS000N finite_bounded_into_collision_from_constructive_decision

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
  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(b,c,n)Original native command in the exact edition
  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 : Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  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(b,c,n)Original native command in the exact edition
  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(b,c,n)Original native command in the exact edition
  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 : ∃ v. BetaAt(b,c,n,v) ∧ Lt(v,n)Definitions: BetaAt(b,c,n,v)Lt(v,n)Original native command in the exact edition
  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 : ContainsPrefix(b,c,n,x)Definitions: ContainsPrefix(b,c,n,x)Original native command in the exact edition
  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 defined 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 : Le(n,l)
    Exact native replay linehave 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 : BoundedPrefix(b,c,n)
    Exact native replay linehave 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 : Lt(i,l)
    Exact native replay linehave 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 : InjectivePrefix(b,c,n)
    Exact native replay linehave 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 : SurjectivePrefix(b,c,n)
    Exact native replay linehave 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 : ∃ v. BetaAt(b,c,n,v) ∧ Lt(v,n)
    Exact native replay linehave 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 : ContainsPrefix(b,c,n,x)
    Exact native replay linehave 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