PA002F · theorem

beta_at_unique

Stable checked-use theorem · independently closed

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

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. ∀ i. ∀ x. ∀ y. BetaAt(b,c,i,x) → BetaAt(b,c,i,y) → x = y

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

PD0013 BetaAt

2 occurrences

In local proof propositions

none

0 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA000H mul_comm PA002E division_remainder_unique

Direct theorem 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

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

37 script commands · 8 reading checkpoints · 3 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 (2)
mul commdivision remainder unique
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro i
  4. L4
    intro x
  5. L5
    intro y
  6. L6
    intro hx
  7. L7
    intro hy
02Separate the logical casesL8–11

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

  1. L8
    cases hx
  2. L9
    cases hy
  3. L10
    cases hx_right
  4. L11
    cases hy_right
03Establish hdxL12–17

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

  1. L12
    have hdx : b = S ((S i) * c) * x1 + x
  2. L13
    trans x1 * S ((S i) * c) + x
  3. L14
    exact hx_right_witness
  4. L15
    congr
  5. L16
    apply mul_comm
  6. L17
    refl
04Establish hdyL18–27

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

  1. L18
    have hdy : b = S ((S i) * c) * x2 + y
  2. L19
    trans x2 * S ((S i) * c) + y
  3. L20
    exact hy_right_witness
  4. L21
    congr
  5. L22
    apply mul_comm
  6. L23
    refl
  7. L24
    specialize division_remainder_unique (S ((S i) * c))
  8. L25
    specialize division_remainder_unique b
  9. L26
    specialize division_remainder_unique x1
  10. L27
    specialize division_remainder_unique x
05Use earlier factsL28–29

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

  1. L28
    specialize division_remainder_unique x2
  2. L29
    specialize division_remainder_unique y
06Establish huniqL30–35

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

  1. L30
    have huniq : x1 = x2 /\ x = y
  2. L31
    apply division_remainder_unique
  3. L32
    exact hdx
  4. L33
    exact hx_left
  5. L34
    exact hdy
  6. L35
    exact hy_left
07Separate the logical casesL36–36

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

  1. L36
    cases huniq
08Use earlier factsL37–37

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

  1. L37
    exact huniq_right

Library-wide reading audit

Original defined command ledger · 37 lines
  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