BT0042

beta_at_unique

Stable · empty-context checked

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

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

Direct prerequisites: mul_comm, division_remainder_unique. The authored body proceeds by case analysis (5), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT001U division_remainder_unique

Direct dependents

BT005A beta_exclusive_recode_congruence_step BT005G beta_product_functional BT005I beta_product_zero BT005J beta_product_succ_decompose BT0069 beta_factor_divides_product BT007X beta_repeat_entry_eq BT0087 beta_range_entry_eq BT008B beta_sum_trace_functional BT008E beta_sum_zero BT008F beta_sum_succ_decompose BT008O bit_count_succ_decompose BT00JB eisenstein_initial_segment_decoded_choice BT00JC beta_all_one_bit_count_exact BT00S1 power_quotient_prefix_transport BT00SJ power_quotient_prefix_decoded_divrem BT00SR beta_sum_succ_last_zero BT00T9 beta_pascal_zero_row_pointwise_functional BT00TA beta_pascal_row_step_pointwise_functional BT00TB beta_pascal_table_row_pointwise_functional BT00TE choose_zero BT00TF beta_pascal_table_diagonal_boundary BT00TH beta_pascal_table_successor_cell_recurrence BT00UD primorial_succ_decompose BT00UW primorial_interval_factor_prefix_shift BT00VE primorial_interval_pairwise_coprime BT00VF primorial_interval_divides_choose_between BT00Y3 beta_sum_double_carry_exact BT00Y5 central_binom_prime_power_contribution_le_double BT00YC double_quotient_carry_prefix_entries_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients BT00YW prime_contribution_prefix_pairwise_coprime BT00YY prime_contribution_product_divides BT010P prime_contribution_interval_prefix_shift BT010Y no_bertrand_small_contribution_product_le_power BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0112 no_bertrand_high_contribution_interval_eq_one

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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