PA00DD · theorem

eisenstein_row_indicator_prefix_exists

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

Every finite family of exact cell choices has a beta-coded row prefix.

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. ∀ l. (∀ x. Lt(x,l) → ∃ 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. ∃ y. ∀ z. Lt(z,l) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))

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

11 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

21 occurrences

Exact expanded native-PA statement
forall p q i l. (forall eri_column_row_indicator_exists_all. (exists eri_gap_row_indicator_exists_all_bound. eri_gap_row_indicator_exists_all_bound + S (eri_column_row_indicator_exists_all) = l) -> exists eri_bit_row_indicator_exists_all. (((eri_bit_row_indicator_exists_all = 0 /\ ((exists eri_gap_row_indicator_exists_all_choice_left. eri_gap_row_indicator_exists_all_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_all) /\ ~(exists eri_gap_row_indicator_exists_all_choice_right. eri_gap_row_indicator_exists_all_choice_right + S (p * S eri_column_row_indicator_exists_all) = q * S i))) \/ (eri_bit_row_indicator_exists_all = 1 /\ ((exists eri_gap_row_indicator_exists_all_choice_right. eri_gap_row_indicator_exists_all_choice_right + S (p * S eri_column_row_indicator_exists_all) = q * S i) /\ ~(exists eri_gap_row_indicator_exists_all_choice_left. eri_gap_row_indicator_exists_all_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_all)))))) -> (exists rb rc. (forall eri_column_row_indicator_exists_result. (exists eri_gap_row_indicator_exists_result_bound. eri_gap_row_indicator_exists_result_bound + S (eri_column_row_indicator_exists_result) = l) -> exists eri_bit_row_indicator_exists_result. ((((exists ff_h_eri_row_indicator_exists_result_decoded. ff_h_eri_row_indicator_exists_result_decoded + S (eri_bit_row_indicator_exists_result) = S ((S (eri_column_row_indicator_exists_result)) * rc)) /\ exists ff_q_eri_row_indicator_exists_result_decoded. rb = ff_q_eri_row_indicator_exists_result_decoded * S ((S (eri_column_row_indicator_exists_result)) * rc) + (eri_bit_row_indicator_exists_result))) /\ (((eri_bit_row_indicator_exists_result = 0 /\ ((exists eri_gap_row_indicator_exists_result_choice_left. eri_gap_row_indicator_exists_result_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_result) /\ ~(exists eri_gap_row_indicator_exists_result_choice_right. eri_gap_row_indicator_exists_result_choice_right + S (p * S eri_column_row_indicator_exists_result) = q * S i))) \/ (eri_bit_row_indicator_exists_result = 1 /\ ((exists eri_gap_row_indicator_exists_result_choice_right. eri_gap_row_indicator_exists_result_choice_right + S (p * S eri_column_row_indicator_exists_result) = q * S i) /\ ~(exists eri_gap_row_indicator_exists_result_choice_left. eri_gap_row_indicator_exists_result_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_result))))))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA00DC eisenstein_row_indicator_prefix_extend

Direct theorem dependents

PA00DF distinct_odd_prime_half_row_count_exists

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

50 script commands · 12 reading checkpoints · 5 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 (5)
add eq zero rightsucc ne zerole succle refleisenstein row indicator prefix extend
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro i
02Induction on lL4–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro hchoices
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–9

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

  1. L8
    intro j
  2. L9
    intro hj
05Separate the logical casesL10–11

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

  1. L10
    exfalso
  2. L11
    cases hj
06Establish hsjL12–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L12
    have hsj : S j = 0
  2. L13
    specialize add_eq_zero_right x
  3. L14
    specialize add_eq_zero_right (S j)
  4. L15
    apply add_eq_zero_right
  5. L16
    exact hj_witness
  6. L17
    specialize succ_ne_zero j
  7. L18
    apply succ_ne_zero
  8. L19
    exact hsj
  9. L20
    intro hchoices
07Establish hprevious_choicesL21–29

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

  1. L21
    have hprevious_choices : ∀ eri_column_row_indicator_exists_previous_choices. Lt(eri_column_row_indicator_exists_previous_choices,l) → ∃ x. x = 0 ∧ (Lt(q · S i,p · S eri_column_row_indicator_exists_previous_choices) ∧ ¬Lt(p · S eri_column_row_indicator_exists_previous_choices,q · S i)) ∨ x = 1 ∧ (Lt(p · S eri_column_row_indicator_exists_previous_choices,q · S i) ∧ ¬Lt(q · S i,p · S eri_column_row_indicator_exists_previous_choices))Definitions: Lt(eri_column_row_indicator_exists_previous_choices,l)Lt(q · S i,p · S eri_column_row_indicator_exists_previous_choices)Lt(p · S eri_column_row_indicator_exists_previous_choices,q · S i)Original native command in the exact edition
  2. L22
    intro j
  3. L23
    intro hj
  4. L24
    specialize hchoices j
  5. L25
    apply hchoices
  6. L26
    specialize le_succ (S j)
  7. L27
    specialize le_succ l
  8. L28
    apply le_succ
  9. L29
    exact hj
08Establish hpreviousL30–32

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

  1. L30
    have hprevious : ∃ rb. ∃ rc. ∀ x. Lt(x,l) → ∃ 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)))Definitions: Lt(x,l)BetaAt(rb,rc,x,y)Lt(q · S i,p · S x)Lt(p · S x,q · S i)Original native command in the exact edition
  2. L31
    apply IH
  3. L32
    exact hprevious_choices
