BT00JE · Bertrand theorem

eisenstein_initial_segment_bit_count_exact

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

A bounded exact initial-segment prefix has native BitCount q.

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

∀ q. ∀ b. ∀ c. ∀ k. (∀ x. Lt(x,k) → ∃ y. BetaAt(b,c,x,y) ∧ (y = 1 ∧ Lt(x,q) ∨ y = 0 ∧ Lt(q,S x))) → Le(q,k) → BitCount(b,c,k,q)

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

PD0001 Le PD0002 Lt PD0013 BetaAt PD0017 BitCount

6 occurrences

In local proof propositions

PD0016 AllBits PD0017 BitCount

2 occurrences

Exact expanded native-PA statement
forall q b c k. (forall eis_index_initial_segment_count_result_prefix. (exists eis_lt_gap_initial_segment_count_result_prefix_bound. eis_lt_gap_initial_segment_count_result_prefix_bound + S (eis_index_initial_segment_count_result_prefix) = k) -> exists eis_bit_initial_segment_count_result_prefix. ((((exists ff_h_eis_initial_segment_count_result_prefix_decoded. ff_h_eis_initial_segment_count_result_prefix_decoded + S (eis_bit_initial_segment_count_result_prefix) = S ((S (eis_index_initial_segment_count_result_prefix)) * c)) /\ exists ff_q_eis_initial_segment_count_result_prefix_decoded. b = ff_q_eis_initial_segment_count_result_prefix_decoded * S ((S (eis_index_initial_segment_count_result_prefix)) * c) + (eis_bit_initial_segment_count_result_prefix))) /\ (((eis_bit_initial_segment_count_result_prefix = 1 /\ (exists eis_le_gap_initial_segment_count_result_prefix_choice_inside. eis_le_gap_initial_segment_count_result_prefix_choice_inside + (S eis_index_initial_segment_count_result_prefix) = q)) \/ (eis_bit_initial_segment_count_result_prefix = 0 /\ (exists eis_lt_gap_initial_segment_count_result_prefix_choice_outside. eis_lt_gap_initial_segment_count_result_prefix_choice_outside + S (q) = S eis_index_initial_segment_count_result_prefix)))))) -> (exists eis_le_gap_initial_segment_count_result_bound. eis_le_gap_initial_segment_count_result_bound + (q) = k) -> (((exists ff_u_initial_segment_count_result_sum ff_v_initial_segment_count_result_sum. ((((exists ff_h_initial_segment_count_result_sum_start. ff_h_initial_segment_count_result_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_start. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_start * S ((S (0)) * ff_v_initial_segment_count_result_sum) + (0))) /\ ((((exists ff_h_initial_segment_count_result_sum_terminal. ff_h_initial_segment_count_result_sum_terminal + S (q) = S ((S (k)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_terminal. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_terminal * S ((S (k)) * ff_v_initial_segment_count_result_sum) + (q))) /\ forall ff_i_initial_segment_count_result_sum. (exists ff_lt_initial_segment_count_result_sum_bound. ff_lt_initial_segment_count_result_sum_bound + S ff_i_initial_segment_count_result_sum = k) -> exists ff_a_initial_segment_count_result_sum ff_r_initial_segment_count_result_sum ff_s_initial_segment_count_result_sum. ((((exists ff_h_initial_segment_count_result_sum_summand. ff_h_initial_segment_count_result_sum_summand + S (ff_a_initial_segment_count_result_sum) = S ((S (ff_i_initial_segment_count_result_sum)) * c)) /\ exists ff_q_initial_segment_count_result_sum_summand. b = ff_q_initial_segment_count_result_sum_summand * S ((S (ff_i_initial_segment_count_result_sum)) * c) + (ff_a_initial_segment_count_result_sum))) /\ ((((exists ff_h_initial_segment_count_result_sum_partial. ff_h_initial_segment_count_result_sum_partial + S (ff_r_initial_segment_count_result_sum) = S ((S (ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_partial. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_partial * S ((S (ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum) + (ff_r_initial_segment_count_result_sum))) /\ ((((exists ff_h_initial_segment_count_result_sum_successor. ff_h_initial_segment_count_result_sum_successor + S (ff_s_initial_segment_count_result_sum) = S ((S (S ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum)) /\ exists ff_q_initial_segment_count_result_sum_successor. ff_u_initial_segment_count_result_sum = ff_q_initial_segment_count_result_sum_successor * S ((S (S ff_i_initial_segment_count_result_sum)) * ff_v_initial_segment_count_result_sum) + (ff_s_initial_segment_count_result_sum))) /\ ff_s_initial_segment_count_result_sum = ff_r_initial_segment_count_result_sum + ff_a_initial_segment_count_result_sum)))))) /\ (forall ff_i_initial_segment_count_result_bits. (exists ff_lt_initial_segment_count_result_bits_bound. ff_lt_initial_segment_count_result_bits_bound + S ff_i_initial_segment_count_result_bits = k) -> exists ff_bit_initial_segment_count_result_bits. ((((exists ff_h_initial_segment_count_result_bits_decoded. ff_h_initial_segment_count_result_bits_decoded + S (ff_bit_initial_segment_count_result_bits) = S ((S (ff_i_initial_segment_count_result_bits)) * c)) /\ exists ff_q_initial_segment_count_result_bits_decoded. b = ff_q_initial_segment_count_result_bits_decoded * S ((S (ff_i_initial_segment_count_result_bits)) * c) + (ff_bit_initial_segment_count_result_bits))) /\ (ff_bit_initial_segment_count_result_bits = 0 \/ ff_bit_initial_segment_count_result_bits = 1)))))

Proof neighborhood

Direct theorem prerequisites

BT00JA eisenstein_initial_segment_prefix_all_bits BT008L bit_count_exists BT00JD eisenstein_initial_segment_bit_count_functional

Direct theorem dependents

BT00SU initial_segment_prefix_sum_exists

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

33 script commands · 7 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 (3)
eisenstein initial segment prefix all bitsbit count existseisenstein initial segment bit count functional
01Fix variables and assumptionsL1–6

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

  1. L1
    intro q
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro k
  5. L5
    intro hprefix
  6. L6
    intro hqk
02Establish hallbitsL7–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein initial segment prefix all bits.

  1. L7
    have hallbits : AllBits(b,c,k)Definitions: AllBits(b,c,k)Original native command in the exact edition
  2. L8
    specialize eisenstein_initial_segment_prefix_all_bits q
  3. L9
    specialize eisenstein_initial_segment_prefix_all_bits b
  4. L10
    specialize eisenstein_initial_segment_prefix_all_bits c
  5. L11
    specialize eisenstein_initial_segment_prefix_all_bits k
  6. L12
    apply eisenstein_initial_segment_prefix_all_bits
  7. L13
    exact hprefix
03Establish hcountL14–19

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

  1. L14
    have hcount : ∃ n. BitCount(b,c,k,n)Definitions: BitCount(b,c,k,n)Original native command in the exact edition
  2. L15
    specialize bit_count_exists b
  3. L16
    specialize bit_count_exists c
  4. L17
    specialize bit_count_exists k
  5. L18
    apply bit_count_exists
  6. L19
    exact hallbits
04Separate the logical casesL20–20

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

  1. L20
    cases hcount
05Establish hnqL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein initial segment bit count functional.

  1. L21
    have hnq : x = q
  2. L22
    specialize eisenstein_initial_segment_bit_count_functional q
  3. L23
    specialize eisenstein_initial_segment_bit_count_functional b
  4. L24
    specialize eisenstein_initial_segment_bit_count_functional c
  5. L25
    specialize eisenstein_initial_segment_bit_count_functional k
  6. L26
    specialize eisenstein_initial_segment_bit_count_functional x
  7. L27
    apply eisenstein_initial_segment_bit_count_functional
  8. L28
    exact hprefix
  9. L29
    exact hqk
  10. L30
    exact hcount_witness
06Calculate and transport equalitiesL31–32

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

  1. L31
    rewrite hnq at hcount_witness
  2. L32
    rewrite hnq at hcount_witness
07Use earlier factsL33–33

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

  1. L33
    exact hcount_witness

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro q
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro hprefix
  6. 0006intro hqk
  7. 0007have hallbits : AllBits(b,c,k)
    Exact native replay linehave hallbits : forall ff_i_initial_segment_exact_all_bits. (exists ff_lt_initial_segment_exact_all_bits_bound. ff_lt_initial_segment_exact_all_bits_bound + S ff_i_initial_segment_exact_all_bits = k) -> exists ff_bit_initial_segment_exact_all_bits. ((((exists ff_h_initial_segment_exact_all_bits_decoded. ff_h_initial_segment_exact_all_bits_decoded + S (ff_bit_initial_segment_exact_all_bits) = S ((S (ff_i_initial_segment_exact_all_bits)) * c)) /\ exists ff_q_initial_segment_exact_all_bits_decoded. b = ff_q_initial_segment_exact_all_bits_decoded * S ((S (ff_i_initial_segment_exact_all_bits)) * c) + (ff_bit_initial_segment_exact_all_bits))) /\ (ff_bit_initial_segment_exact_all_bits = 0 \/ ff_bit_initial_segment_exact_all_bits = 1))
  8. 0008specialize eisenstein_initial_segment_prefix_all_bits q
  9. 0009specialize eisenstein_initial_segment_prefix_all_bits b
  10. 0010specialize eisenstein_initial_segment_prefix_all_bits c
  11. 0011specialize eisenstein_initial_segment_prefix_all_bits k
  12. 0012apply eisenstein_initial_segment_prefix_all_bits
  13. 0013exact hprefix
  14. 0014have hcount : ∃ n. BitCount(b,c,k,n)
    Exact native replay linehave hcount : exists n. ((exists ff_u_initial_segment_exact_exists_sum ff_v_initial_segment_exact_exists_sum. ((((exists ff_h_initial_segment_exact_exists_sum_start. ff_h_initial_segment_exact_exists_sum_start + S (0) = S ((S (0)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_start. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_start * S ((S (0)) * ff_v_initial_segment_exact_exists_sum) + (0))) /\ ((((exists ff_h_initial_segment_exact_exists_sum_terminal. ff_h_initial_segment_exact_exists_sum_terminal + S (n) = S ((S (k)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_terminal. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_terminal * S ((S (k)) * ff_v_initial_segment_exact_exists_sum) + (n))) /\ forall ff_i_initial_segment_exact_exists_sum. (exists ff_lt_initial_segment_exact_exists_sum_bound. ff_lt_initial_segment_exact_exists_sum_bound + S ff_i_initial_segment_exact_exists_sum = k) -> exists ff_a_initial_segment_exact_exists_sum ff_r_initial_segment_exact_exists_sum ff_s_initial_segment_exact_exists_sum. ((((exists ff_h_initial_segment_exact_exists_sum_summand. ff_h_initial_segment_exact_exists_sum_summand + S (ff_a_initial_segment_exact_exists_sum) = S ((S (ff_i_initial_segment_exact_exists_sum)) * c)) /\ exists ff_q_initial_segment_exact_exists_sum_summand. b = ff_q_initial_segment_exact_exists_sum_summand * S ((S (ff_i_initial_segment_exact_exists_sum)) * c) + (ff_a_initial_segment_exact_exists_sum))) /\ ((((exists ff_h_initial_segment_exact_exists_sum_partial. ff_h_initial_segment_exact_exists_sum_partial + S (ff_r_initial_segment_exact_exists_sum) = S ((S (ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_partial. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_partial * S ((S (ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum) + (ff_r_initial_segment_exact_exists_sum))) /\ ((((exists ff_h_initial_segment_exact_exists_sum_successor. ff_h_initial_segment_exact_exists_sum_successor + S (ff_s_initial_segment_exact_exists_sum) = S ((S (S ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum)) /\ exists ff_q_initial_segment_exact_exists_sum_successor. ff_u_initial_segment_exact_exists_sum = ff_q_initial_segment_exact_exists_sum_successor * S ((S (S ff_i_initial_segment_exact_exists_sum)) * ff_v_initial_segment_exact_exists_sum) + (ff_s_initial_segment_exact_exists_sum))) /\ ff_s_initial_segment_exact_exists_sum = ff_r_initial_segment_exact_exists_sum + ff_a_initial_segment_exact_exists_sum)))))) /\ (forall ff_i_initial_segment_exact_exists_bits. (exists ff_lt_initial_segment_exact_exists_bits_bound. ff_lt_initial_segment_exact_exists_bits_bound + S ff_i_initial_segment_exact_exists_bits = k) -> exists ff_bit_initial_segment_exact_exists_bits. ((((exists ff_h_initial_segment_exact_exists_bits_decoded. ff_h_initial_segment_exact_exists_bits_decoded + S (ff_bit_initial_segment_exact_exists_bits) = S ((S (ff_i_initial_segment_exact_exists_bits)) * c)) /\ exists ff_q_initial_segment_exact_exists_bits_decoded. b = ff_q_initial_segment_exact_exists_bits_decoded * S ((S (ff_i_initial_segment_exact_exists_bits)) * c) + (ff_bit_initial_segment_exact_exists_bits))) /\ (ff_bit_initial_segment_exact_exists_bits = 0 \/ ff_bit_initial_segment_exact_exists_bits = 1))))
  15. 0015specialize bit_count_exists b
  16. 0016specialize bit_count_exists c
  17. 0017specialize bit_count_exists k
  18. 0018apply bit_count_exists
  19. 0019exact hallbits
  20. 0020cases hcount
  21. 0021have hnq : x = q
  22. 0022specialize eisenstein_initial_segment_bit_count_functional q
  23. 0023specialize eisenstein_initial_segment_bit_count_functional b
  24. 0024specialize eisenstein_initial_segment_bit_count_functional c
  25. 0025specialize eisenstein_initial_segment_bit_count_functional k
  26. 0026specialize eisenstein_initial_segment_bit_count_functional x
  27. 0027apply eisenstein_initial_segment_bit_count_functional
  28. 0028exact hprefix
  29. 0029exact hqk
  30. 0030exact hcount_witness
  31. 0031rewrite hnq at hcount_witness
  32. 0032rewrite hnq at hcount_witness
  33. 0033exact hcount_witness