PA00F5

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.

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

Structural proof guide

Generated structural guide

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

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by case analysis (13).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00F6 eisenstein_transposed_column_counts_extensional PA00F9 eisenstein_successor_terminal_bit_matches_last_column

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

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.

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