PA00EC · theorem

eisenstein_transposed_decoded_cell_bits_complementary

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

A decoded cell bit and its swapped-row transpose are exact complements.

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. ∀ rb. ∀ rc. ∀ cb. ∀ cc. ∀ a. ∀ d. (∀ x. Lt(x,k) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) → (∀ x. Lt(x,h) → ∃ y. BetaAt(cb,cc,x,y) ∧ (y = 0 ∧ (Lt(p · S j,q · S x) ∧ ¬Lt(q · S x,p · S j)) ∨ y = 1 ∧ (Lt(q · S x,p · S j) ∧ ¬Lt(p · S j,q · S x)))) → Lt(j,k) → Lt(i,h) → BetaAt(rb,rc,j,a) → BetaAt(cb,cc,i,d) → a = 0 ∧ d = 1 ∨ a = 1 ∧ d = 0

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 PD0013 BetaAt

16 occurrences

In local proof propositions

PD0002 Lt

8 occurrences

Exact expanded native-PA statement
forall p q h k i j rb rc cb cc a d. (forall eri_column_transpose_row. (exists eri_gap_transpose_row_bound. eri_gap_transpose_row_bound + S (eri_column_transpose_row) = k) -> exists eri_bit_transpose_row. ((((exists ff_h_eri_transpose_row_decoded. ff_h_eri_transpose_row_decoded + S (eri_bit_transpose_row) = S ((S (eri_column_transpose_row)) * rc)) /\ exists ff_q_eri_transpose_row_decoded. rb = ff_q_eri_transpose_row_decoded * S ((S (eri_column_transpose_row)) * rc) + (eri_bit_transpose_row))) /\ (((eri_bit_transpose_row = 0 /\ ((exists eri_gap_transpose_row_choice_left. eri_gap_transpose_row_choice_left + S (q * S i) = p * S eri_column_transpose_row) /\ ~(exists eri_gap_transpose_row_choice_right. eri_gap_transpose_row_choice_right + S (p * S eri_column_transpose_row) = q * S i))) \/ (eri_bit_transpose_row = 1 /\ ((exists eri_gap_transpose_row_choice_right. eri_gap_transpose_row_choice_right + S (p * S eri_column_transpose_row) = q * S i) /\ ~(exists eri_gap_transpose_row_choice_left. eri_gap_transpose_row_choice_left + S (q * S i) = p * S eri_column_transpose_row))))))) -> (forall eri_column_transpose_column. (exists eri_gap_transpose_column_bound. eri_gap_transpose_column_bound + S (eri_column_transpose_column) = h) -> exists eri_bit_transpose_column. ((((exists ff_h_eri_transpose_column_decoded. ff_h_eri_transpose_column_decoded + S (eri_bit_transpose_column) = S ((S (eri_column_transpose_column)) * cc)) /\ exists ff_q_eri_transpose_column_decoded. cb = ff_q_eri_transpose_column_decoded * S ((S (eri_column_transpose_column)) * cc) + (eri_bit_transpose_column))) /\ (((eri_bit_transpose_column = 0 /\ ((exists eri_gap_transpose_column_choice_left. eri_gap_transpose_column_choice_left + S (p * S j) = q * S eri_column_transpose_column) /\ ~(exists eri_gap_transpose_column_choice_right. eri_gap_transpose_column_choice_right + S (q * S eri_column_transpose_column) = p * S j))) \/ (eri_bit_transpose_column = 1 /\ ((exists eri_gap_transpose_column_choice_right. eri_gap_transpose_column_choice_right + S (q * S eri_column_transpose_column) = p * S j) /\ ~(exists eri_gap_transpose_column_choice_left. eri_gap_transpose_column_choice_left + S (p * S j) = q * S eri_column_transpose_column))))))) -> (exists gap. gap + S j = k) -> (exists gap. gap + S i = h) -> (((exists ff_h_transpose_row_entry. ff_h_transpose_row_entry + S (a) = S ((S (j)) * rc)) /\ exists ff_q_transpose_row_entry. rb = ff_q_transpose_row_entry * S ((S (j)) * rc) + (a))) -> (((exists ff_h_transpose_column_entry. ff_h_transpose_column_entry + S (d) = S ((S (i)) * cc)) /\ exists ff_q_transpose_column_entry. cb = ff_q_transpose_column_entry * S ((S (i)) * cc) + (d))) -> ((a = 0 /\ d = 1) \/ (a = 1 /\ d = 0))

