PQ001F

prime_field_polynomial_leading_zero_cut_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 expanded first-order arithmetic 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))))))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 99 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_repeat_empty Stable theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized eq_decidable Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

PQ0021 prime_field_polynomial_trim_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: BetaAtRepeat
  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 : forall pfp_repeat_index_cut_zero_old. (exists pfa_gap_cut_zero_oldindex. pfa_gap_cut_zero_oldindex + S (pfp_repeat_index_cut_zero_old) = (L)) -> (((exists ff_h_pfp_cut_zero_oldentry. ff_h_pfp_cut_zero_oldentry + S (0) = S ((S (pfp_repeat_index_cut_zero_old)) * c)) /\ exists ff_q_pfp_cut_zero_oldentry. b = ff_q_pfp_cut_zero_oldentry * S ((S (pfp_repeat_index_cut_zero_old)) * c) + (0)))
  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 : exists a. (((exists ff_h_pfp_cut_last. ff_h_pfp_cut_last + S (a) = S ((S (L)) * c)) /\ exists ff_q_pfp_cut_last. b = ff_q_pfp_cut_last * S ((S (L)) * c) + (a)))
  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 \/ (exists pfa_gap_cut_old_index. pfa_gap_cut_old_index + S (i) = (L))
  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 exact 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 : exists t M. ((((L)=(t)+(M)) /\ (((forall pfp_repeat_index_cut_previouszero. (exists pfa_gap_cut_previouszeroindex. pfa_gap_cut_previouszeroindex + S (pfp_repeat_index_cut_previouszero) = (t)) -> (((exists ff_h_pfp_cut_previouszeroentry. ff_h_pfp_cut_previouszeroentry + S (0) = S ((S (pfp_repeat_index_cut_previouszero)) * c)) /\ exists ff_q_pfp_cut_previouszeroentry. b = ff_q_pfp_cut_previouszeroentry * S ((S (pfp_repeat_index_cut_previouszero)) * c) + (0)))) /\ (((M)=0 \/ (((~((M)=0)) /\ ((exists pftrim_leading_cut_previoushead. ((((exists ff_h_pfp_cut_previousheadentry. ff_h_pfp_cut_previousheadentry + S (pftrim_leading_cut_previoushead) = S ((S (t)) * c)) /\ exists ff_q_pfp_cut_previousheadentry. b = ff_q_pfp_cut_previousheadentry * S ((S (t)) * c) + (pftrim_leading_cut_previoushead))) /\ ((~(pftrim_leading_cut_previoushead=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 : forall pfp_repeat_index_cut_zero_old. (exists pfa_gap_cut_zero_oldindex. pfa_gap_cut_zero_oldindex + S (pfp_repeat_index_cut_zero_old) = (L)) -> (((exists ff_h_pfp_cut_zero_oldentry. ff_h_pfp_cut_zero_oldentry + S (0) = S ((S (pfp_repeat_index_cut_zero_old)) * c)) /\ exists ff_q_pfp_cut_zero_oldentry. b = ff_q_pfp_cut_zero_oldentry * S ((S (pfp_repeat_index_cut_zero_old)) * c) + (0)))
  30. 0030rewrite hlen
  31. 0031exact hold_witness_witness_right_left
  32. 0032have ha : exists a. (((exists ff_h_pfp_cut_last. ff_h_pfp_cut_last + S (a) = S ((S (L)) * c)) /\ exists ff_q_pfp_cut_last. b = ff_q_pfp_cut_last * S ((S (L)) * c) + (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 \/ (exists pfa_gap_cut_old_index. pfa_gap_cut_old_index + S (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