BT00JC · Bertrand theorem

beta_all_one_bit_count_exact

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A length-k beta prefix consisting only of ones has BitCount k.

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. ∀ k. ∀ n. Repeat(b,c,1,k) → BitCount(b,c,k,n) → n = k

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

PD0017 BitCount PD0019 Repeat

2 occurrences

In local proof propositions

PD0013 BetaAt PD0017 BitCount PD0019 Repeat

4 occurrences

Exact expanded native-PA statement
forall b c k n. (forall eis_one_index_initial_segment_all_one_source. (exists eis_lt_gap_initial_segment_all_one_source_bound. eis_lt_gap_initial_segment_all_one_source_bound + S (eis_one_index_initial_segment_all_one_source) = k) -> (((exists ff_h_eis_initial_segment_all_one_source_decoded. ff_h_eis_initial_segment_all_one_source_decoded + S (1) = S ((S (eis_one_index_initial_segment_all_one_source)) * c)) /\ exists ff_q_eis_initial_segment_all_one_source_decoded. b = ff_q_eis_initial_segment_all_one_source_decoded * S ((S (eis_one_index_initial_segment_all_one_source)) * c) + (1)))) -> (((exists ff_u_initial_segment_all_one_count_sum ff_v_initial_segment_all_one_count_sum. ((((exists ff_h_initial_segment_all_one_count_sum_start. ff_h_initial_segment_all_one_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_start. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_start * S ((S (0)) * ff_v_initial_segment_all_one_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_all_one_count_sum_terminal. ff_h_initial_segment_all_one_count_sum_terminal + S (n) = S ((S (k)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_terminal. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_all_one_count_sum) + (n))) /\ forall ff_i_initial_segment_all_one_count_sum. (exists ff_lt_initial_segment_all_one_count_sum_bound. ff_lt_initial_segment_all_one_count_sum_bound + S ff_i_initial_segment_all_one_count_sum = k) -> exists ff_a_initial_segment_all_one_count_sum ff_r_initial_segment_all_one_count_sum ff_s_initial_segment_all_one_count_sum. ((((exists ff_h_initial_segment_all_one_count_sum_summand. ff_h_initial_segment_all_one_count_sum_summand + S (ff_a_initial_segment_all_one_count_sum) = S ((S (ff_i_initial_segment_all_one_count_sum)) * c)) /\ exists ff_q_initial_segment_all_one_count_sum_summand. b = ff_q_initial_segment_all_one_count_sum_summand * S ((S (ff_i_initial_segment_all_one_count_sum)) * c) + (ff_a_initial_segment_all_one_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_count_sum_partial. ff_h_initial_segment_all_one_count_sum_partial + S (ff_r_initial_segment_all_one_count_sum) = S ((S (ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_partial. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_partial * S ((S (ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum) + (ff_r_initial_segment_all_one_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_count_sum_successor. ff_h_initial_segment_all_one_count_sum_successor + S (ff_s_initial_segment_all_one_count_sum) = S ((S (S ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum)) /\ exists ff_q_initial_segment_all_one_count_sum_successor. ff_u_initial_segment_all_one_count_sum = ff_q_initial_segment_all_one_count_sum_successor * S ((S (S ff_i_initial_segment_all_one_count_sum)) * ff_v_initial_segment_all_one_count_sum) + (ff_s_initial_segment_all_one_count_sum))) /\ ff_s_initial_segment_all_one_count_sum = ff_r_initial_segment_all_one_count_sum + ff_a_initial_segment_all_one_count_sum)))))) /\ (forall ff_i_initial_segment_all_one_count_bits. (exists ff_lt_initial_segment_all_one_count_bits_bound. ff_lt_initial_segment_all_one_count_bits_bound + S ff_i_initial_segment_all_one_count_bits = k) -> exists ff_bit_initial_segment_all_one_count_bits. ((((exists ff_h_initial_segment_all_one_count_bits_decoded. ff_h_initial_segment_all_one_count_bits_decoded + S (ff_bit_initial_segment_all_one_count_bits) = S ((S (ff_i_initial_segment_all_one_count_bits)) * c)) /\ exists ff_q_initial_segment_all_one_count_bits_decoded. b = ff_q_initial_segment_all_one_count_bits_decoded * S ((S (ff_i_initial_segment_all_one_count_bits)) * c) + (ff_bit_initial_segment_all_one_count_bits))) /\ (ff_bit_initial_segment_all_one_count_bits = 0 \/ ff_bit_initial_segment_all_one_count_bits = 1))))) -> n = k

Proof neighborhood

Direct theorem prerequisites

BT008N bit_count_zero BT008O bit_count_succ_decompose BT008J all_bits_prefix_succ BT0042 beta_at_unique BT0018 le_succ BT000E le_refl

Direct theorem dependents

BT00JD eisenstein_initial_segment_bit_count_functional

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

62 script commands · 11 reading checkpoints · 5 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 (5)
bit count zerobit count succ decomposebeta at uniquele succle refl
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on kL3–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction k
  2. L4
    intro n
  3. L5
    intro hone
  4. L6
    intro hcount
  5. L7
    specialize bit_count_zero b
  6. L8
    specialize bit_count_zero c
  7. L9
    specialize bit_count_zero 0
  8. L10
    specialize bit_count_zero n
  9. L11
    apply bit_count_zero
  10. L12
    refl
03Use earlier factsL13–13

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

  1. L13
    exact hcount
04Fix variables and assumptionsL14–16

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

  1. L14
    intro n
  2. L15
    intro hone
  3. L16
    intro hcount
05Establish hdecompL17–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count succ decompose.

  1. L17
    have hdecomp : ∃ a. ∃ r. BetaAt(b,c,k,a) ∧ (BitCount(b,c,k,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))Definitions: BetaAt(b,c,k,a)BitCount(b,c,k,r)Original native command in the exact edition
  2. L18
    specialize bit_count_succ_decompose b
  3. L19
    specialize bit_count_succ_decompose c
  4. L20
    specialize bit_count_succ_decompose k
  5. L21
    specialize bit_count_succ_decompose (S k)
  6. L22
    specialize bit_count_succ_decompose n
  7. L23
    apply bit_count_succ_decompose
  8. L24
    refl
  9. L25
    exact hcount
06Separate the logical casesL26–30

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

  1. L26
    cases hdecomp
  2. L27
    cases hdecomp_witness
  3. L28
    cases hdecomp_witness_witness
  4. L29
    cases hdecomp_witness_witness_right
  5. L30
    cases hdecomp_witness_witness_right_right
07Establish hone_previousL31–39

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

  1. L31
    have hone_previous : Repeat(b,c,1,k)Definitions: Repeat(b,c,1,k)Original native command in the exact edition
  2. L32
    intro j
  3. L33
    intro hj
  4. L34
    specialize hone j
  5. L35
    apply hone
  6. L36
    specialize le_succ (S j)
  7. L37
    specialize le_succ k
  8. L38
    apply le_succ
  9. L39
    exact hj
08Establish hrL40–44

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

  1. L40
    have hr : x1 = k
  2. L41
    specialize IH x1
  3. L42
    apply IH
  4. L43
    exact hone_previous
  5. L44
    exact hdecomp_witness_witness_right_left
09Establish hlast_oneL45–49

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

  1. L45
    have hlast_one : BetaAt(b,c,k,1)Definitions: BetaAt(b,c,k,1)Original native command in the exact edition
  2. L46
    specialize hone k
  3. L47
    apply hone
  4. L48
    specialize le_refl (S k)
  5. L49
    exact le_refl
10Establish haL50–59

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

  1. L50
    have ha : x = 1
  2. L51
    specialize beta_at_unique b
  3. L52
    specialize beta_at_unique c
  4. L53
    specialize beta_at_unique k
  5. L54
    specialize beta_at_unique x
  6. L55
    specialize beta_at_unique 1
  7. L56
    apply beta_at_unique
  8. L57
    exact hdecomp_witness_witness_left
  9. L58
    exact hlast_one
  10. L59
    rewrite hdecomp_witness_witness_right_right_right
11Calculate and transport equalitiesL60–62

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    rewrite hr
  2. L61
    rewrite ha
  3. L62
    simp

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction k
  4. 0004intro n
  5. 0005intro hone
  6. 0006intro hcount
  7. 0007specialize bit_count_zero b
  8. 0008specialize bit_count_zero c
  9. 0009specialize bit_count_zero 0
  10. 0010specialize bit_count_zero n
  11. 0011apply bit_count_zero
  12. 0012refl
  13. 0013exact hcount
  14. 0014intro n
  15. 0015intro hone
  16. 0016intro hcount
  17. 0017have hdecomp : ∃ a. ∃ r. BetaAt(b,c,k,a) ∧ (BitCount(b,c,k,r) ∧ ((a = 0 ∨ a = 1) ∧ n = r + a))
    Exact native replay linehave hdecomp : exists a r. (((exists ff_h_initial_segment_all_one_last. ff_h_initial_segment_all_one_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_all_one_last. b = ff_q_initial_segment_all_one_last * S ((S (k)) * c) + (a))) /\ ((((exists ff_u_initial_segment_all_one_prefix_count_sum ff_v_initial_segment_all_one_prefix_count_sum. ((((exists ff_h_initial_segment_all_one_prefix_count_sum_start. ff_h_initial_segment_all_one_prefix_count_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_start. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_start * S ((S (0)) * ff_v_initial_segment_all_one_prefix_count_sum) + (0))) /\ ((((exists ff_h_initial_segment_all_one_prefix_count_sum_terminal. ff_h_initial_segment_all_one_prefix_count_sum_terminal + S (r) = S ((S (k)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_terminal. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_terminal * S ((S (k)) * ff_v_initial_segment_all_one_prefix_count_sum) + (r))) /\ forall ff_i_initial_segment_all_one_prefix_count_sum. (exists ff_lt_initial_segment_all_one_prefix_count_sum_bound. ff_lt_initial_segment_all_one_prefix_count_sum_bound + S ff_i_initial_segment_all_one_prefix_count_sum = k) -> exists ff_a_initial_segment_all_one_prefix_count_sum ff_r_initial_segment_all_one_prefix_count_sum ff_s_initial_segment_all_one_prefix_count_sum. ((((exists ff_h_initial_segment_all_one_prefix_count_sum_summand. ff_h_initial_segment_all_one_prefix_count_sum_summand + S (ff_a_initial_segment_all_one_prefix_count_sum) = S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * c)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_summand. b = ff_q_initial_segment_all_one_prefix_count_sum_summand * S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * c) + (ff_a_initial_segment_all_one_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_prefix_count_sum_partial. ff_h_initial_segment_all_one_prefix_count_sum_partial + S (ff_r_initial_segment_all_one_prefix_count_sum) = S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_partial. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_partial * S ((S (ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum) + (ff_r_initial_segment_all_one_prefix_count_sum))) /\ ((((exists ff_h_initial_segment_all_one_prefix_count_sum_successor. ff_h_initial_segment_all_one_prefix_count_sum_successor + S (ff_s_initial_segment_all_one_prefix_count_sum) = S ((S (S ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum)) /\ exists ff_q_initial_segment_all_one_prefix_count_sum_successor. ff_u_initial_segment_all_one_prefix_count_sum = ff_q_initial_segment_all_one_prefix_count_sum_successor * S ((S (S ff_i_initial_segment_all_one_prefix_count_sum)) * ff_v_initial_segment_all_one_prefix_count_sum) + (ff_s_initial_segment_all_one_prefix_count_sum))) /\ ff_s_initial_segment_all_one_prefix_count_sum = ff_r_initial_segment_all_one_prefix_count_sum + ff_a_initial_segment_all_one_prefix_count_sum)))))) /\ (forall ff_i_initial_segment_all_one_prefix_count_bits. (exists ff_lt_initial_segment_all_one_prefix_count_bits_bound. ff_lt_initial_segment_all_one_prefix_count_bits_bound + S ff_i_initial_segment_all_one_prefix_count_bits = k) -> exists ff_bit_initial_segment_all_one_prefix_count_bits. ((((exists ff_h_initial_segment_all_one_prefix_count_bits_decoded. ff_h_initial_segment_all_one_prefix_count_bits_decoded + S (ff_bit_initial_segment_all_one_prefix_count_bits) = S ((S (ff_i_initial_segment_all_one_prefix_count_bits)) * c)) /\ exists ff_q_initial_segment_all_one_prefix_count_bits_decoded. b = ff_q_initial_segment_all_one_prefix_count_bits_decoded * S ((S (ff_i_initial_segment_all_one_prefix_count_bits)) * c) + (ff_bit_initial_segment_all_one_prefix_count_bits))) /\ (ff_bit_initial_segment_all_one_prefix_count_bits = 0 \/ ff_bit_initial_segment_all_one_prefix_count_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ n = r + a))
  18. 0018specialize bit_count_succ_decompose b
  19. 0019specialize bit_count_succ_decompose c
  20. 0020specialize bit_count_succ_decompose k
  21. 0021specialize bit_count_succ_decompose (S k)
  22. 0022specialize bit_count_succ_decompose n
  23. 0023apply bit_count_succ_decompose
  24. 0024refl
  25. 0025exact hcount
  26. 0026cases hdecomp
  27. 0027cases hdecomp_witness
  28. 0028cases hdecomp_witness_witness
  29. 0029cases hdecomp_witness_witness_right
  30. 0030cases hdecomp_witness_witness_right_right
  31. 0031have hone_previous : Repeat(b,c,1,k)
    Exact native replay linehave hone_previous : forall eis_one_index_initial_segment_all_one_previous. (exists eis_lt_gap_initial_segment_all_one_previous_bound. eis_lt_gap_initial_segment_all_one_previous_bound + S (eis_one_index_initial_segment_all_one_previous) = k) -> (((exists ff_h_eis_initial_segment_all_one_previous_decoded. ff_h_eis_initial_segment_all_one_previous_decoded + S (1) = S ((S (eis_one_index_initial_segment_all_one_previous)) * c)) /\ exists ff_q_eis_initial_segment_all_one_previous_decoded. b = ff_q_eis_initial_segment_all_one_previous_decoded * S ((S (eis_one_index_initial_segment_all_one_previous)) * c) + (1)))
  32. 0032intro j
  33. 0033intro hj
  34. 0034specialize hone j
  35. 0035apply hone
  36. 0036specialize le_succ (S j)
  37. 0037specialize le_succ k
  38. 0038apply le_succ
  39. 0039exact hj
  40. 0040have hr : x1 = k
  41. 0041specialize IH x1
  42. 0042apply IH
  43. 0043exact hone_previous
  44. 0044exact hdecomp_witness_witness_right_left
  45. 0045have hlast_one : BetaAt(b,c,k,1)
    Exact native replay linehave hlast_one : ((exists ff_h_initial_segment_all_one_terminal. ff_h_initial_segment_all_one_terminal + S (1) = S ((S (k)) * c)) /\ exists ff_q_initial_segment_all_one_terminal. b = ff_q_initial_segment_all_one_terminal * S ((S (k)) * c) + (1))
  46. 0046specialize hone k
  47. 0047apply hone
  48. 0048specialize le_refl (S k)
  49. 0049exact le_refl
  50. 0050have ha : x = 1
  51. 0051specialize beta_at_unique b
  52. 0052specialize beta_at_unique c
  53. 0053specialize beta_at_unique k
  54. 0054specialize beta_at_unique x
  55. 0055specialize beta_at_unique 1
  56. 0056apply beta_at_unique
  57. 0057exact hdecomp_witness_witness_left
  58. 0058exact hlast_one
  59. 0059rewrite hdecomp_witness_witness_right_right_right
  60. 0060rewrite hr
  61. 0061rewrite ha
  62. 0062simp