PA00E1 · theorem

distinct_odd_prime_row_bit_count_equals_decoded_quotient

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

The semantic row count equals the quotient decoded by the scaled division prefix at that row.

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. ∀ tb. ∀ tc. ∀ qb. ∀ qc. ∀ ub. ∀ uc. ∀ rb. ∀ rc. ∀ n. ∀ d. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = q · (1 + x)) → DivisionPrefix(p,tb,tc,qb,qc,ub,uc,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) → BetaAt(qb,qc,i,d) → 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 PD0040 DivisionPrefix

14 occurrences

In local proof propositions

PD0007 DivRem PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall p q h k i tb tc qb qc ub uc rb rc n d. 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 esd_index_row_quotient_scaled esd_value_row_quotient_scaled. (exists esd_gap_row_quotient_scaled. esd_gap_row_quotient_scaled + S esd_index_row_quotient_scaled = h) -> (((exists ff_h_esd_row_quotient_scaled_decoded. ff_h_esd_row_quotient_scaled_decoded + S (esd_value_row_quotient_scaled) = S ((S (esd_index_row_quotient_scaled)) * tc)) /\ exists ff_q_esd_row_quotient_scaled_decoded. tb = ff_q_esd_row_quotient_scaled_decoded * S ((S (esd_index_row_quotient_scaled)) * tc) + (esd_value_row_quotient_scaled))) -> esd_value_row_quotient_scaled = q * (1 + esd_index_row_quotient_scaled)) -> (forall fdp_index_row_quotient_division. (exists gsp_lt_gap_row_quotient_division_index_bound. gsp_lt_gap_row_quotient_division_index_bound + S fdp_index_row_quotient_division = h) -> exists fdp_value_row_quotient_division fdp_quotient_row_quotient_division fdp_remainder_row_quotient_division. (((exists ff_h_fdp_row_quotient_division_source. ff_h_fdp_row_quotient_division_source + S (fdp_value_row_quotient_division) = S ((S (fdp_index_row_quotient_division)) * tc)) /\ exists ff_q_fdp_row_quotient_division_source. tb = ff_q_fdp_row_quotient_division_source * S ((S (fdp_index_row_quotient_division)) * tc) + (fdp_value_row_quotient_division))) /\ ((((exists ff_h_fdp_row_quotient_division_quotient_entry. ff_h_fdp_row_quotient_division_quotient_entry + S (fdp_quotient_row_quotient_division) = S ((S (fdp_index_row_quotient_division)) * qc)) /\ exists ff_q_fdp_row_quotient_division_quotient_entry. qb = ff_q_fdp_row_quotient_division_quotient_entry * S ((S (fdp_index_row_quotient_division)) * qc) + (fdp_quotient_row_quotient_division))) /\ ((((exists ff_h_fdp_row_quotient_division_remainder_entry. ff_h_fdp_row_quotient_division_remainder_entry + S (fdp_remainder_row_quotient_division) = S ((S (fdp_index_row_quotient_division)) * uc)) /\ exists ff_q_fdp_row_quotient_division_remainder_entry. ub = ff_q_fdp_row_quotient_division_remainder_entry * S ((S (fdp_index_row_quotient_division)) * uc) + (fdp_remainder_row_quotient_division))) /\ (fdp_value_row_quotient_division = p * fdp_quotient_row_quotient_division + fdp_remainder_row_quotient_division /\ (exists gsp_lt_gap_row_quotient_division_remainder_bound. gsp_lt_gap_row_quotient_division_remainder_bound + S fdp_remainder_row_quotient_division = p))))) -> (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))))) -> (((exists ff_h_row_quotient_decoded_quotient. ff_h_row_quotient_decoded_quotient + S (d) = S ((S (i)) * qc)) /\ exists ff_q_row_quotient_decoded_quotient. qb = ff_q_row_quotient_decoded_quotient * S ((S (i)) * qc) + (d))) -> n = d

Proof neighborhood

Direct theorem prerequisites

PA000E add_succ_left PA0001 zero_add PA002F beta_at_unique PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

Direct theorem dependents

PA00E2 distinct_odd_prime_semantic_row_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

96 script commands · 15 reading checkpoints · 7 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 (4)
add succ leftzero addbeta at uniquedistinct odd prime row bit count equals division quotient
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 tb
  7. L7
    intro tc
  8. L8
    intro qb
  9. L9
    intro qc
  10. L10
    intro ub
02Fix variables and assumptionsL11–20

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

  1. L11
    intro uc
  2. L12
    intro rb
  3. L13
    intro rc
  4. L14
    intro n
  5. L15
    intro d
  6. L16
    intro hpodd
  7. L17
    intro hqodd
  8. L18
    intro hp
  9. L19
    intro hq
  10. L20
    intro hpq
03Fix variables and assumptionsL21–26

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

  1. L21
    intro hi
  2. L22
    intro hscaled
  3. L23
    intro hdivisions
  4. L24
    intro hrow
  5. L25
    intro hcount
  6. L26
    intro hdentry
