PA00DB

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.

Exact expanded 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))))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites distinct_odd_prime_half_cell_indicator_choice as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA00DA distinct_odd_prime_half_cell_indicator_choice

Proof neighborhood

Direct dependencies

PA00DA distinct_odd_prime_half_cell_indicator_choice

Direct dependents

PA00DF distinct_odd_prime_half_row_count_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

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 exact 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