PA00F5 · theorem

eisenstein_cell_indicator_choice_unique

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

The exact orientation predicate determines its zero-or-one indicator uniquely.

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. ∀ i. ∀ j. ∀ a. ∀ d. a = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ a = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) → d = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ d = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) → a = d

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

8 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p q i j a d. (((a = 0 /\ ((exists eri_gap_fubini_cell_choice_unique_first_left. eri_gap_fubini_cell_choice_unique_first_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_fubini_cell_choice_unique_first_right. eri_gap_fubini_cell_choice_unique_first_right + S (p * S j) = q * S i))) \/ (a = 1 /\ ((exists eri_gap_fubini_cell_choice_unique_first_right. eri_gap_fubini_cell_choice_unique_first_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_fubini_cell_choice_unique_first_left. eri_gap_fubini_cell_choice_unique_first_left + S (q * S i) = p * S j))))) -> (((d = 0 /\ ((exists eri_gap_fubini_cell_choice_unique_second_left. eri_gap_fubini_cell_choice_unique_second_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_fubini_cell_choice_unique_second_right. eri_gap_fubini_cell_choice_unique_second_right + S (p * S j) = q * S i))) \/ (d = 1 /\ ((exists eri_gap_fubini_cell_choice_unique_second_right. eri_gap_fubini_cell_choice_unique_second_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_fubini_cell_choice_unique_second_left. eri_gap_fubini_cell_choice_unique_second_left + S (q * S i) = p * S j))))) -> a = d

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA00F6 eisenstein_transposed_column_counts_extensional PA00F9 eisenstein_successor_terminal_bit_matches_last_column

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

35 script commands · 15 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.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro i
  4. L4
    intro j
  5. L5
    intro a
  6. L6
    intro d
  7. L7
    intro ha
  8. L8
    intro hd
02Separate the logical casesL9–13

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

  1. L9
    cases ha
  2. L10
    cases ha_left
  3. L11
    cases ha_left_right
  4. L12
    cases hd
  5. L13
    cases hd_left
03Calculate and transport equalitiesL14–14

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

  1. L14
    trans 0
04Use earlier factsL15–15

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

  1. L15
    exact ha_left_left
05Calculate and transport equalitiesL16–16

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

  1. L16
    symm
06Use earlier factsL17–17

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

  1. L17
    exact hd_left_left
07Separate the logical casesL18–20

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

  1. L18
    cases hd_right
  2. L19
    cases hd_right_right
  3. L20
    exfalso
08Use earlier factsL21–22

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

  1. L21
    apply hd_right_right_right
  2. L22
    exact ha_left_right_left
09Separate the logical casesL23–28

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

  1. L23
    cases ha_right
  2. L24
    cases ha_right_right
  3. L25
    cases hd
  4. L26
    cases hd_left
  5. L27
    cases hd_left_right
  6. L28
    exfalso
10Use earlier factsL29–30

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

  1. L29
    apply ha_right_right_right
  2. L30
    exact hd_left_right_left
11Separate the logical casesL31–31

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

  1. L31
    cases hd_right
12Calculate and transport equalitiesL32–32

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

  1. L32
    trans 1
13Use earlier factsL33–33

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

  1. L33
    exact ha_right_left
14Calculate and transport equalitiesL34–34

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

  1. L34
    symm
15Use earlier factsL35–35

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

  1. L35
    exact hd_right_left

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004intro j
  5. 0005intro a
  6. 0006intro d
  7. 0007intro ha
  8. 0008intro hd
  9. 0009cases ha
  10. 0010cases ha_left
  11. 0011cases ha_left_right
  12. 0012cases hd
  13. 0013cases hd_left
  14. 0014trans 0
  15. 0015exact ha_left_left
  16. 0016symm
  17. 0017exact hd_left_left
  18. 0018cases hd_right
  19. 0019cases hd_right_right
  20. 0020exfalso
  21. 0021apply hd_right_right_right
  22. 0022exact ha_left_right_left
  23. 0023cases ha_right
  24. 0024cases ha_right_right
  25. 0025cases hd
  26. 0026cases hd_left
  27. 0027cases hd_left_right
  28. 0028exfalso
  29. 0029apply ha_right_right_right
  30. 0030exact hd_left_right_left
  31. 0031cases hd_right
  32. 0032trans 1
  33. 0033exact ha_right_left
  34. 0034symm
  35. 0035exact hd_right_left