04Establish hdivision_entryL27–30

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

  1. L27
    have hdivision_entry : ∃ x. ∃ quotient. ∃ remainder. BetaAt(tb,tc,i,x) ∧ (BetaAt(qb,qc,i,quotient) ∧ (BetaAt(ub,uc,i,remainder) ∧ DivRem(x,p,quotient,remainder)))Definitions: BetaAt(tb,tc,i,x)BetaAt(qb,qc,i,quotient)BetaAt(ub,uc,i,remainder)DivRem(x,p,quotient,remainder)Original native command in the exact edition
  2. L28
    specialize hdivisions i
  3. L29
    apply hdivisions
  4. L30
    exact hi
05Separate the logical casesL31–37

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

  1. L31
    cases hdivision_entry
  2. L32
    cases hdivision_entry_witness
  3. L33
    cases hdivision_entry_witness_witness
  4. L34
    cases hdivision_entry_witness_witness_witness
  5. L35
    cases hdivision_entry_witness_witness_witness_right
  6. L36
    cases hdivision_entry_witness_witness_witness_right_right
  7. L37
    cases hdivision_entry_witness_witness_witness_right_right_right
06Establish hxscaledL38–43

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

  1. L38
    have hxscaled : x = q * (1 + i)
  2. L39
    specialize hscaled i
  3. L40
    specialize hscaled x
  4. L41
    apply hscaled
  5. L42
    exact hi
  6. L43
    exact hdivision_entry_witness_witness_witness_left
07Establish honeL44–51

Establish this local claim before using it. It is not an additional assumption.

  1. L44
    have hone : 1 + i = S i
  2. L45
    trans S (0 + i)
  3. L46
    specialize add_succ_left 0
  4. L47
    specialize add_succ_left i
  5. L48
    exact add_succ_left
  6. L49
    congr
  7. L50
    specialize zero_add i
  8. L51
    exact zero_add
08Establish hxscaled_succL52–57

Establish this local claim before using it. It is not an additional assumption.

  1. L52
    have hxscaled_succ : x = q * S i
  2. L53
    trans q * (1 + i)
  3. L54
    exact hxscaled
  4. L55
    congr
  5. L56
    refl
  6. L57
    exact hone
09Establish hquotient_eqL58–66

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

  1. L58
    have hquotient_eq : x1 = d
  2. L59
    specialize beta_at_unique qb
  3. L60
    specialize beta_at_unique qc
  4. L61
    specialize beta_at_unique i
  5. L62
    specialize beta_at_unique x1
  6. L63
    specialize beta_at_unique d
  7. L64
    apply beta_at_unique
  8. L65
    exact hdivision_entry_witness_witness_witness_right_left
  9. L66
    exact hdentry
10Establish hdivisionL67–71

Establish this local claim before using it. It is not an additional assumption.

  1. L67
    have hdivision : q * S i = p * x1 + x2
  2. L68
    trans x
  3. L69
    symm
  4. L70
    exact hxscaled_succ
  5. L71
    exact hdivision_entry_witness_witness_witness_right_right_right_left
11Establish hnqL72–81

Establish this local claim before using it. It is not an additional assumption.

  1. L72
    have hnq : n = x1
  2. L73
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient p
  3. L74
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient q
  4. L75
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient h
  5. L76
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient k
  6. L77
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient i
  7. L78
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient x1
  8. L79
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient x2
  9. L80
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient rb
  10. L81
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient rc
12Use earlier factsL82–91

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

  1. L82
    specialize distinct_odd_prime_row_bit_count_equals_division_quotient n
  2. L83
    apply distinct_odd_prime_row_bit_count_equals_division_quotient
  3. L84
    exact hpodd
  4. L85
    exact hqodd
  5. L86
    exact hp
  6. L87
    exact hq
  7. L88
    exact hpq
  8. L89
    exact hi
  9. L90
    exact hrow
  10. L91
    exact hcount
13Use earlier factsL92–93

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

  1. L92
    exact hdivision
  2. L93
    exact hdivision_entry_witness_witness_witness_right_right_right_right
14Calculate and transport equalitiesL94–94

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

  1. L94
    trans x1
15Use earlier factsL95–96

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

  1. L95
    exact hnq
  2. L96
    exact hquotient_eq

Library-wide reading audit

