PA00DB · theorem

distinct_odd_prime_half_row_indicator_choices

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

A fixed bounded row has a constructive exact bit choice in every column.

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. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → ∀ x. Lt(x,k) → ∃ 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))

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

8 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p q h k i. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_indicator_prime_p frp_prime_right_row_indicator_prime_p. p = frp_prime_left_row_indicator_prime_p * frp_prime_right_row_indicator_prime_p -> frp_prime_left_row_indicator_prime_p = 1 \/ frp_prime_right_row_indicator_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_indicator_prime_q frp_prime_right_row_indicator_prime_q. q = frp_prime_left_row_indicator_prime_q * frp_prime_right_row_indicator_prime_q -> frp_prime_left_row_indicator_prime_q = 1 \/ frp_prime_right_row_indicator_prime_q = 1)) -> ~(p = q) -> (exists eri_gap_row_indicator_i_bound. eri_gap_row_indicator_i_bound + S (i) = h) -> (forall eri_column_row_indicator_concrete_choices. (exists eri_gap_row_indicator_concrete_choices_bound. eri_gap_row_indicator_concrete_choices_bound + S (eri_column_row_indicator_concrete_choices) = k) -> exists eri_bit_row_indicator_concrete_choices. (((eri_bit_row_indicator_concrete_choices = 0 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i))) \/ (eri_bit_row_indicator_concrete_choices = 1 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices))))))

Proof neighborhood

Direct theorem prerequisites

PA00DA distinct_odd_prime_half_cell_indicator_choice

Direct theorem dependents

PA00DF distinct_odd_prime_half_row_count_exists

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

27 script commands · 4 reading checkpoints · 0 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 (1)
distinct odd prime half cell indicator 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 i
  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 hi
  2. L12
    intro j
  3. L13
    intro hj
03Use earlier factsL14–23

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

  1. L14
    specialize distinct_odd_prime_half_cell_indicator_choice p
  2. L15
    specialize distinct_odd_prime_half_cell_indicator_choice q
  3. L16
    specialize distinct_odd_prime_half_cell_indicator_choice h
  4. L17
    specialize distinct_odd_prime_half_cell_indicator_choice k
  5. L18
    specialize distinct_odd_prime_half_cell_indicator_choice i
  6. L19
    specialize distinct_odd_prime_half_cell_indicator_choice j
  7. L20
    apply distinct_odd_prime_half_cell_indicator_choice
  8. L21
    exact hpodd
  9. L22
    exact hqodd
  10. L23
    exact hp
04Use earlier factsL24–27

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

  1. L24
    exact hq
  2. L25
    exact hpq
  3. L26
    exact hi
  4. L27
    exact hj

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hi
  12. 0012intro j
  13. 0013intro hj
  14. 0014specialize distinct_odd_prime_half_cell_indicator_choice p
  15. 0015specialize distinct_odd_prime_half_cell_indicator_choice q
  16. 0016specialize distinct_odd_prime_half_cell_indicator_choice h
  17. 0017specialize distinct_odd_prime_half_cell_indicator_choice k
  18. 0018specialize distinct_odd_prime_half_cell_indicator_choice i
  19. 0019specialize distinct_odd_prime_half_cell_indicator_choice j
  20. 0020apply distinct_odd_prime_half_cell_indicator_choice
  21. 0021exact hpodd
  22. 0022exact hqodd
  23. 0023exact hp
  24. 0024exact hq
  25. 0025exact hpq
  26. 0026exact hi
  27. 0027exact hj