PA00DT · theorem

eisenstein_row_indicator_prefix_to_initial_segment

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

A semantic row prefix is the exact initial segment cut out by its nonzero division quotient.

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

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

9 occurrences

Exact expanded native-PA statement
forall p q i d r rb rc k. (forall eri_column_row_quotient_source. (exists eri_gap_row_quotient_source_bound. eri_gap_row_quotient_source_bound + S (eri_column_row_quotient_source) = k) -> exists eri_bit_row_quotient_source. ((((exists ff_h_eri_row_quotient_source_decoded. ff_h_eri_row_quotient_source_decoded + S (eri_bit_row_quotient_source) = S ((S (eri_column_row_quotient_source)) * rc)) /\ exists ff_q_eri_row_quotient_source_decoded. rb = ff_q_eri_row_quotient_source_decoded * S ((S (eri_column_row_quotient_source)) * rc) + (eri_bit_row_quotient_source))) /\ (((eri_bit_row_quotient_source = 0 /\ ((exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source) /\ ~(exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i))) \/ (eri_bit_row_quotient_source = 1 /\ ((exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i) /\ ~(exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source))))))) -> q * S i = p * d + r -> ~(r = 0) -> (exists edt_lt_gap_row_quotient_remainder_bound. edt_lt_gap_row_quotient_remainder_bound + S (r) = p) -> (forall eis_index_row_quotient_initial. (exists eis_lt_gap_row_quotient_initial_bound. eis_lt_gap_row_quotient_initial_bound + S (eis_index_row_quotient_initial) = k) -> exists eis_bit_row_quotient_initial. ((((exists ff_h_eis_row_quotient_initial_decoded. ff_h_eis_row_quotient_initial_decoded + S (eis_bit_row_quotient_initial) = S ((S (eis_index_row_quotient_initial)) * rc)) /\ exists ff_q_eis_row_quotient_initial_decoded. rb = ff_q_eis_row_quotient_initial_decoded * S ((S (eis_index_row_quotient_initial)) * rc) + (eis_bit_row_quotient_initial))) /\ (((eis_bit_row_quotient_initial = 1 /\ (exists eis_le_gap_row_quotient_initial_choice_inside. eis_le_gap_row_quotient_initial_choice_inside + (S eis_index_row_quotient_initial) = d)) \/ (eis_bit_row_quotient_initial = 0 /\ (exists eis_lt_gap_row_quotient_initial_choice_outside. eis_lt_gap_row_quotient_initial_choice_outside + S (d) = S eis_index_row_quotient_initial))))))

Proof neighborhood

Direct theorem prerequisites

PA00DS nonzero_remainder_division_positive_multiple_threshold PA003B le_or_lt

Direct theorem dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

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

55 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 (2)
nonzero remainder division positive multiple thresholdle or lt
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 i
  4. L4
    intro d
  5. L5
    intro r
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro k
  9. L9
    intro hrow
  10. L10
    intro hdivision
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hr0
  2. L12
    intro hrp
  3. L13
    intro j
  4. L14
    intro hj
03Establish hstoredL15–18

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

  1. L15
    have hstored : ∃ bit. BetaAt(rb,rc,j,bit) ∧ (bit = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ bit = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)))Definitions: BetaAt(rb,rc,j,bit)Lt(q · S i,p · S j)Lt(p · S j,q · S i)Original native command in the exact edition
  2. L16
    specialize hrow j
  3. L17
    apply hrow
  4. L18
    exact hj
04Separate the logical casesL19–20

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

  1. L19
    cases hstored
  2. L20
    cases hstored_witness
05Construct an explicit witnessL21–21

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

  1. L21
    exists x
06Separate the logical casesL22–22

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

  1. L22
    split
07Use earlier factsL23–23

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

  1. L23
    exact hstored_witness_left
08Establish hthresholdL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nonzero remainder division positive multiple threshold.

  1. L24
    have hthreshold : (Lt(p · S j,q · S i) → Lt(j,d)) ∧ (Lt(j,d) → Lt(p · S j,q · S i))Definitions: Lt(p · S j,q · S i)Lt(j,d)Original native command in the exact edition
  2. L25
    specialize nonzero_remainder_division_positive_multiple_threshold p
  3. L26
    specialize nonzero_remainder_division_positive_multiple_threshold (q * S i)
  4. L27
    specialize nonzero_remainder_division_positive_multiple_threshold d
  5. L28
    specialize nonzero_remainder_division_positive_multiple_threshold r
  6. L29
    specialize nonzero_remainder_division_positive_multiple_threshold j
  7. L30
    apply nonzero_remainder_division_positive_multiple_threshold
  8. L31
    exact hdivision
  9. L32
    exact hr0
  10. L33
    exact hrp
