PA0096

finite_inverse_choice_injective

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

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

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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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