09Separate the logical casesL33–34

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

  1. L33
    cases hprevious
  2. L34
    cases hprevious_witness
10Establish hlastL35–39

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

  1. L35
    have hlast : ∃ bit. bit = 0 ∧ (Lt(q · S i,p · S l) ∧ ¬Lt(p · S l,q · S i)) ∨ bit = 1 ∧ (Lt(p · S l,q · S i) ∧ ¬Lt(q · S i,p · S l))Definitions: Lt(q · S i,p · S l)Lt(p · S l,q · S i)Original native command in the exact edition
  2. L36
    specialize hchoices l
  3. L37
    apply hchoices
  4. L38
    specialize le_refl (S l)
  5. L39
    exact le_refl
11Establish hnextL40–49

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

  1. L40
    have hnext : ∃ rb. ∃ rc. ∀ x. Lt(x,S l) → ∃ 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)))Definitions: Lt(x,S l)BetaAt(rb,rc,x,y)Lt(q · S i,p · S x)Lt(p · S x,q · S i)Original native command in the exact edition
  2. L41
    specialize eisenstein_row_indicator_prefix_extend p
  3. L42
    specialize eisenstein_row_indicator_prefix_extend q
  4. L43
    specialize eisenstein_row_indicator_prefix_extend i
  5. L44
    specialize eisenstein_row_indicator_prefix_extend x
  6. L45
    specialize eisenstein_row_indicator_prefix_extend x1
  7. L46
    specialize eisenstein_row_indicator_prefix_extend l
  8. L47
    apply eisenstein_row_indicator_prefix_extend
  9. L48
    exact hprevious_witness_witness
  10. L49
    exact hlast
