PA0096

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.

Exact expanded 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)

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (7), equality transport (2).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA0097 finite_short_cover_impossible

Formal native tactic body

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

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.

Named ingredients (1)
beta at unique

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–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: LtBetaAt
  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: LtBetaAt
  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 : 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)))
  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 : 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)))
  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 exact 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 : 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 : 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 : 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 : 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