Proof neighborhood

Direct theorem prerequisites

PA00EA eisenstein_row_indicator_decoded_choice

Direct theorem dependents

PA00ED eisenstein_transposed_column_pointwise_complement

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

71 script commands · 14 reading checkpoints · 2 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)
eisenstein row indicator decoded 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 j
  7. L7
    intro rb
  8. L8
    intro rc
  9. L9
    intro cb
  10. L10
    intro cc
02Fix variables and assumptionsL11–18

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

  1. L11
    intro a
  2. L12
    intro d
  3. L13
    intro hrow
  4. L14
    intro htransposed_row
  5. L15
    intro hj
  6. L16
    intro hi
  7. L17
    intro ha
  8. L18
    intro hd
03Establish horiginalL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein row indicator decoded choice.

  1. L19
    have horiginal : 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))Definitions: Lt(q · S i,p · S j)Lt(p · S j,q · S i)Original native command in the exact edition
  2. L20
    specialize eisenstein_row_indicator_decoded_choice p
  3. L21
    specialize eisenstein_row_indicator_decoded_choice q
  4. L22
    specialize eisenstein_row_indicator_decoded_choice i
  5. L23
    specialize eisenstein_row_indicator_decoded_choice rb
  6. L24
    specialize eisenstein_row_indicator_decoded_choice rc
  7. L25
    specialize eisenstein_row_indicator_decoded_choice k
  8. L26
    specialize eisenstein_row_indicator_decoded_choice j
  9. L27
    specialize eisenstein_row_indicator_decoded_choice a
  10. L28
    apply eisenstein_row_indicator_decoded_choice
04Use earlier factsL29–31

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

  1. L29
    exact hrow
  2. L30
    exact hj
  3. L31
    exact ha
05Establish htransposedL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein row indicator decoded choice.

  1. L32
    have htransposed : d = 0 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) ∨ d = 1 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i))Definitions: Lt(p · S j,q · S i)Lt(q · S i,p · S j)Original native command in the exact edition
  2. L33
    specialize eisenstein_row_indicator_decoded_choice q
  3. L34
    specialize eisenstein_row_indicator_decoded_choice p
  4. L35
    specialize eisenstein_row_indicator_decoded_choice j
  5. L36
    specialize eisenstein_row_indicator_decoded_choice cb
  6. L37
    specialize eisenstein_row_indicator_decoded_choice cc
  7. L38
    specialize eisenstein_row_indicator_decoded_choice h
  8. L39
    specialize eisenstein_row_indicator_decoded_choice i
  9. L40
    specialize eisenstein_row_indicator_decoded_choice d
  10. L41
    apply eisenstein_row_indicator_decoded_choice
06Use earlier factsL42–44

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

  1. L42
    exact htransposed_row
  2. L43
    exact hi
  3. L44
    exact hd
07Separate the logical casesL45–51

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

  1. L45
    cases horiginal
  2. L46
    cases horiginal_left
  3. L47
    cases horiginal_left_right
  4. L48
    cases htransposed
  5. L49
    cases htransposed_left
  6. L50
    cases htransposed_left_right
  7. L51
    exfalso
08Use earlier factsL52–53

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

  1. L52
    apply horiginal_left_right_right
  2. L53
    exact htransposed_left_right_left
09Separate the logical casesL54–56

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

  1. L54
    cases htransposed_right
  2. L55
    left
  3. L56
    split
10Use earlier factsL57–58

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

  1. L57
    exact horiginal_left_left
  2. L58
    exact htransposed_right_left
11Separate the logical casesL59–64

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

  1. L59
    cases horiginal_right
  2. L60
    cases horiginal_right_right
  3. L61
    cases htransposed
  4. L62
    cases htransposed_left
  5. L63
    right
  6. L64
    split
12Use earlier factsL65–66

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

  1. L65
    exact horiginal_right_left
  2. L66
    exact htransposed_left_left
13Separate the logical casesL67–69

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

  1. L67
    cases htransposed_right
  2. L68
    cases htransposed_right_right
  3. L69
    exfalso