Original defined command ledger · 96 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro tb
  7. 0007intro tc
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro ub
  11. 0011intro uc
  12. 0012intro rb
  13. 0013intro rc
  14. 0014intro n
  15. 0015intro d
  16. 0016intro hpodd
  17. 0017intro hqodd
  18. 0018intro hp
  19. 0019intro hq
  20. 0020intro hpq
  21. 0021intro hi
  22. 0022intro hscaled
  23. 0023intro hdivisions
  24. 0024intro hrow
  25. 0025intro hcount
  26. 0026intro hdentry
  27. 0027have hdivision_entry : ∃ x. ∃ quotient. ∃ remainder. BetaAt(tb,tc,i,x) ∧ (BetaAt(qb,qc,i,quotient) ∧ (BetaAt(ub,uc,i,remainder) ∧ DivRem(x,p,quotient,remainder)))
    Exact native replay linehave hdivision_entry : exists x quotient remainder. (((exists ff_h_row_quotient_source_entry. ff_h_row_quotient_source_entry + S (x) = S ((S (i)) * tc)) /\ exists ff_q_row_quotient_source_entry. tb = ff_q_row_quotient_source_entry * S ((S (i)) * tc) + (x))) /\ ((((exists ff_h_row_quotient_quotient_entry. ff_h_row_quotient_quotient_entry + S (quotient) = S ((S (i)) * qc)) /\ exists ff_q_row_quotient_quotient_entry. qb = ff_q_row_quotient_quotient_entry * S ((S (i)) * qc) + (quotient))) /\ ((((exists ff_h_row_quotient_remainder_entry. ff_h_row_quotient_remainder_entry + S (remainder) = S ((S (i)) * uc)) /\ exists ff_q_row_quotient_remainder_entry. ub = ff_q_row_quotient_remainder_entry * S ((S (i)) * uc) + (remainder))) /\ (x = p * quotient + remainder /\ (exists edt_lt_gap_row_quotient_entry_remainder_bound. edt_lt_gap_row_quotient_entry_remainder_bound + S (remainder) = p))))
  28. 0028specialize hdivisions i
  29. 0029apply hdivisions
  30. 0030exact hi
  31. 0031cases hdivision_entry
  32. 0032cases hdivision_entry_witness
  33. 0033cases hdivision_entry_witness_witness
  34. 0034cases hdivision_entry_witness_witness_witness
  35. 0035cases hdivision_entry_witness_witness_witness_right
  36. 0036cases hdivision_entry_witness_witness_witness_right_right
  37. 0037cases hdivision_entry_witness_witness_witness_right_right_right
  38. 0038have hxscaled : x = q * (1 + i)
  39. 0039specialize hscaled i
  40. 0040specialize hscaled x
  41. 0041apply hscaled
  42. 0042exact hi
  43. 0043exact hdivision_entry_witness_witness_witness_left
  44. 0044have hone : 1 + i = S i
  45. 0045trans S (0 + i)
  46. 0046specialize add_succ_left 0
  47. 0047specialize add_succ_left i
  48. 0048exact add_succ_left
  49. 0049congr
  50. 0050specialize zero_add i
  51. 0051exact zero_add
  52. 0052have hxscaled_succ : x = q * S i
  53. 0053trans q * (1 + i)
  54. 0054exact hxscaled
  55. 0055congr
  56. 0056refl
  57. 0057exact hone
  58. 0058have hquotient_eq : x1 = d
  59. 0059specialize beta_at_unique qb
  60. 0060specialize beta_at_unique qc
  61. 0061specialize beta_at_unique i
  62. 0062specialize beta_at_unique x1
  63. 0063specialize beta_at_unique d
  64. 0064apply beta_at_unique
  65. 0065exact hdivision_entry_witness_witness_witness_right_left
  66. 0066exact hdentry
  67. 0067have hdivision : q * S i = p * x1 + x2
  68. 0068trans x
  69. 0069symm
  70. 0070exact hxscaled_succ
  71. 0071exact hdivision_entry_witness_witness_witness_right_right_right_left
  72. 0072have hnq : n = x1
  73. 0073specialize distinct_odd_prime_row_bit_count_equals_division_quotient p
  74. 0074specialize distinct_odd_prime_row_bit_count_equals_division_quotient q
  75. 0075specialize distinct_odd_prime_row_bit_count_equals_division_quotient h
  76. 0076specialize distinct_odd_prime_row_bit_count_equals_division_quotient k
  77. 0077specialize distinct_odd_prime_row_bit_count_equals_division_quotient i
  78. 0078specialize distinct_odd_prime_row_bit_count_equals_division_quotient x1
  79. 0079specialize distinct_odd_prime_row_bit_count_equals_division_quotient x2
  80. 0080specialize distinct_odd_prime_row_bit_count_equals_division_quotient rb
  81. 0081specialize distinct_odd_prime_row_bit_count_equals_division_quotient rc
  82. 0082specialize distinct_odd_prime_row_bit_count_equals_division_quotient n
  83. 0083apply distinct_odd_prime_row_bit_count_equals_division_quotient
  84. 0084exact hpodd
  85. 0085exact hqodd
  86. 0086exact hp
  87. 0087exact hq
  88. 0088exact hpq
  89. 0089exact hi
  90. 0090exact hrow
  91. 0091exact hcount
  92. 0092exact hdivision
  93. 0093exact hdivision_entry_witness_witness_witness_right_right_right_right
  94. 0094trans x1
  95. 0095exact hnq
  96. 0096exact hquotient_eq