PA00DH · theorem

distinct_odd_prime_half_row_count_choices_bounded

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

Every prefix length at most h has semantic row-count choices.

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. ∀ l. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Le(l,h) → ∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y)

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 PD0004 Prime PD0013 BetaAt PD0017 BitCount

11 occurrences

In local proof propositions

PD0002 Lt

1 occurrences

Exact expanded native-PA statement
forall p q h k l. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_rectangle_count_prime_p frp_prime_right_rectangle_count_prime_p. p = frp_prime_left_rectangle_count_prime_p * frp_prime_right_rectangle_count_prime_p -> frp_prime_left_rectangle_count_prime_p = 1 \/ frp_prime_right_rectangle_count_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_rectangle_count_prime_q frp_prime_right_rectangle_count_prime_q. q = frp_prime_left_rectangle_count_prime_q * frp_prime_right_rectangle_count_prime_q -> frp_prime_left_rectangle_count_prime_q = 1 \/ frp_prime_right_rectangle_count_prime_q = 1)) -> ~(p = q) -> (exists erc_le_gap_rectangle_count_length_bound. erc_le_gap_rectangle_count_length_bound + (l) = h) -> (forall erc_row_rectangle_count_bounded_choices. (exists erc_lt_gap_rectangle_count_bounded_choices_bound. erc_lt_gap_rectangle_count_bounded_choices_bound + S (erc_row_rectangle_count_bounded_choices) = l) -> exists erc_count_rectangle_count_bounded_choices. (exists erc_row_code_rectangle_count_bounded_choices_witness erc_row_scale_rectangle_count_bounded_choices_witness. ((forall eri_column_erc_rectangle_count_bounded_choices_witness_row. (exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_bound. eri_gap_erc_rectangle_count_bounded_choices_witness_row_bound + S (eri_column_erc_rectangle_count_bounded_choices_witness_row) = k) -> exists eri_bit_erc_rectangle_count_bounded_choices_witness_row. ((((exists ff_h_eri_erc_rectangle_count_bounded_choices_witness_row_decoded. ff_h_eri_erc_rectangle_count_bounded_choices_witness_row_decoded + S (eri_bit_erc_rectangle_count_bounded_choices_witness_row) = S ((S (eri_column_erc_rectangle_count_bounded_choices_witness_row)) * erc_row_scale_rectangle_count_bounded_choices_witness)) /\ exists ff_q_eri_erc_rectangle_count_bounded_choices_witness_row_decoded. erc_row_code_rectangle_count_bounded_choices_witness = ff_q_eri_erc_rectangle_count_bounded_choices_witness_row_decoded * S ((S (eri_column_erc_rectangle_count_bounded_choices_witness_row)) * erc_row_scale_rectangle_count_bounded_choices_witness) + (eri_bit_erc_rectangle_count_bounded_choices_witness_row))) /\ (((eri_bit_erc_rectangle_count_bounded_choices_witness_row = 0 /\ ((exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_bounded_choices) = p * S eri_column_erc_rectangle_count_bounded_choices_witness_row) /\ ~(exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_bounded_choices_witness_row) = q * S erc_row_rectangle_count_bounded_choices))) \/ (eri_bit_erc_rectangle_count_bounded_choices_witness_row = 1 /\ ((exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_right + S (p * S eri_column_erc_rectangle_count_bounded_choices_witness_row) = q * S erc_row_rectangle_count_bounded_choices) /\ ~(exists eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left. eri_gap_erc_rectangle_count_bounded_choices_witness_row_choice_left + S (q * S erc_row_rectangle_count_bounded_choices) = p * S eri_column_erc_rectangle_count_bounded_choices_witness_row))))))) /\ (((exists ff_u_erc_rectangle_count_bounded_choices_witness_count_sum ff_v_erc_rectangle_count_bounded_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_start. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_start. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_start * S ((S (0)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_terminal. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_terminal + S (erc_count_rectangle_count_bounded_choices) = S ((S (k)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_terminal. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (erc_count_rectangle_count_bounded_choices))) /\ forall ff_i_erc_rectangle_count_bounded_choices_witness_count_sum. (exists ff_lt_erc_rectangle_count_bounded_choices_witness_count_sum_bound. ff_lt_erc_rectangle_count_bounded_choices_witness_count_sum_bound + S ff_i_erc_rectangle_count_bounded_choices_witness_count_sum = k) -> exists ff_a_erc_rectangle_count_bounded_choices_witness_count_sum ff_r_erc_rectangle_count_bounded_choices_witness_count_sum ff_s_erc_rectangle_count_bounded_choices_witness_count_sum. ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_summand. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_summand + S (ff_a_erc_rectangle_count_bounded_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * erc_row_scale_rectangle_count_bounded_choices_witness)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_summand. erc_row_code_rectangle_count_bounded_choices_witness = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_summand * S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * erc_row_scale_rectangle_count_bounded_choices_witness) + (ff_a_erc_rectangle_count_bounded_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_partial. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_partial + S (ff_r_erc_rectangle_count_bounded_choices_witness_count_sum) = S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_partial. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_partial * S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (ff_r_erc_rectangle_count_bounded_choices_witness_count_sum))) /\ ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_successor. ff_h_erc_rectangle_count_bounded_choices_witness_count_sum_successor + S (ff_s_erc_rectangle_count_bounded_choices_witness_count_sum) = S ((S (S ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_successor. ff_u_erc_rectangle_count_bounded_choices_witness_count_sum = ff_q_erc_rectangle_count_bounded_choices_witness_count_sum_successor * S ((S (S ff_i_erc_rectangle_count_bounded_choices_witness_count_sum)) * ff_v_erc_rectangle_count_bounded_choices_witness_count_sum) + (ff_s_erc_rectangle_count_bounded_choices_witness_count_sum))) /\ ff_s_erc_rectangle_count_bounded_choices_witness_count_sum = ff_r_erc_rectangle_count_bounded_choices_witness_count_sum + ff_a_erc_rectangle_count_bounded_choices_witness_count_sum)))))) /\ (forall ff_i_erc_rectangle_count_bounded_choices_witness_count_bits. (exists ff_lt_erc_rectangle_count_bounded_choices_witness_count_bits_bound. ff_lt_erc_rectangle_count_bounded_choices_witness_count_bits_bound + S ff_i_erc_rectangle_count_bounded_choices_witness_count_bits = k) -> exists ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits. ((((exists ff_h_erc_rectangle_count_bounded_choices_witness_count_bits_decoded. ff_h_erc_rectangle_count_bounded_choices_witness_count_bits_decoded + S (ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits) = S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_bits)) * erc_row_scale_rectangle_count_bounded_choices_witness)) /\ exists ff_q_erc_rectangle_count_bounded_choices_witness_count_bits_decoded. erc_row_code_rectangle_count_bounded_choices_witness = ff_q_erc_rectangle_count_bounded_choices_witness_count_bits_decoded * S ((S (ff_i_erc_rectangle_count_bounded_choices_witness_count_bits)) * erc_row_scale_rectangle_count_bounded_choices_witness) + (ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits))) /\ (ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits = 0 \/ ff_bit_erc_rectangle_count_bounded_choices_witness_count_bits = 1))))))))

