PQ001F

prime_field_polynomial_leading_zero_cut_exists

Finite induction scans actual decoded coefficients: either the entire prefix is zero or the first retained position has an actual nonzero value.

Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ L. ∃ t. ∃ M. L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0)))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 1BetaAt(b,c,i,x) · 3Repeat(b,c,a,l) · 3

Actual proof prerequisites

beta_repeat_empty · checked external prerequisitebeta_at_exists · checked external prerequisiteeq_decidable · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall b c L. exists t M. ((((L)=(t)+(M)) /\ (((forall pfp_repeat_index_cut_existszero. (exists pfa_gap_cut_existszeroindex. pfa_gap_cut_existszeroindex + S (pfp_repeat_index_cut_existszero) = (t)) -> (((exists ff_h_pfp_cut_existszeroentry. ff_h_pfp_cut_existszeroentry + S (0) = S ((S (pfp_repeat_index_cut_existszero)) * c)) /\ exists ff_q_pfp_cut_existszeroentry. b = ff_q_pfp_cut_existszeroentry * S ((S (pfp_repeat_index_cut_existszero)) * c) + (0)))) /\ (((M)=0 \/ (((~((M)=0)) /\ ((exists pftrim_leading_cut_existshead. ((((exists ff_h_pfp_cut_existsheadentry. ff_h_pfp_cut_existsheadentry + S (pftrim_leading_cut_existshead) = S ((S (t)) * c)) /\ exists ff_q_pfp_cut_existsheadentry. b = ff_q_pfp_cut_existsheadentry * S ((S (t)) * c) + (pftrim_leading_cut_existshead))) /\ ((~(pftrim_leading_cut_existshead=0))))))))))))))

Complete tactic proof in conservative notation

All 99 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

99 script commands · 52 reading checkpoints · 6 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–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on LL3–3

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

  1. L3
    induction L
03Construct an explicit witnessL4–5

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

  1. L4
    exists 0
  2. L5
    exists 0
04Separate the logical casesL6–6

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

  1. L6
    split
05Calculate and transport equalitiesL7–7

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

  1. L7
    simp
06Separate the logical casesL8–8

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

  1. L8
    split
07Use earlier factsL9–13

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

  1. L9
    specialize beta_repeat_empty (b)
  2. L10
    specialize beta_repeat_empty (c)
  3. L11
    specialize beta_repeat_empty (0)
  4. L12
    specialize beta_repeat_empty (0)
  5. L13
    apply beta_repeat_empty
08Calculate and transport equalitiesL14–14

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

  1. L14
    refl
09Separate the logical casesL15–15

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

  1. L15
    left
10Calculate and transport equalitiesL16–16

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

  1. L16
    refl
11Establish holdL17–18

Establish this local claim before using it. It is not an additional assumption.

  1. L17
    have hold : ∃ t. ∃ M. L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0)))Definitions: Repeat(b,c,0,t)BetaAt(b,c,t,x)Original native command in the exact edition
  2. L18
    exact IH
12Separate the logical casesL19–23

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

  1. L19
    cases hold
  2. L20
    cases hold_witness
  3. L21
    cases hold_witness_witness
  4. L22
    cases hold_witness_witness_right
  5. L23
    cases hold_witness_witness_right_right
13Establish hlenL24–28

Establish this local claim before using it. It is not an additional assumption.

  1. L24
    have hlen : L=x
  2. L25
    trans x+x1
  3. L26
    exact hold_witness_witness_left
  4. L27
    rewrite hold_witness_witness_right_right_left
  5. L28
    simp
14Establish hzeroL29–31

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hzero : Repeat(b,c,0,L)Definitions: Repeat(b,c,0,L)Original native command in the exact edition
  2. L30
    rewrite hlen
  3. L31
    exact hold_witness_witness_right_left
