PA00D9 · theorem

distinct_odd_prime_half_cell_oriented

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

Every bounded half-rectangle cell has one exclusive orientation.

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) → 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)

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

PD0001 Le

2 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_lattice_prime_p frp_prime_right_lattice_prime_p. p = frp_prime_left_lattice_prime_p * frp_prime_right_lattice_prime_p -> frp_prime_left_lattice_prime_p = 1 \/ frp_prime_right_lattice_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_lattice_prime_q frp_prime_right_lattice_prime_q. q = frp_prime_left_lattice_prime_q * frp_prime_right_lattice_prime_q -> frp_prime_left_lattice_prime_q = 1 \/ frp_prime_right_lattice_prime_q = 1)) -> ~(p = q) -> (exists elo_gap_lattice_i_bound. elo_gap_lattice_i_bound + S (i) = h) -> (exists elo_gap_lattice_j_bound. elo_gap_lattice_j_bound + S (j) = k) -> ((((exists elo_gap_lattice_cell_result_left. elo_gap_lattice_cell_result_left + S (q * S i) = p * S j) /\ ~(exists elo_gap_lattice_cell_result_right. elo_gap_lattice_cell_result_right + S (p * S j) = q * S i)) \/ ((exists elo_gap_lattice_cell_result_right. elo_gap_lattice_cell_result_right + S (p * S j) = q * S i) /\ ~(exists elo_gap_lattice_cell_result_left. elo_gap_lattice_cell_result_left + S (q * S i) = p * S j))))

Proof neighborhood

Direct theorem prerequisites

PA00D8 distinct_odd_prime_half_products_ne PA0011 lt_trichotomy PA000X lt_to_le PA003A lt_not_le

Direct theorem dependents

PA00DA distinct_odd_prime_half_cell_indicator_choice

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

65 script commands · 14 reading checkpoints · 3 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)
distinct odd prime half products nelt trichotomylt to lelt not le
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 hneL14–23

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

  1. L14
    have hne : ~(q * S i = p * S j)
  2. L15
    intro heq
  3. L16
    specialize distinct_odd_prime_half_products_ne p
  4. L17
    specialize distinct_odd_prime_half_products_ne q
  5. L18
    specialize distinct_odd_prime_half_products_ne h
  6. L19
    specialize distinct_odd_prime_half_products_ne k
  7. L20
    specialize distinct_odd_prime_half_products_ne i
  8. L21
    specialize distinct_odd_prime_half_products_ne j
  9. L22
    apply distinct_odd_prime_half_products_ne
  10. L23
    exact hpodd
04Use earlier factsL24–32

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

  1. L24
    exact hqodd
  2. L25
    exact hp
  3. L26
    exact hq
  4. L27
    exact hpq
  5. L28
    exact hi
  6. L29
    exact hj
  7. L30
    exact heq
  8. L31
    specialize lt_trichotomy (q * S i)
  9. L32
    specialize lt_trichotomy (p * S j)
05Separate the logical casesL33–34

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

  1. L33
    cases lt_trichotomy
  2. L34
    exfalso
06Use earlier factsL35–36

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

  1. L35
    apply hne
  2. L36
    exact lt_trichotomy_left
07Separate the logical casesL37–39

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

  1. L37
    cases lt_trichotomy_right
  2. L38
    left
  3. L39
    split
08Use earlier factsL40–40

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

  1. L40
    exact lt_trichotomy_right_left
09Fix variables and assumptionsL41–41

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

  1. L41
    intro hreverse
10Establish hleL42–51

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

  1. L42
    have hle : Le(p · S j,q · S i)Definitions: Le(p · S j,q · S i)Original native command in the exact edition
  2. L43
    specialize lt_to_le (p * S j)
  3. L44
    specialize lt_to_le (q * S i)
  4. L45
    apply lt_to_le
  5. L46
    exact hreverse
  6. L47
    specialize lt_not_le (q * S i)
  7. L48
    specialize lt_not_le (p * S j)
  8. L49
    apply lt_not_le
  9. L50
    exact lt_trichotomy_right_left
  10. L51
    exact hle
11Separate the logical casesL52–53

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

  1. L52
    right
  2. L53
    split
12Use earlier factsL54–54

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

  1. L54
    exact lt_trichotomy_right_right
13Fix variables and assumptionsL55–55

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

  1. L55
    intro hreverse
14Establish hleL56–65

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

  1. L56
    have hle : Le(q · S i,p · S j)Definitions: Le(q · S i,p · S j)Original native command in the exact edition
  2. L57
    specialize lt_to_le (q * S i)
  3. L58
    specialize lt_to_le (p * S j)
  4. L59
    apply lt_to_le
  5. L60
    exact hreverse
  6. L61
    specialize lt_not_le (p * S j)
  7. L62
    specialize lt_not_le (q * S i)
  8. L63
    apply lt_not_le
  9. L64
    exact lt_trichotomy_right_right
  10. L65
    exact hle

Library-wide reading audit

Original defined command ledger · 65 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 hne : ~(q * S i = p * S j)
  15. 0015intro heq
  16. 0016specialize distinct_odd_prime_half_products_ne p
  17. 0017specialize distinct_odd_prime_half_products_ne q
  18. 0018specialize distinct_odd_prime_half_products_ne h
  19. 0019specialize distinct_odd_prime_half_products_ne k
  20. 0020specialize distinct_odd_prime_half_products_ne i
  21. 0021specialize distinct_odd_prime_half_products_ne j
  22. 0022apply distinct_odd_prime_half_products_ne
  23. 0023exact hpodd
  24. 0024exact hqodd
  25. 0025exact hp
  26. 0026exact hq
  27. 0027exact hpq
  28. 0028exact hi
  29. 0029exact hj
  30. 0030exact heq
  31. 0031specialize lt_trichotomy (q * S i)
  32. 0032specialize lt_trichotomy (p * S j)
  33. 0033cases lt_trichotomy
  34. 0034exfalso
  35. 0035apply hne
  36. 0036exact lt_trichotomy_left
  37. 0037cases lt_trichotomy_right
  38. 0038left
  39. 0039split
  40. 0040exact lt_trichotomy_right_left
  41. 0041intro hreverse
  42. 0042have hle : Le(p · S j,q · S i)
    Exact native replay linehave hle : exists gap. gap + (p * S j) = q * S i
  43. 0043specialize lt_to_le (p * S j)
  44. 0044specialize lt_to_le (q * S i)
  45. 0045apply lt_to_le
  46. 0046exact hreverse
  47. 0047specialize lt_not_le (q * S i)
  48. 0048specialize lt_not_le (p * S j)
  49. 0049apply lt_not_le
  50. 0050exact lt_trichotomy_right_left
  51. 0051exact hle
  52. 0052right
  53. 0053split
  54. 0054exact lt_trichotomy_right_right
  55. 0055intro hreverse
  56. 0056have hle : Le(q · S i,p · S j)
    Exact native replay linehave hle : exists gap. gap + (q * S i) = p * S j
  57. 0057specialize lt_to_le (q * S i)
  58. 0058specialize lt_to_le (p * S j)
  59. 0059apply lt_to_le
  60. 0060exact hreverse
  61. 0061specialize lt_not_le (p * S j)
  62. 0062specialize lt_not_le (q * S i)
  63. 0063apply lt_not_le
  64. 0064exact lt_trichotomy_right_right
  65. 0065exact hle