PA002F

beta_at_unique

Stable checked-use theorem · independently closed

The decoded residue at a Gödel-beta position is unique.

Exact expanded PA statement

forall b c i x y. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y) -> x = y

Structural proof guide

Generated structural guide

The decoded residue at a Gödel-beta position is unique.

Use the direct prerequisites mul_comm, division_remainder_unique as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (3).

Referenced ingredients

PA000H mul_comm PA002E division_remainder_unique

Proof neighborhood

Direct dependencies

PA000H mul_comm PA002E division_remainder_unique

Direct dependents

PA002G beta_exclusive_recode_congruence_step PA0032 beta_range_entry_eq PA003Y beta_sum_succ_decompose PA0042 bit_count_succ_decompose PA0047 beta_sum_zero PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004C beta_repeat_entry_eq PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA004L finite_bounded_entry_lt PA004N beta_prefix_swap_last_reflect PA004W finite_bounded_injective_surjective PA0051 beta_product_functional PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA0054 beta_reindex_alignment_swap_last PA006K beta_sum_trace_functional PA007C gauss_signed_half_magnitude_injective PA007D beta_magnitude_predecessor_recode_exists PA007F beta_sign_factor_prefix_extend PA007I beta_sign_factor_product_power PA007K beta_pointwise_mul_prefix_extend PA007P gauss_signed_pointwise_mul_scale_mod PA007T beta_magnitude_predecessor_recode_reflect PA007V gauss_predecessor_half_range_aligned PA007W beta_product_reindex_fixed_last PA007X beta_product_permutation_invariant PA008C beta_successor_lift_exists PA008E prime_mul_index_map_injective PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod PA0096 finite_inverse_choice_injective PA0097 finite_short_cover_impossible PA0099 scaled_inverse_prefix_entry_sound PA009L beta_prefix_append_two_reflect PA009M beta_prefix_append_two_scaled_orbit_closed PA009X scaled_pair_order_successor_lift_adjacent_targets PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00AF inverse_prefix_entry_sound PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AT beta_prefix_append_two_orbit_closed PA00B7 paired_successor_lift_adjacent_units PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00CP gauss_eisenstein_prefix_pointwise_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00CU beta_sum_replace_balance PA00CV beta_sum_swap_last_invariant PA00CW beta_sum_reindex_fixed_last PA00CX beta_sum_permutation_invariant PA00DV eisenstein_initial_segment_decoded_choice PA00DW beta_all_one_bit_count_exact PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient PA00E6 eisenstein_rectangle_decoded_row_count PA00EA eisenstein_row_indicator_decoded_choice PA00ED eisenstein_transposed_column_pointwise_complement PA00EM eisenstein_transposed_column_count_decoded_witness PA00EN eisenstein_transposed_column_count_decoded_partition PA00F1 eisenstein_successor_row_split_decoded_add PA00F4 eisenstein_transposed_column_decoded_choice PA00F9 eisenstein_successor_terminal_bit_matches_last_column PA00FC eisenstein_fubini_universal

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003intro i
  4. 0004intro x
  5. 0005intro y
  6. 0006intro hx
  7. 0007intro hy
  8. 0008cases hx
  9. 0009cases hy
  10. 0010cases hx_right
  11. 0011cases hy_right
  12. 0012have hdx : b = S ((S i) * c) * x1 + x
  13. 0013trans x1 * S ((S i) * c) + x
  14. 0014exact hx_right_witness
  15. 0015congr
  16. 0016apply mul_comm
  17. 0017refl
  18. 0018have hdy : b = S ((S i) * c) * x2 + y
  19. 0019trans x2 * S ((S i) * c) + y
  20. 0020exact hy_right_witness
  21. 0021congr
  22. 0022apply mul_comm
  23. 0023refl
  24. 0024specialize division_remainder_unique (S ((S i) * c))
  25. 0025specialize division_remainder_unique b
  26. 0026specialize division_remainder_unique x1
  27. 0027specialize division_remainder_unique x
  28. 0028specialize division_remainder_unique x2
  29. 0029specialize division_remainder_unique y
  30. 0030have huniq : x1 = x2 /\ x = y
  31. 0031apply division_remainder_unique
  32. 0032exact hdx
  33. 0033exact hx_left
  34. 0034exact hdy
  35. 0035exact hy_left
  36. 0036cases huniq
  37. 0037exact huniq_right