15Establish haL32–36

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

  1. L32
    have ha : ∃ a. BetaAt(b,c,L,a)Definitions: BetaAt(b,c,L,a)Original native command in the exact edition
  2. L33
    specialize beta_at_exists (b)
  3. L34
    specialize beta_at_exists (c)
  4. L35
    specialize beta_at_exists (L)
  5. L36
    apply beta_at_exists
16Separate the logical casesL37–37

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

  1. L37
    cases ha
17Establish hzL38–41

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

  1. L38
    have hz : x2=0 \/ ~(x2=0)
  2. L39
    specialize eq_decidable (x2)
  3. L40
    specialize eq_decidable (0)
  4. L41
    apply eq_decidable
18Separate the logical casesL42–42

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

  1. L42
    cases hz
19Construct an explicit witnessL43–44

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

  1. L43
    exists S L
  2. L44
    exists 0
20Separate the logical casesL45–45

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

  1. L45
    split
21Calculate and transport equalitiesL46–46

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

  1. L46
    simp
22Separate the logical casesL47–47

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

  1. L47
    split
23Fix variables and assumptionsL48–49

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

  1. L48
    intro i
  2. L49
    intro hi
24Establish hindexL50–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L50
    have hindex : i = L ∨ Lt(i,L)Definitions: Lt(i,L)Original native command in the exact edition
  2. L51
    specialize finite_lt_succ_eq_or_lt (L)
  3. L52
    specialize finite_lt_succ_eq_or_lt (i)
  4. L53
    apply finite_lt_succ_eq_or_lt
  5. L54
    exact hi
25Separate the logical casesL55–55

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

  1. L55
    cases hindex
26Calculate and transport equalitiesL56–59

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

  1. L56
    rewrite hindex_left
  2. L57
    rewrite hindex_left
  3. L58
    rewrite hz_left at ha_witness
  4. L59
    rewrite hz_left at ha_witness
27Use earlier factsL60–63

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

  1. L60
    exact ha_witness
  2. L61
    specialize hzero (i)
  3. L62
    apply hzero
  4. L63
    exact hindex_right
28Separate the logical casesL64–64

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

  1. L64
    left
29Calculate and transport equalitiesL65–65

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

  1. L65
    refl
30Construct an explicit witnessL66–67

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

  1. L66
    exists L
  2. L67
    exists 1
31Separate the logical casesL68–68

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

  1. L68
    split
32Calculate and transport equalitiesL69–69

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

  1. L69
    simp
33Separate the logical casesL70–70

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

  1. L70
    split
34Use earlier factsL71–71

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

  1. L71
    exact hzero
35Separate the logical casesL72–73

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

  1. L72
    right
  2. L73
    split
36Fix variables and assumptionsL74–74

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

  1. L74
    intro hbad
37Use earlier factsL75–77

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

  1. L75
    specialize succ_ne_zero (0)
  2. L76
    apply succ_ne_zero
  3. L77
    exact hbad
38Construct an explicit witnessL78–78

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

  1. L78
    exists x2
39Separate the logical casesL79–79

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

  1. L79
    split
40Use earlier factsL80–81

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

  1. L80
    exact ha_witness
  2. L81
    exact hz_right
41Separate the logical casesL82–82

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

  1. L82
    cases hold_witness_witness_right_right_right
42Construct an explicit witnessL83–84

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

  1. L83
    exists x
  2. L84
    exists S x1
43Separate the logical casesL85–85

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

  1. L85
    split
44Calculate and transport equalitiesL86–87

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

  1. L86
    trans S (x+x1)
  2. L87
    congr
45Use earlier factsL88–88

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

  1. L88
    exact hold_witness_witness_left
46Calculate and transport equalitiesL89–89

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

  1. L89
    symm
47Use earlier factsL90–90

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

  1. L90
    apply PA4
48Separate the logical casesL91–91

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

  1. L91
    split
49Use earlier factsL92–92

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

  1. L92
    exact hold_witness_witness_right_left
50Separate the logical casesL93–94

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

  1. L93
    right
  2. L94
    split