12Use earlier factsL50–50

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

  1. L50
    exact hnext

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004induction l
  5. 0005intro hchoices
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro j
  9. 0009intro hj
  10. 0010exfalso
  11. 0011cases hj
  12. 0012have hsj : S j = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S j)
  15. 0015apply add_eq_zero_right
  16. 0016exact hj_witness
  17. 0017specialize succ_ne_zero j
  18. 0018apply succ_ne_zero
  19. 0019exact hsj
  20. 0020intro hchoices
  21. 0021have hprevious_choices : ∀ eri_column_row_indicator_exists_previous_choices. Lt(eri_column_row_indicator_exists_previous_choices,l) → ∃ x. x = 0 ∧ (Lt(q · S i,p · S eri_column_row_indicator_exists_previous_choices) ∧ ¬Lt(p · S eri_column_row_indicator_exists_previous_choices,q · S i)) ∨ x = 1 ∧ (Lt(p · S eri_column_row_indicator_exists_previous_choices,q · S i) ∧ ¬Lt(q · S i,p · S eri_column_row_indicator_exists_previous_choices))
    Exact native replay linehave hprevious_choices : forall eri_column_row_indicator_exists_previous_choices. (exists eri_gap_row_indicator_exists_previous_choices_bound. eri_gap_row_indicator_exists_previous_choices_bound + S (eri_column_row_indicator_exists_previous_choices) = l) -> exists eri_bit_row_indicator_exists_previous_choices. (((eri_bit_row_indicator_exists_previous_choices = 0 /\ ((exists eri_gap_row_indicator_exists_previous_choices_choice_left. eri_gap_row_indicator_exists_previous_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_previous_choices) /\ ~(exists eri_gap_row_indicator_exists_previous_choices_choice_right. eri_gap_row_indicator_exists_previous_choices_choice_right + S (p * S eri_column_row_indicator_exists_previous_choices) = q * S i))) \/ (eri_bit_row_indicator_exists_previous_choices = 1 /\ ((exists eri_gap_row_indicator_exists_previous_choices_choice_right. eri_gap_row_indicator_exists_previous_choices_choice_right + S (p * S eri_column_row_indicator_exists_previous_choices) = q * S i) /\ ~(exists eri_gap_row_indicator_exists_previous_choices_choice_left. eri_gap_row_indicator_exists_previous_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_previous_choices)))))
  22. 0022intro j
  23. 0023intro hj
  24. 0024specialize hchoices j
  25. 0025apply hchoices
  26. 0026specialize le_succ (S j)
  27. 0027specialize le_succ l
  28. 0028apply le_succ
  29. 0029exact hj
  30. 0030have hprevious : ∃ rb. ∃ rc. ∀ x. Lt(x,l) → ∃ 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)))
    Exact native replay linehave hprevious : exists rb rc. (forall eri_column_row_indicator_exists_previous_prefix. (exists eri_gap_row_indicator_exists_previous_prefix_bound. eri_gap_row_indicator_exists_previous_prefix_bound + S (eri_column_row_indicator_exists_previous_prefix) = l) -> exists eri_bit_row_indicator_exists_previous_prefix. ((((exists ff_h_eri_row_indicator_exists_previous_prefix_decoded. ff_h_eri_row_indicator_exists_previous_prefix_decoded + S (eri_bit_row_indicator_exists_previous_prefix) = S ((S (eri_column_row_indicator_exists_previous_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_exists_previous_prefix_decoded. rb = ff_q_eri_row_indicator_exists_previous_prefix_decoded * S ((S (eri_column_row_indicator_exists_previous_prefix)) * rc) + (eri_bit_row_indicator_exists_previous_prefix))) /\ (((eri_bit_row_indicator_exists_previous_prefix = 0 /\ ((exists eri_gap_row_indicator_exists_previous_prefix_choice_left. eri_gap_row_indicator_exists_previous_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_previous_prefix) /\ ~(exists eri_gap_row_indicator_exists_previous_prefix_choice_right. eri_gap_row_indicator_exists_previous_prefix_choice_right + S (p * S eri_column_row_indicator_exists_previous_prefix) = q * S i))) \/ (eri_bit_row_indicator_exists_previous_prefix = 1 /\ ((exists eri_gap_row_indicator_exists_previous_prefix_choice_right. eri_gap_row_indicator_exists_previous_prefix_choice_right + S (p * S eri_column_row_indicator_exists_previous_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_exists_previous_prefix_choice_left. eri_gap_row_indicator_exists_previous_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_previous_prefix)))))))
  31. 0031apply IH
  32. 0032exact hprevious_choices
  33. 0033cases hprevious
  34. 0034cases hprevious_witness
  35. 0035have hlast : ∃ bit. bit = 0 ∧ (Lt(q · S i,p · S l) ∧ ¬Lt(p · S l,q · S i)) ∨ bit = 1 ∧ (Lt(p · S l,q · S i) ∧ ¬Lt(q · S i,p · S l))
    Exact native replay linehave hlast : exists bit. (((bit = 0 /\ ((exists eri_gap_row_indicator_exists_last_choice_left. eri_gap_row_indicator_exists_last_choice_left + S (q * S i) = p * S l) /\ ~(exists eri_gap_row_indicator_exists_last_choice_right. eri_gap_row_indicator_exists_last_choice_right + S (p * S l) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_exists_last_choice_right. eri_gap_row_indicator_exists_last_choice_right + S (p * S l) = q * S i) /\ ~(exists eri_gap_row_indicator_exists_last_choice_left. eri_gap_row_indicator_exists_last_choice_left + S (q * S i) = p * S l)))))
  36. 0036specialize hchoices l
  37. 0037apply hchoices
  38. 0038specialize le_refl (S l)
  39. 0039exact le_refl
  40. 0040have hnext : ∃ rb. ∃ rc. ∀ x. Lt(x,S l) → ∃ 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)))
    Exact native replay linehave hnext : exists rb rc. (forall eri_column_row_indicator_exists_successor_prefix. (exists eri_gap_row_indicator_exists_successor_prefix_bound. eri_gap_row_indicator_exists_successor_prefix_bound + S (eri_column_row_indicator_exists_successor_prefix) = S l) -> exists eri_bit_row_indicator_exists_successor_prefix. ((((exists ff_h_eri_row_indicator_exists_successor_prefix_decoded. ff_h_eri_row_indicator_exists_successor_prefix_decoded + S (eri_bit_row_indicator_exists_successor_prefix) = S ((S (eri_column_row_indicator_exists_successor_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_exists_successor_prefix_decoded. rb = ff_q_eri_row_indicator_exists_successor_prefix_decoded * S ((S (eri_column_row_indicator_exists_successor_prefix)) * rc) + (eri_bit_row_indicator_exists_successor_prefix))) /\ (((eri_bit_row_indicator_exists_successor_prefix = 0 /\ ((exists eri_gap_row_indicator_exists_successor_prefix_choice_left. eri_gap_row_indicator_exists_successor_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_successor_prefix) /\ ~(exists eri_gap_row_indicator_exists_successor_prefix_choice_right. eri_gap_row_indicator_exists_successor_prefix_choice_right + S (p * S eri_column_row_indicator_exists_successor_prefix) = q * S i))) \/ (eri_bit_row_indicator_exists_successor_prefix = 1 /\ ((exists eri_gap_row_indicator_exists_successor_prefix_choice_right. eri_gap_row_indicator_exists_successor_prefix_choice_right + S (p * S eri_column_row_indicator_exists_successor_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_exists_successor_prefix_choice_left. eri_gap_row_indicator_exists_successor_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_exists_successor_prefix)))))))
  41. 0041specialize eisenstein_row_indicator_prefix_extend p
  42. 0042specialize eisenstein_row_indicator_prefix_extend q
  43. 0043specialize eisenstein_row_indicator_prefix_extend i
  44. 0044specialize eisenstein_row_indicator_prefix_extend x
  45. 0045specialize eisenstein_row_indicator_prefix_extend x1
  46. 0046specialize eisenstein_row_indicator_prefix_extend l
  47. 0047apply eisenstein_row_indicator_prefix_extend
  48. 0048exact hprevious_witness_witness
  49. 0049exact hlast
  50. 0050exact hnext