PA00DA · theorem

distinct_odd_prime_half_cell_indicator_choice

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

Every bounded lattice cell has a constructive exact indicator bit.

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

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

PD0002 Lt

4 occurrences

Exact expanded native-PA statement
forall p q h k i j. 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) -> (exists eri_gap_row_indicator_j_bound. eri_gap_row_indicator_j_bound + S (j) = k) -> exists bit. (((bit = 0 /\ ((exists eri_gap_row_indicator_point_result_left. eri_gap_row_indicator_point_result_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_point_result_right. eri_gap_row_indicator_point_result_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_point_result_right. eri_gap_row_indicator_point_result_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_point_result_left. eri_gap_row_indicator_point_result_left + S (q * S i) = p * S j)))))

Proof neighborhood

Direct theorem prerequisites

PA00D9 distinct_odd_prime_half_cell_oriented

Direct theorem dependents

PA00DB distinct_odd_prime_half_row_indicator_choices

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

39 script commands · 13 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 (1)
distinct odd prime half cell oriented
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 j
  7. L7
    intro hpodd
  8. L8
    intro hqodd
  9. L9
    intro hp
  10. L10
    intro hq
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hpq
  2. L12
    intro hi
  3. L13
    intro hj
03Establish horientationL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half cell oriented.

  1. L14
    have horientation : Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i) ∨ Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)Definitions: Lt(q · S i,p · S j)Lt(p · S j,q · S i)Original native command in the exact edition
  2. L15
    specialize distinct_odd_prime_half_cell_oriented p
  3. L16
    specialize distinct_odd_prime_half_cell_oriented q
  4. L17
    specialize distinct_odd_prime_half_cell_oriented h
  5. L18
    specialize distinct_odd_prime_half_cell_oriented k
  6. L19
    specialize distinct_odd_prime_half_cell_oriented i
  7. L20
    specialize distinct_odd_prime_half_cell_oriented j
  8. L21
    apply distinct_odd_prime_half_cell_oriented
  9. L22
    exact hpodd
  10. L23
    exact hqodd
04Use earlier factsL24–28

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

  1. L24
    exact hp
  2. L25
    exact hq
  3. L26
    exact hpq
  4. L27
    exact hi
  5. L28
    exact hj
05Separate the logical casesL29–29

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

  1. L29
    cases horientation
06Construct an explicit witnessL30–30

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists 0
07Separate the logical casesL31–32

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

  1. L31
    left
  2. L32
    split
08Calculate and transport equalitiesL33–33

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

  1. L33
    refl
09Use earlier factsL34–34

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

  1. L34
    exact horientation_left
10Construct an explicit witnessL35–35

Supply the displayed value, then prove that it has the required property.

  1. L35
    exists 1
11Separate the logical casesL36–37

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

  1. L36
    right
  2. L37
    split
12Calculate and transport equalitiesL38–38

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

  1. L38
    refl
13Use earlier factsL39–39

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

  1. L39
    exact horientation_right

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro j
  7. 0007intro hpodd
  8. 0008intro hqodd
  9. 0009intro hp
  10. 0010intro hq
  11. 0011intro hpq
  12. 0012intro hi
  13. 0013intro hj
  14. 0014have horientation : Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i) ∨ Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)
    Exact native replay linehave horientation : (((exists elo_gap_row_indicator_point_orientation_left. elo_gap_row_indicator_point_orientation_left + S (q * S i) = p * S j) /\ ~(exists elo_gap_row_indicator_point_orientation_right. elo_gap_row_indicator_point_orientation_right + S (p * S j) = q * S i)) \/ ((exists elo_gap_row_indicator_point_orientation_right. elo_gap_row_indicator_point_orientation_right + S (p * S j) = q * S i) /\ ~(exists elo_gap_row_indicator_point_orientation_left. elo_gap_row_indicator_point_orientation_left + S (q * S i) = p * S j)))
  15. 0015specialize distinct_odd_prime_half_cell_oriented p
  16. 0016specialize distinct_odd_prime_half_cell_oriented q
  17. 0017specialize distinct_odd_prime_half_cell_oriented h
  18. 0018specialize distinct_odd_prime_half_cell_oriented k
  19. 0019specialize distinct_odd_prime_half_cell_oriented i
  20. 0020specialize distinct_odd_prime_half_cell_oriented j
  21. 0021apply distinct_odd_prime_half_cell_oriented
  22. 0022exact hpodd
  23. 0023exact hqodd
  24. 0024exact hp
  25. 0025exact hq
  26. 0026exact hpq
  27. 0027exact hi
  28. 0028exact hj
  29. 0029cases horientation
  30. 0030exists 0
  31. 0031left
  32. 0032split
  33. 0033refl
  34. 0034exact horientation_left
  35. 0035exists 1
  36. 0036right
  37. 0037split
  38. 0038refl
  39. 0039exact horientation_right