51Fix variables and assumptionsL95–95

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

  1. L95
    intro hbad
52Use earlier factsL96–99

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

  1. L96
    specialize succ_ne_zero (x1)
  2. L97
    apply succ_ne_zero
  3. L98
    exact hbad
  4. L99
    exact hold_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 99 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction L
  4. 0004exists 0
  5. 0005exists 0
  6. 0006split
  7. 0007simp
  8. 0008split
  9. 0009specialize beta_repeat_empty (b)
  10. 0010specialize beta_repeat_empty (c)
  11. 0011specialize beta_repeat_empty (0)
  12. 0012specialize beta_repeat_empty (0)
  13. 0013apply beta_repeat_empty
  14. 0014refl
  15. 0015left
  16. 0016refl
  17. 0017have hold : ∃ t. ∃ M. L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0)))
  18. 0018exact IH
  19. 0019cases hold
  20. 0020cases hold_witness
  21. 0021cases hold_witness_witness
  22. 0022cases hold_witness_witness_right
  23. 0023cases hold_witness_witness_right_right
  24. 0024have hlen : L=x
  25. 0025trans x+x1
  26. 0026exact hold_witness_witness_left
  27. 0027rewrite hold_witness_witness_right_right_left
  28. 0028simp
  29. 0029have hzero : Repeat(b,c,0,L)
  30. 0030rewrite hlen
  31. 0031exact hold_witness_witness_right_left
  32. 0032have ha : ∃ a. BetaAt(b,c,L,a)
  33. 0033specialize beta_at_exists (b)
  34. 0034specialize beta_at_exists (c)
  35. 0035specialize beta_at_exists (L)
  36. 0036apply beta_at_exists
  37. 0037cases ha
  38. 0038have hz : x2=0 \/ ~(x2=0)
  39. 0039specialize eq_decidable (x2)
  40. 0040specialize eq_decidable (0)
  41. 0041apply eq_decidable
  42. 0042cases hz
  43. 0043exists S L
  44. 0044exists 0
  45. 0045split
  46. 0046simp
  47. 0047split
  48. 0048intro i
  49. 0049intro hi
  50. 0050have hindex : i = L ∨ Lt(i,L)
  51. 0051specialize finite_lt_succ_eq_or_lt (L)
  52. 0052specialize finite_lt_succ_eq_or_lt (i)
  53. 0053apply finite_lt_succ_eq_or_lt
  54. 0054exact hi
  55. 0055cases hindex
  56. 0056rewrite hindex_left
  57. 0057rewrite hindex_left
  58. 0058rewrite hz_left at ha_witness
  59. 0059rewrite hz_left at ha_witness
  60. 0060exact ha_witness
  61. 0061specialize hzero (i)
  62. 0062apply hzero
  63. 0063exact hindex_right
  64. 0064left
  65. 0065refl
  66. 0066exists L
  67. 0067exists 1
  68. 0068split
  69. 0069simp
  70. 0070split
  71. 0071exact hzero
  72. 0072right
  73. 0073split
  74. 0074intro hbad
  75. 0075specialize succ_ne_zero (0)
  76. 0076apply succ_ne_zero
  77. 0077exact hbad
  78. 0078exists x2
  79. 0079split
  80. 0080exact ha_witness
  81. 0081exact hz_right
  82. 0082cases hold_witness_witness_right_right_right
  83. 0083exists x
  84. 0084exists S x1
  85. 0085split
  86. 0086trans S (x+x1)
  87. 0087congr
  88. 0088exact hold_witness_witness_left
  89. 0089symm
  90. 0090apply PA4
  91. 0091split
  92. 0092exact hold_witness_witness_right_left
  93. 0093right
  94. 0094split
  95. 0095intro hbad
  96. 0096specialize succ_ne_zero (x1)
  97. 0097apply succ_ne_zero
  98. 0098exact hbad
  99. 0099exact hold_witness_witness_right_right_right_right