Proof neighborhood

Direct theorem prerequisites

PA006L lt_of_lt_of_le PA00DG distinct_odd_prime_half_row_count_choice

Direct theorem dependents

PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded

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

32 script commands · 4 reading checkpoints · 1 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 (2)
lt of lt of ledistinct odd prime half row count choice
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 l
  6. L6
    intro hpodd
  7. L7
    intro hqodd
  8. L8
    intro hp
  9. L9
    intro hq
  10. L10
    intro hpq
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hlh
  2. L12
    intro i
  3. L13
    intro hil
03Establish hihL14–23

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

  1. L14
  2. L15
    specialize lt_of_lt_of_le i
  3. L16
    specialize lt_of_lt_of_le l
  4. L17
    specialize lt_of_lt_of_le h
  5. L18
    apply lt_of_lt_of_le
  6. L19
    exact hil
  7. L20
    exact hlh
  8. L21
    specialize distinct_odd_prime_half_row_count_choice p
  9. L22
    specialize distinct_odd_prime_half_row_count_choice q
  10. L23
    specialize distinct_odd_prime_half_row_count_choice h
04Use earlier factsL24–32

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

  1. L24
    specialize distinct_odd_prime_half_row_count_choice k
  2. L25
    specialize distinct_odd_prime_half_row_count_choice i
  3. L26
    apply distinct_odd_prime_half_row_count_choice
  4. L27
    exact hpodd
  5. L28
    exact hqodd
  6. L29
    exact hp
  7. L30
    exact hq
  8. L31
    exact hpq
  9. L32
    exact hih

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro l
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hlh
  12. 0012intro i
  13. 0013intro hil
  14. 0014have hih : Lt(i,h)
    Exact native replay linehave hih : exists erc_lt_gap_rectangle_count_row_bound. erc_lt_gap_rectangle_count_row_bound + S (i) = h
  15. 0015specialize lt_of_lt_of_le i
  16. 0016specialize lt_of_lt_of_le l
  17. 0017specialize lt_of_lt_of_le h
  18. 0018apply lt_of_lt_of_le
  19. 0019exact hil
  20. 0020exact hlh
  21. 0021specialize distinct_odd_prime_half_row_count_choice p
  22. 0022specialize distinct_odd_prime_half_row_count_choice q
  23. 0023specialize distinct_odd_prime_half_row_count_choice h
  24. 0024specialize distinct_odd_prime_half_row_count_choice k
  25. 0025specialize distinct_odd_prime_half_row_count_choice i
  26. 0026apply distinct_odd_prime_half_row_count_choice
  27. 0027exact hpodd
  28. 0028exact hqodd
  29. 0029exact hp
  30. 0030exact hq
  31. 0031exact hpq
  32. 0032exact hih