PA00DY · theorem

eisenstein_initial_segment_bit_count_exact

Alpha v34 checked-use theorem · independently closed; 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. 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

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

PA00DU eisenstein_initial_segment_prefix_all_bits PA003I bit_count_exists PA00DX eisenstein_initial_segment_bit_count_functional

Direct theorem dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

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

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