09Separate the logical casesL34–39

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

  1. L34
    cases hthreshold
  2. L35
    cases hstored_witness_right
  3. L36
    cases hstored_witness_right_left
  4. L37
    cases hstored_witness_right_left_right
  5. L38
    right
  6. L39
    split
10Use earlier factsL40–42

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

  1. L40
    exact hstored_witness_right_left_left
  2. L41
    specialize le_or_lt (S j)
  3. L42
    specialize le_or_lt d
11Separate the logical casesL43–44

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

  1. L43
    cases le_or_lt
  2. L44
    exfalso
12Use earlier factsL45–48

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

  1. L45
    apply hstored_witness_right_left_right_right
  2. L46
    apply hthreshold_right
  3. L47
    exact le_or_lt_left
  4. L48
    exact le_or_lt_right
13Separate the logical casesL49–52

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

  1. L49
    cases hstored_witness_right_right
  2. L50
    cases hstored_witness_right_right_right
  3. L51
    left
  4. L52
    split
14Use earlier factsL53–55

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

  1. L53
    exact hstored_witness_right_right_left
  2. L54
    apply hthreshold_left
  3. L55
    exact hstored_witness_right_right_right_left

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004intro d
  5. 0005intro r
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro k
  9. 0009intro hrow
  10. 0010intro hdivision
  11. 0011intro hr0
  12. 0012intro hrp
  13. 0013intro j
  14. 0014intro hj
  15. 0015have hstored : ∃ bit. BetaAt(rb,rc,j,bit) ∧ (bit = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ bit = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)))
    Exact native replay linehave hstored : exists bit. ((((exists ff_h_row_quotient_stored. ff_h_row_quotient_stored + S (bit) = S ((S (j)) * rc)) /\ exists ff_q_row_quotient_stored. rb = ff_q_row_quotient_stored * S ((S (j)) * rc) + (bit))) /\ (((bit = 0 /\ ((exists eri_gap_row_quotient_stored_choice_left. eri_gap_row_quotient_stored_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_quotient_stored_choice_right. eri_gap_row_quotient_stored_choice_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_quotient_stored_choice_right. eri_gap_row_quotient_stored_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_quotient_stored_choice_left. eri_gap_row_quotient_stored_choice_left + S (q * S i) = p * S j))))))
  16. 0016specialize hrow j
  17. 0017apply hrow
  18. 0018exact hj
  19. 0019cases hstored
  20. 0020cases hstored_witness
  21. 0021exists x
  22. 0022split
  23. 0023exact hstored_witness_left
  24. 0024have hthreshold : (Lt(p · S j,q · S i) → Lt(j,d)) ∧ (Lt(j,d) → Lt(p · S j,q · S i))
    Exact native replay linehave hthreshold : (((exists edt_lt_gap_row_quotient_below. edt_lt_gap_row_quotient_below + S (p * S j) = q * S i) -> (exists edt_le_gap_row_quotient_bounded. edt_le_gap_row_quotient_bounded + (S j) = d)) /\ ((exists edt_le_gap_row_quotient_bounded. edt_le_gap_row_quotient_bounded + (S j) = d) -> (exists edt_lt_gap_row_quotient_below. edt_lt_gap_row_quotient_below + S (p * S j) = q * S i)))
  25. 0025specialize nonzero_remainder_division_positive_multiple_threshold p
  26. 0026specialize nonzero_remainder_division_positive_multiple_threshold (q * S i)
  27. 0027specialize nonzero_remainder_division_positive_multiple_threshold d
  28. 0028specialize nonzero_remainder_division_positive_multiple_threshold r
  29. 0029specialize nonzero_remainder_division_positive_multiple_threshold j
  30. 0030apply nonzero_remainder_division_positive_multiple_threshold
  31. 0031exact hdivision
  32. 0032exact hr0
  33. 0033exact hrp
  34. 0034cases hthreshold
  35. 0035cases hstored_witness_right
  36. 0036cases hstored_witness_right_left
  37. 0037cases hstored_witness_right_left_right
  38. 0038right
  39. 0039split
  40. 0040exact hstored_witness_right_left_left
  41. 0041specialize le_or_lt (S j)
  42. 0042specialize le_or_lt d
  43. 0043cases le_or_lt
  44. 0044exfalso
  45. 0045apply hstored_witness_right_left_right_right
  46. 0046apply hthreshold_right
  47. 0047exact le_or_lt_left
  48. 0048exact le_or_lt_right
  49. 0049cases hstored_witness_right_right
  50. 0050cases hstored_witness_right_right_right
  51. 0051left
  52. 0052split
  53. 0053exact hstored_witness_right_right_left
  54. 0054apply hthreshold_left
  55. 0055exact hstored_witness_right_right_right_left