BT0042 · Bertrand theorem

beta_at_unique

Stable checked-use theorem · independently kernel verified

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. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

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

BT0006 mul_comm BT001U division_remainder_unique

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

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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