14Use earlier factsL70–71

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

  1. L70
    apply horiginal_right_right_right
  2. L71
    exact htransposed_right_right_left

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro j
  7. 0007intro rb
  8. 0008intro rc
  9. 0009intro cb
  10. 0010intro cc
  11. 0011intro a
  12. 0012intro d
  13. 0013intro hrow
  14. 0014intro htransposed_row
  15. 0015intro hj
  16. 0016intro hi
  17. 0017intro ha
  18. 0018intro hd
  19. 0019have horiginal : 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))
    Exact native replay linehave horiginal : ((a = 0 /\ ((exists eri_gap_transpose_row_choice_left. eri_gap_transpose_row_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_transpose_row_choice_right. eri_gap_transpose_row_choice_right + S (p * S j) = q * S i))) \/ (a = 1 /\ ((exists eri_gap_transpose_row_choice_right. eri_gap_transpose_row_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_transpose_row_choice_left. eri_gap_transpose_row_choice_left + S (q * S i) = p * S j))))
  20. 0020specialize eisenstein_row_indicator_decoded_choice p
  21. 0021specialize eisenstein_row_indicator_decoded_choice q
  22. 0022specialize eisenstein_row_indicator_decoded_choice i
  23. 0023specialize eisenstein_row_indicator_decoded_choice rb
  24. 0024specialize eisenstein_row_indicator_decoded_choice rc
  25. 0025specialize eisenstein_row_indicator_decoded_choice k
  26. 0026specialize eisenstein_row_indicator_decoded_choice j
  27. 0027specialize eisenstein_row_indicator_decoded_choice a
  28. 0028apply eisenstein_row_indicator_decoded_choice
  29. 0029exact hrow
  30. 0030exact hj
  31. 0031exact ha
  32. 0032have htransposed : d = 0 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)) ∨ d = 1 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i))
    Exact native replay linehave htransposed : ((d = 0 /\ ((exists eri_gap_transpose_column_choice_left. eri_gap_transpose_column_choice_left + S (p * S j) = q * S i) /\ ~(exists eri_gap_transpose_column_choice_right. eri_gap_transpose_column_choice_right + S (q * S i) = p * S j))) \/ (d = 1 /\ ((exists eri_gap_transpose_column_choice_right. eri_gap_transpose_column_choice_right + S (q * S i) = p * S j) /\ ~(exists eri_gap_transpose_column_choice_left. eri_gap_transpose_column_choice_left + S (p * S j) = q * S i))))
  33. 0033specialize eisenstein_row_indicator_decoded_choice q
  34. 0034specialize eisenstein_row_indicator_decoded_choice p
  35. 0035specialize eisenstein_row_indicator_decoded_choice j
  36. 0036specialize eisenstein_row_indicator_decoded_choice cb
  37. 0037specialize eisenstein_row_indicator_decoded_choice cc
  38. 0038specialize eisenstein_row_indicator_decoded_choice h
  39. 0039specialize eisenstein_row_indicator_decoded_choice i
  40. 0040specialize eisenstein_row_indicator_decoded_choice d
  41. 0041apply eisenstein_row_indicator_decoded_choice
  42. 0042exact htransposed_row
  43. 0043exact hi
  44. 0044exact hd
  45. 0045cases horiginal
  46. 0046cases horiginal_left
  47. 0047cases horiginal_left_right
  48. 0048cases htransposed
  49. 0049cases htransposed_left
  50. 0050cases htransposed_left_right
  51. 0051exfalso
  52. 0052apply horiginal_left_right_right
  53. 0053exact htransposed_left_right_left
  54. 0054cases htransposed_right
  55. 0055left
  56. 0056split
  57. 0057exact horiginal_left_left
  58. 0058exact htransposed_right_left
  59. 0059cases horiginal_right
  60. 0060cases horiginal_right_right
  61. 0061cases htransposed
  62. 0062cases htransposed_left
  63. 0063right
  64. 0064split
  65. 0065exact horiginal_right_left
  66. 0066exact htransposed_left_left
  67. 0067cases htransposed_right
  68. 0068cases htransposed_right_right
  69. 0069exfalso
  70. 0070apply horiginal_right_right_right
  71. 0071exact htransposed_right_right_left