PA0096 · theorem

finite_inverse_choice_injective

Alpha v34 checked-use theorem · independently closed; not Stable

A beta-coded choice of source preimages is injective by functionality of the source code.

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. ∀ z. ∀ d. ∀ n. (∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))) → InjectivePrefix(z,d,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix

5 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

14 occurrences

Exact expanded native-PA statement
forall b c l z d n. (forall fom_value_injective_choice. (exists fom_gap_injective_choice_value_bound. fom_gap_injective_choice_value_bound + S (fom_value_injective_choice) = n) -> exists fom_index_injective_choice. ((((exists fom_beta_height_injective_choice_choice_entry. fom_beta_height_injective_choice_choice_entry + S (fom_index_injective_choice) = S ((S (fom_value_injective_choice)) * d)) /\ exists fom_beta_quotient_injective_choice_choice_entry. z = fom_beta_quotient_injective_choice_choice_entry * S ((S (fom_value_injective_choice)) * d) + (fom_index_injective_choice))) /\ ((exists fom_gap_injective_choice_index_bound. fom_gap_injective_choice_index_bound + S (fom_index_injective_choice) = l) /\ (((exists fom_beta_height_injective_choice_source_entry. fom_beta_height_injective_choice_source_entry + S (fom_value_injective_choice) = S ((S (fom_index_injective_choice)) * c)) /\ exists fom_beta_quotient_injective_choice_source_entry. b = fom_beta_quotient_injective_choice_source_entry * S ((S (fom_index_injective_choice)) * c) + (fom_value_injective_choice)))))) -> (forall fp_i_injective_result fp_j_injective_result fp_value_injective_result. (exists fp_gap_injective_result_i. fp_gap_injective_result_i + S fp_i_injective_result = n) -> (exists fp_gap_injective_result_j. fp_gap_injective_result_j + S fp_j_injective_result = n) -> (((exists ff_h_injective_result_left. ff_h_injective_result_left + S (fp_value_injective_result) = S ((S (fp_i_injective_result)) * d)) /\ exists ff_q_injective_result_left. z = ff_q_injective_result_left * S ((S (fp_i_injective_result)) * d) + (fp_value_injective_result))) -> (((exists ff_h_injective_result_right. ff_h_injective_result_right + S (fp_value_injective_result) = S ((S (fp_j_injective_result)) * d)) /\ exists ff_q_injective_result_right. z = ff_q_injective_result_right * S ((S (fp_j_injective_result)) * d) + (fp_value_injective_result))) -> fp_i_injective_result = fp_j_injective_result)

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique

Direct theorem dependents

PA0097 finite_short_cover_impossible

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

65 script commands · 11 reading checkpoints · 7 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.

Named ingredients (1)
beta at unique
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 l
  4. L4
    intro z
  5. L5
    intro d
  6. L6
    intro n
  7. L7
    intro hchoice
  8. L8
    intro i
  9. L9
    intro j
  10. L10
    intro v
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hi
  2. L12
    intro hj
  3. L13
    intro hvi
  4. L14
    intro hvj
03Establish hchoice_leftL15–16

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

  1. L15
    have hchoice_left : ∀ fom_value_injective_choice_left. Lt(fom_value_injective_choice_left,n) → ∃ x. BetaAt(z,d,fom_value_injective_choice_left,x) ∧ (Lt(x,l) ∧ BetaAt(b,c,x,fom_value_injective_choice_left))Definitions: Lt(fom_value_injective_choice_left,n)BetaAt(z,d,fom_value_injective_choice_left,x)Lt(x,l)BetaAt(b,c,x,fom_value_injective_choice_left)Original native command in the exact edition
  2. L16
    exact hchoice
04Establish hchoice_rightL17–19

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

  1. L17
    have hchoice_right : ∀ fom_value_injective_choice_right. Lt(fom_value_injective_choice_right,n) → ∃ x. BetaAt(z,d,fom_value_injective_choice_right,x) ∧ (Lt(x,l) ∧ BetaAt(b,c,x,fom_value_injective_choice_right))Definitions: Lt(fom_value_injective_choice_right,n)BetaAt(z,d,fom_value_injective_choice_right,x)Lt(x,l)BetaAt(b,c,x,fom_value_injective_choice_right)Original native command in the exact edition
  2. L18
    exact hchoice
  3. L19
    specialize hchoice_left i
05Establish hleftL20–23

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

  1. L20
    have hleft : ∃ a. BetaAt(z,d,i,a) ∧ (Lt(a,l) ∧ BetaAt(b,c,a,i))Definitions: BetaAt(z,d,i,a)Lt(a,l)BetaAt(b,c,a,i)Original native command in the exact edition
  2. L21
    apply hchoice_left
  3. L22
    exact hi
  4. L23
    specialize hchoice_right j
06Establish hrightL24–26

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

  1. L24
    have hright : ∃ a. BetaAt(z,d,j,a) ∧ (Lt(a,l) ∧ BetaAt(b,c,a,j))Definitions: BetaAt(z,d,j,a)Lt(a,l)BetaAt(b,c,a,j)Original native command in the exact edition
  2. L25
    apply hchoice_right
  3. L26
    exact hj
07Separate the logical casesL27–32

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

  1. L27
    cases hleft
  2. L28
    cases hleft_witness
  3. L29
    cases hleft_witness_right
  4. L30
    cases hright
  5. L31
    cases hright_witness
  6. L32
    cases hright_witness_right
08Establish hvxL33–41

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

  1. L33
    have hvx : v = x
  2. L34
    specialize beta_at_unique z
  3. L35
    specialize beta_at_unique d
  4. L36
    specialize beta_at_unique i
  5. L37
    specialize beta_at_unique v
  6. L38
    specialize beta_at_unique x
  7. L39
    apply beta_at_unique
  8. L40
    exact hvi
  9. L41
    exact hleft_witness_left
09Establish hvx1L42–50

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

  1. L42
    have hvx1 : v = x1
  2. L43
    specialize beta_at_unique z
  3. L44
    specialize beta_at_unique d
  4. L45
    specialize beta_at_unique j
  5. L46
    specialize beta_at_unique v
  6. L47
    specialize beta_at_unique x1
  7. L48
    apply beta_at_unique
  8. L49
    exact hvj
  9. L50
    exact hright_witness_left
10Establish hxxL51–60

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

  1. L51
    have hxx : x = x1
  2. L52
    trans v
  3. L53
    symm
  4. L54
    exact hvx
  5. L55
    exact hvx1
  6. L56
    rewrite hxx at hleft_witness_right_right
  7. L57
    rewrite hxx at hleft_witness_right_right
  8. L58
    specialize beta_at_unique b
  9. L59
    specialize beta_at_unique c
  10. L60
    specialize beta_at_unique x1
11Use earlier factsL61–65

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

  1. L61
    specialize beta_at_unique i
  2. L62
    specialize beta_at_unique j
  3. L63
    apply beta_at_unique
  4. L64
    exact hleft_witness_right_right
  5. L65
    exact hright_witness_right_right

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro z
  5. 0005intro d
  6. 0006intro n
  7. 0007intro hchoice
  8. 0008intro i
  9. 0009intro j
  10. 0010intro v
  11. 0011intro hi
  12. 0012intro hj
  13. 0013intro hvi
  14. 0014intro hvj
  15. 0015have hchoice_left : ∀ fom_value_injective_choice_left. Lt(fom_value_injective_choice_left,n) → ∃ x. BetaAt(z,d,fom_value_injective_choice_left,x) ∧ (Lt(x,l) ∧ BetaAt(b,c,x,fom_value_injective_choice_left))
    Exact native replay linehave hchoice_left : forall fom_value_injective_choice_left. (exists fom_gap_injective_choice_left_value_bound. fom_gap_injective_choice_left_value_bound + S (fom_value_injective_choice_left) = n) -> exists fom_index_injective_choice_left. ((((exists fom_beta_height_injective_choice_left_choice_entry. fom_beta_height_injective_choice_left_choice_entry + S (fom_index_injective_choice_left) = S ((S (fom_value_injective_choice_left)) * d)) /\ exists fom_beta_quotient_injective_choice_left_choice_entry. z = fom_beta_quotient_injective_choice_left_choice_entry * S ((S (fom_value_injective_choice_left)) * d) + (fom_index_injective_choice_left))) /\ ((exists fom_gap_injective_choice_left_index_bound. fom_gap_injective_choice_left_index_bound + S (fom_index_injective_choice_left) = l) /\ (((exists fom_beta_height_injective_choice_left_source_entry. fom_beta_height_injective_choice_left_source_entry + S (fom_value_injective_choice_left) = S ((S (fom_index_injective_choice_left)) * c)) /\ exists fom_beta_quotient_injective_choice_left_source_entry. b = fom_beta_quotient_injective_choice_left_source_entry * S ((S (fom_index_injective_choice_left)) * c) + (fom_value_injective_choice_left)))))
  16. 0016exact hchoice
  17. 0017have hchoice_right : ∀ fom_value_injective_choice_right. Lt(fom_value_injective_choice_right,n) → ∃ x. BetaAt(z,d,fom_value_injective_choice_right,x) ∧ (Lt(x,l) ∧ BetaAt(b,c,x,fom_value_injective_choice_right))
    Exact native replay linehave hchoice_right : forall fom_value_injective_choice_right. (exists fom_gap_injective_choice_right_value_bound. fom_gap_injective_choice_right_value_bound + S (fom_value_injective_choice_right) = n) -> exists fom_index_injective_choice_right. ((((exists fom_beta_height_injective_choice_right_choice_entry. fom_beta_height_injective_choice_right_choice_entry + S (fom_index_injective_choice_right) = S ((S (fom_value_injective_choice_right)) * d)) /\ exists fom_beta_quotient_injective_choice_right_choice_entry. z = fom_beta_quotient_injective_choice_right_choice_entry * S ((S (fom_value_injective_choice_right)) * d) + (fom_index_injective_choice_right))) /\ ((exists fom_gap_injective_choice_right_index_bound. fom_gap_injective_choice_right_index_bound + S (fom_index_injective_choice_right) = l) /\ (((exists fom_beta_height_injective_choice_right_source_entry. fom_beta_height_injective_choice_right_source_entry + S (fom_value_injective_choice_right) = S ((S (fom_index_injective_choice_right)) * c)) /\ exists fom_beta_quotient_injective_choice_right_source_entry. b = fom_beta_quotient_injective_choice_right_source_entry * S ((S (fom_index_injective_choice_right)) * c) + (fom_value_injective_choice_right)))))
  18. 0018exact hchoice
  19. 0019specialize hchoice_left i
  20. 0020have hleft : ∃ a. BetaAt(z,d,i,a) ∧ (Lt(a,l) ∧ BetaAt(b,c,a,i))
    Exact native replay linehave hleft : exists a. (((exists h. h + S a = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + a) /\ ((exists h. h + S a = l) /\ ((exists h. h + S i = S ((S a) * c)) /\ exists q. b = q * S ((S a) * c) + i)))
  21. 0021apply hchoice_left
  22. 0022exact hi
  23. 0023specialize hchoice_right j
  24. 0024have hright : ∃ a. BetaAt(z,d,j,a) ∧ (Lt(a,l) ∧ BetaAt(b,c,a,j))
    Exact native replay linehave hright : exists a. (((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a) /\ ((exists h. h + S a = l) /\ ((exists h. h + S j = S ((S a) * c)) /\ exists q. b = q * S ((S a) * c) + j)))
  25. 0025apply hchoice_right
  26. 0026exact hj
  27. 0027cases hleft
  28. 0028cases hleft_witness
  29. 0029cases hleft_witness_right
  30. 0030cases hright
  31. 0031cases hright_witness
  32. 0032cases hright_witness_right
  33. 0033have hvx : v = x
  34. 0034specialize beta_at_unique z
  35. 0035specialize beta_at_unique d
  36. 0036specialize beta_at_unique i
  37. 0037specialize beta_at_unique v
  38. 0038specialize beta_at_unique x
  39. 0039apply beta_at_unique
  40. 0040exact hvi
  41. 0041exact hleft_witness_left
  42. 0042have hvx1 : v = x1
  43. 0043specialize beta_at_unique z
  44. 0044specialize beta_at_unique d
  45. 0045specialize beta_at_unique j
  46. 0046specialize beta_at_unique v
  47. 0047specialize beta_at_unique x1
  48. 0048apply beta_at_unique
  49. 0049exact hvj
  50. 0050exact hright_witness_left
  51. 0051have hxx : x = x1
  52. 0052trans v
  53. 0053symm
  54. 0054exact hvx
  55. 0055exact hvx1
  56. 0056rewrite hxx at hleft_witness_right_right
  57. 0057rewrite hxx at hleft_witness_right_right
  58. 0058specialize beta_at_unique b
  59. 0059specialize beta_at_unique c
  60. 0060specialize beta_at_unique x1
  61. 0061specialize beta_at_unique i
  62. 0062specialize beta_at_unique j
  63. 0063apply beta_at_unique
  64. 0064exact hleft_witness_right_right
  65. 0065exact hright_witness_right_right