PA00E0 · theorem

distinct_odd_prime_row_bit_count_equals_division_quotient

Alpha v34 checked-use theorem · independently closed; not Stable

A semantic row BitCount is the quotient in its bounded nonzero division.

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

∀ p. ∀ q. ∀ h. ∀ k. ∀ i. ∀ d. ∀ r. ∀ rb. ∀ rc. ∀ n. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → (∀ x. Lt(x,k) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) → BitCount(rb,rc,k,n) → q · S i = p · d + r → Lt(r,p) → n = d

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

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0017 BitCount

11 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt PD0017 BitCount

6 occurrences

Exact expanded native-PA statement
forall p q h k i d r rb rc n. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_quotient_prime_p frp_prime_right_row_quotient_prime_p. p = frp_prime_left_row_quotient_prime_p * frp_prime_right_row_quotient_prime_p -> frp_prime_left_row_quotient_prime_p = 1 \/ frp_prime_right_row_quotient_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_quotient_prime_q frp_prime_right_row_quotient_prime_q. q = frp_prime_left_row_quotient_prime_q * frp_prime_right_row_quotient_prime_q -> frp_prime_left_row_quotient_prime_q = 1 \/ frp_prime_right_row_quotient_prime_q = 1)) -> ~(p = q) -> (exists edt_lt_gap_row_quotient_row_bound. edt_lt_gap_row_quotient_row_bound + S (i) = h) -> (forall eri_column_row_quotient_source. (exists eri_gap_row_quotient_source_bound. eri_gap_row_quotient_source_bound + S (eri_column_row_quotient_source) = k) -> exists eri_bit_row_quotient_source. ((((exists ff_h_eri_row_quotient_source_decoded. ff_h_eri_row_quotient_source_decoded + S (eri_bit_row_quotient_source) = S ((S (eri_column_row_quotient_source)) * rc)) /\ exists ff_q_eri_row_quotient_source_decoded. rb = ff_q_eri_row_quotient_source_decoded * S ((S (eri_column_row_quotient_source)) * rc) + (eri_bit_row_quotient_source))) /\ (((eri_bit_row_quotient_source = 0 /\ ((exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source) /\ ~(exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i))) \/ (eri_bit_row_quotient_source = 1 /\ ((exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i) /\ ~(exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source))))))) -> (((exists ff_u_row_quotient_count_n_sum ff_v_row_quotient_count_n_sum. ((((exists ff_h_row_quotient_count_n_sum_start. ff_h_row_quotient_count_n_sum_start + S (0) = S ((S (0)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_start. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_start * S ((S (0)) * ff_v_row_quotient_count_n_sum) + (0))) /\ ((((exists ff_h_row_quotient_count_n_sum_terminal. ff_h_row_quotient_count_n_sum_terminal + S (n) = S ((S (k)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_terminal. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_terminal * S ((S (k)) * ff_v_row_quotient_count_n_sum) + (n))) /\ forall ff_i_row_quotient_count_n_sum. (exists ff_lt_row_quotient_count_n_sum_bound. ff_lt_row_quotient_count_n_sum_bound + S ff_i_row_quotient_count_n_sum = k) -> exists ff_a_row_quotient_count_n_sum ff_r_row_quotient_count_n_sum ff_s_row_quotient_count_n_sum. ((((exists ff_h_row_quotient_count_n_sum_summand. ff_h_row_quotient_count_n_sum_summand + S (ff_a_row_quotient_count_n_sum) = S ((S (ff_i_row_quotient_count_n_sum)) * rc)) /\ exists ff_q_row_quotient_count_n_sum_summand. rb = ff_q_row_quotient_count_n_sum_summand * S ((S (ff_i_row_quotient_count_n_sum)) * rc) + (ff_a_row_quotient_count_n_sum))) /\ ((((exists ff_h_row_quotient_count_n_sum_partial. ff_h_row_quotient_count_n_sum_partial + S (ff_r_row_quotient_count_n_sum) = S ((S (ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_partial. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_partial * S ((S (ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum) + (ff_r_row_quotient_count_n_sum))) /\ ((((exists ff_h_row_quotient_count_n_sum_successor. ff_h_row_quotient_count_n_sum_successor + S (ff_s_row_quotient_count_n_sum) = S ((S (S ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_successor. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_successor * S ((S (S ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum) + (ff_s_row_quotient_count_n_sum))) /\ ff_s_row_quotient_count_n_sum = ff_r_row_quotient_count_n_sum + ff_a_row_quotient_count_n_sum)))))) /\ (forall ff_i_row_quotient_count_n_bits. (exists ff_lt_row_quotient_count_n_bits_bound. ff_lt_row_quotient_count_n_bits_bound + S ff_i_row_quotient_count_n_bits = k) -> exists ff_bit_row_quotient_count_n_bits. ((((exists ff_h_row_quotient_count_n_bits_decoded. ff_h_row_quotient_count_n_bits_decoded + S (ff_bit_row_quotient_count_n_bits) = S ((S (ff_i_row_quotient_count_n_bits)) * rc)) /\ exists ff_q_row_quotient_count_n_bits_decoded. rb = ff_q_row_quotient_count_n_bits_decoded * S ((S (ff_i_row_quotient_count_n_bits)) * rc) + (ff_bit_row_quotient_count_n_bits))) /\ (ff_bit_row_quotient_count_n_bits = 0 \/ ff_bit_row_quotient_count_n_bits = 1))))) -> q * S i = p * d + r -> (exists edt_lt_gap_row_quotient_remainder_bound. edt_lt_gap_row_quotient_remainder_bound + S (r) = p) -> n = d

Proof neighborhood

Direct theorem prerequisites

PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero PA00DR odd_half_division_quotient_bounded PA00DT eisenstein_row_indicator_prefix_to_initial_segment PA00DY eisenstein_initial_segment_bit_count_exact PA006Q bit_count_functional

Direct theorem dependents

PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_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

79 script commands · 10 reading checkpoints · 4 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)
distinct primes own odd half scaled remainder nonzeroodd half division quotient boundedeisenstein row indicator prefix to initial segmenteisenstein initial segment bit count exactbit count functional
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro i
  6. L6
    intro d
  7. L7
    intro r
  8. L8
    intro rb
  9. L9
    intro rc
  10. L10
    intro n
02Fix variables and assumptionsL11–20

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

  1. L11
    intro hpodd
  2. L12
    intro hqodd
  3. L13
    intro hp
  4. L14
    intro hq
  5. L15
    intro hpq
  6. L16
    intro hi
  7. L17
    intro hrow
  8. L18
    intro hcount
  9. L19
    intro hdivision
  10. L20
    intro hrp
03Establish hr0L21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct primes own odd half scaled remainder nonzero.

  1. L21
    have hr0 : ~(r = 0)
  2. L22
    intro hrzero
  3. L23
    specialize distinct_primes_own_odd_half_scaled_remainder_nonzero p
  4. L24
    specialize distinct_primes_own_odd_half_scaled_remainder_nonzero q
  5. L25
    specialize distinct_primes_own_odd_half_scaled_remainder_nonzero h
  6. L26
    specialize distinct_primes_own_odd_half_scaled_remainder_nonzero i
  7. L27
    specialize distinct_primes_own_odd_half_scaled_remainder_nonzero d
  8. L28
    specialize distinct_primes_own_odd_half_scaled_remainder_nonzero r
  9. L29
    apply distinct_primes_own_odd_half_scaled_remainder_nonzero
  10. L30
    exact hpodd
04Use earlier factsL31–36

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

  1. L31
    exact hp
  2. L32
    exact hq
  3. L33
    exact hpq
  4. L34
    exact hi
  5. L35
    exact hdivision
  6. L36
    exact hrzero
05Establish hdleL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half division quotient bounded.

  1. L37
  2. L38
    specialize odd_half_division_quotient_bounded p
  3. L39
    specialize odd_half_division_quotient_bounded q
  4. L40
    specialize odd_half_division_quotient_bounded h
  5. L41
    specialize odd_half_division_quotient_bounded k
  6. L42
    specialize odd_half_division_quotient_bounded i
  7. L43
    specialize odd_half_division_quotient_bounded d
  8. L44
    specialize odd_half_division_quotient_bounded r
  9. L45
    apply odd_half_division_quotient_bounded
  10. L46
    exact hpodd
06Use earlier factsL47–49

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

  1. L47
    exact hqodd
  2. L48
    exact hi
  3. L49
    exact hdivision
07Establish hinitialL50–59

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

  1. L50
    have hinitial : ∀ eis_index_row_quotient_initial. Lt(eis_index_row_quotient_initial,k) → ∃ x. BetaAt(rb,rc,eis_index_row_quotient_initial,x) ∧ (x = 1 ∧ Lt(eis_index_row_quotient_initial,d) ∨ x = 0 ∧ Lt(d,S eis_index_row_quotient_initial))Definitions: Lt(eis_index_row_quotient_initial,k)BetaAt(rb,rc,eis_index_row_quotient_initial,x)Lt(eis_index_row_quotient_initial,d)Lt(d,S eis_index_row_quotient_initial)Original native command in the exact edition
  2. L51
    specialize eisenstein_row_indicator_prefix_to_initial_segment p
  3. L52
    specialize eisenstein_row_indicator_prefix_to_initial_segment q
  4. L53
    specialize eisenstein_row_indicator_prefix_to_initial_segment i
  5. L54
    specialize eisenstein_row_indicator_prefix_to_initial_segment d
  6. L55
    specialize eisenstein_row_indicator_prefix_to_initial_segment r
  7. L56
    specialize eisenstein_row_indicator_prefix_to_initial_segment rb
  8. L57
    specialize eisenstein_row_indicator_prefix_to_initial_segment rc
  9. L58
    specialize eisenstein_row_indicator_prefix_to_initial_segment k
  10. L59
    apply eisenstein_row_indicator_prefix_to_initial_segment
08Use earlier factsL60–63

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

  1. L60
    exact hrow
  2. L61
    exact hdivision
  3. L62
    exact hr0
  4. L63
    exact hrp
09Establish hcountdL64–73

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

  1. L64
    have hcountd : BitCount(rb,rc,k,d)Definitions: BitCount(rb,rc,k,d)Original native command in the exact edition
  2. L65
    specialize eisenstein_initial_segment_bit_count_exact d
  3. L66
    specialize eisenstein_initial_segment_bit_count_exact rb
  4. L67
    specialize eisenstein_initial_segment_bit_count_exact rc
  5. L68
    specialize eisenstein_initial_segment_bit_count_exact k
  6. L69
    apply eisenstein_initial_segment_bit_count_exact
  7. L70
    exact hinitial
  8. L71
    exact hdle
  9. L72
    specialize bit_count_functional rb
  10. L73
    specialize bit_count_functional rc
10Use earlier factsL74–79

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

  1. L74
    specialize bit_count_functional k
  2. L75
    specialize bit_count_functional n
  3. L76
    specialize bit_count_functional d
  4. L77
    apply bit_count_functional
  5. L78
    exact hcount
  6. L79
    exact hcountd

Library-wide reading audit

Original defined command ledger · 79 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro d
  7. 0007intro r
  8. 0008intro rb
  9. 0009intro rc
  10. 0010intro n
  11. 0011intro hpodd
  12. 0012intro hqodd
  13. 0013intro hp
  14. 0014intro hq
  15. 0015intro hpq
  16. 0016intro hi
  17. 0017intro hrow
  18. 0018intro hcount
  19. 0019intro hdivision
  20. 0020intro hrp
  21. 0021have hr0 : ~(r = 0)
  22. 0022intro hrzero
  23. 0023specialize distinct_primes_own_odd_half_scaled_remainder_nonzero p
  24. 0024specialize distinct_primes_own_odd_half_scaled_remainder_nonzero q
  25. 0025specialize distinct_primes_own_odd_half_scaled_remainder_nonzero h
  26. 0026specialize distinct_primes_own_odd_half_scaled_remainder_nonzero i
  27. 0027specialize distinct_primes_own_odd_half_scaled_remainder_nonzero d
  28. 0028specialize distinct_primes_own_odd_half_scaled_remainder_nonzero r
  29. 0029apply distinct_primes_own_odd_half_scaled_remainder_nonzero
  30. 0030exact hpodd
  31. 0031exact hp
  32. 0032exact hq
  33. 0033exact hpq
  34. 0034exact hi
  35. 0035exact hdivision
  36. 0036exact hrzero
  37. 0037have hdle : Le(d,k)
    Exact native replay linehave hdle : exists edt_le_gap_row_quotient_quotient_bound. edt_le_gap_row_quotient_quotient_bound + (d) = k
  38. 0038specialize odd_half_division_quotient_bounded p
  39. 0039specialize odd_half_division_quotient_bounded q
  40. 0040specialize odd_half_division_quotient_bounded h
  41. 0041specialize odd_half_division_quotient_bounded k
  42. 0042specialize odd_half_division_quotient_bounded i
  43. 0043specialize odd_half_division_quotient_bounded d
  44. 0044specialize odd_half_division_quotient_bounded r
  45. 0045apply odd_half_division_quotient_bounded
  46. 0046exact hpodd
  47. 0047exact hqodd
  48. 0048exact hi
  49. 0049exact hdivision
  50. 0050have hinitial : ∀ eis_index_row_quotient_initial. Lt(eis_index_row_quotient_initial,k) → ∃ x. BetaAt(rb,rc,eis_index_row_quotient_initial,x) ∧ (x = 1 ∧ Lt(eis_index_row_quotient_initial,d) ∨ x = 0 ∧ Lt(d,S eis_index_row_quotient_initial))
    Exact native replay linehave hinitial : forall eis_index_row_quotient_initial. (exists eis_lt_gap_row_quotient_initial_bound. eis_lt_gap_row_quotient_initial_bound + S (eis_index_row_quotient_initial) = k) -> exists eis_bit_row_quotient_initial. ((((exists ff_h_eis_row_quotient_initial_decoded. ff_h_eis_row_quotient_initial_decoded + S (eis_bit_row_quotient_initial) = S ((S (eis_index_row_quotient_initial)) * rc)) /\ exists ff_q_eis_row_quotient_initial_decoded. rb = ff_q_eis_row_quotient_initial_decoded * S ((S (eis_index_row_quotient_initial)) * rc) + (eis_bit_row_quotient_initial))) /\ (((eis_bit_row_quotient_initial = 1 /\ (exists eis_le_gap_row_quotient_initial_choice_inside. eis_le_gap_row_quotient_initial_choice_inside + (S eis_index_row_quotient_initial) = d)) \/ (eis_bit_row_quotient_initial = 0 /\ (exists eis_lt_gap_row_quotient_initial_choice_outside. eis_lt_gap_row_quotient_initial_choice_outside + S (d) = S eis_index_row_quotient_initial)))))
  51. 0051specialize eisenstein_row_indicator_prefix_to_initial_segment p
  52. 0052specialize eisenstein_row_indicator_prefix_to_initial_segment q
  53. 0053specialize eisenstein_row_indicator_prefix_to_initial_segment i
  54. 0054specialize eisenstein_row_indicator_prefix_to_initial_segment d
  55. 0055specialize eisenstein_row_indicator_prefix_to_initial_segment r
  56. 0056specialize eisenstein_row_indicator_prefix_to_initial_segment rb
  57. 0057specialize eisenstein_row_indicator_prefix_to_initial_segment rc
  58. 0058specialize eisenstein_row_indicator_prefix_to_initial_segment k
  59. 0059apply eisenstein_row_indicator_prefix_to_initial_segment
  60. 0060exact hrow
  61. 0061exact hdivision
  62. 0062exact hr0
  63. 0063exact hrp
  64. 0064have hcountd : BitCount(rb,rc,k,d)
    Exact native replay linehave hcountd : ((exists ff_u_row_quotient_count_d_sum ff_v_row_quotient_count_d_sum. ((((exists ff_h_row_quotient_count_d_sum_start. ff_h_row_quotient_count_d_sum_start + S (0) = S ((S (0)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_start. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_start * S ((S (0)) * ff_v_row_quotient_count_d_sum) + (0))) /\ ((((exists ff_h_row_quotient_count_d_sum_terminal. ff_h_row_quotient_count_d_sum_terminal + S (d) = S ((S (k)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_terminal. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_terminal * S ((S (k)) * ff_v_row_quotient_count_d_sum) + (d))) /\ forall ff_i_row_quotient_count_d_sum. (exists ff_lt_row_quotient_count_d_sum_bound. ff_lt_row_quotient_count_d_sum_bound + S ff_i_row_quotient_count_d_sum = k) -> exists ff_a_row_quotient_count_d_sum ff_r_row_quotient_count_d_sum ff_s_row_quotient_count_d_sum. ((((exists ff_h_row_quotient_count_d_sum_summand. ff_h_row_quotient_count_d_sum_summand + S (ff_a_row_quotient_count_d_sum) = S ((S (ff_i_row_quotient_count_d_sum)) * rc)) /\ exists ff_q_row_quotient_count_d_sum_summand. rb = ff_q_row_quotient_count_d_sum_summand * S ((S (ff_i_row_quotient_count_d_sum)) * rc) + (ff_a_row_quotient_count_d_sum))) /\ ((((exists ff_h_row_quotient_count_d_sum_partial. ff_h_row_quotient_count_d_sum_partial + S (ff_r_row_quotient_count_d_sum) = S ((S (ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_partial. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_partial * S ((S (ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum) + (ff_r_row_quotient_count_d_sum))) /\ ((((exists ff_h_row_quotient_count_d_sum_successor. ff_h_row_quotient_count_d_sum_successor + S (ff_s_row_quotient_count_d_sum) = S ((S (S ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_successor. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_successor * S ((S (S ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum) + (ff_s_row_quotient_count_d_sum))) /\ ff_s_row_quotient_count_d_sum = ff_r_row_quotient_count_d_sum + ff_a_row_quotient_count_d_sum)))))) /\ (forall ff_i_row_quotient_count_d_bits. (exists ff_lt_row_quotient_count_d_bits_bound. ff_lt_row_quotient_count_d_bits_bound + S ff_i_row_quotient_count_d_bits = k) -> exists ff_bit_row_quotient_count_d_bits. ((((exists ff_h_row_quotient_count_d_bits_decoded. ff_h_row_quotient_count_d_bits_decoded + S (ff_bit_row_quotient_count_d_bits) = S ((S (ff_i_row_quotient_count_d_bits)) * rc)) /\ exists ff_q_row_quotient_count_d_bits_decoded. rb = ff_q_row_quotient_count_d_bits_decoded * S ((S (ff_i_row_quotient_count_d_bits)) * rc) + (ff_bit_row_quotient_count_d_bits))) /\ (ff_bit_row_quotient_count_d_bits = 0 \/ ff_bit_row_quotient_count_d_bits = 1))))
  65. 0065specialize eisenstein_initial_segment_bit_count_exact d
  66. 0066specialize eisenstein_initial_segment_bit_count_exact rb
  67. 0067specialize eisenstein_initial_segment_bit_count_exact rc
  68. 0068specialize eisenstein_initial_segment_bit_count_exact k
  69. 0069apply eisenstein_initial_segment_bit_count_exact
  70. 0070exact hinitial
  71. 0071exact hdle
  72. 0072specialize bit_count_functional rb
  73. 0073specialize bit_count_functional rc
  74. 0074specialize bit_count_functional k
  75. 0075specialize bit_count_functional n
  76. 0076specialize bit_count_functional d
  77. 0077apply bit_count_functional
  78. 0078exact hcount
  79. 0079exact hcountd