PX0014

prime_field_polynomial_left_pad_exists

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

Finite induction genuinely constructs the zero block and appends every actual input coefficient, including empty input and arbitrary encodings.

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 t L. exists d e. (((forall pfp_repeat_index_left_pad_existszeros. (exists pfa_gap_left_pad_existszerosindex. pfa_gap_left_pad_existszerosindex + S (pfp_repeat_index_left_pad_existszeros) = (t)) -> (((exists ff_h_pfp_left_pad_existszerosentry. ff_h_pfp_left_pad_existszerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_existszeros)) * e)) /\ exists ff_q_pfp_left_pad_existszerosentry. d = ff_q_pfp_left_pad_existszerosentry * S ((S (pfp_repeat_index_left_pad_existszeros)) * e) + (0)))) /\ ((forall pfrep_index_left_pad_exists pfrep_value_left_pad_exists. (exists pfa_gap_left_pad_existsbound. pfa_gap_left_pad_existsbound + S (pfrep_index_left_pad_exists) = (L)) -> (((exists ff_h_pfp_left_pad_existsinput. ff_h_pfp_left_pad_existsinput + S (pfrep_value_left_pad_exists) = S ((S (pfrep_index_left_pad_exists)) * c)) /\ exists ff_q_pfp_left_pad_existsinput. b = ff_q_pfp_left_pad_existsinput * S ((S (pfrep_index_left_pad_exists)) * c) + (pfrep_value_left_pad_exists))) -> (((exists ff_h_pfp_left_pad_existsoutput. ff_h_pfp_left_pad_existsoutput + S (pfrep_value_left_pad_exists) = S ((S ((t)+pfrep_index_left_pad_exists)) * e)) /\ exists ff_q_pfp_left_pad_existsoutput. d = ff_q_pfp_left_pad_existsoutput * S ((S ((t)+pfrep_index_left_pad_exists)) * e) + (pfrep_value_left_pad_exists)))))))

Constructive proof overview

Generated structural guide

Finite induction genuinely constructs the zero block and appends every actual input coefficient, including empty input and arbitrary encodings.

The unchanged tactic script uses 9 declared prerequisites and contains 100 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_repeat_exists Alpha theorem; checked-use authorized matrix_rank_no_index_below_zero Alpha theorem; checked-use authorized beta_at_exists Alpha theorem; checked-use authorized beta_prefix_extend Alpha theorem; checked-use authorized lt_of_lt_of_le Alpha theorem; checked-use authorized le_add_right Alpha theorem; checked-use authorized finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized beta_at_unique Alpha theorem; checked-use authorized matrix_recursive_lt_add_left Alpha theorem; checked-use authorized

Direct dependents

PX0072 prime_field_polynomial_equivalent_implies_left_pad PX0073 prime_field_polynomial_add_left_pad_output PX0074 prime_field_polynomial_subtract_left_pad_output

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

100 script commands · 30 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–3

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro t
02Induction on LL4–4

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

  1. L4
    induction L
03Establish hzL5–8

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

  1. L5
    have hz : exists d e. (forall pfp_repeat_index_left_pad_empty_zeros. (exists pfa_gap_left_pad_empty_zerosindex. pfa_gap_left_pad_empty_zerosindex + S (pfp_repeat_index_left_pad_empty_zeros) = (t)) -> (((exists ff_h_pfp_left_pad_empty_zerosentry. ff_h_pfp_left_pad_empty_zerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_empty_zeros)) * e)) /\ exists ff_q_pfp_left_pad_empty_zerosentry. d = ff_q_pfp_left_pad_empty_zerosentry * S ((S (pfp_repeat_index_left_pad_empty_zeros)) * e) + (0))))
  2. L6
    specialize beta_repeat_exists (0)
  3. L7
    specialize beta_repeat_exists (t)
  4. L8
    apply beta_repeat_exists
04Separate the logical casesL9–10

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

  1. L9
    cases hz
  2. L10
    cases hz_witness
05Construct an explicit witnessL11–12

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

  1. L11
    exists x
  2. L12
    exists x1
06Separate the logical casesL13–13

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

  1. L13
    split
07Use earlier factsL14–14

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

  1. L14
    exact hz_witness_witness
08Fix variables and assumptionsL15–18

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

  1. L15
    intro i
  2. L16
    intro a
  3. L17
    intro hi
  4. L18
    intro ha
09Separate the logical casesL19–19

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

  1. L19
    exfalso
10Use earlier factsL20–22

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

  1. L20
    specialize matrix_rank_no_index_below_zero (i)
  2. L21
    apply matrix_rank_no_index_below_zero
  3. L22
    exact hi
11Establish holdL23–24

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

  1. L23
    have hold : ∃ d. ∃ e. PolynomialLeftPad(b,c,L,t,d,e)Definitions: PolynomialLeftPad
  2. L24
    exact IH
12Separate the logical casesL25–27

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

  1. L25
    cases hold
  2. L26
    cases hold_witness
  3. L27
    cases hold_witness_witness
13Establish haL28–32

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

  1. L28
    have ha : exists a. (((exists ff_h_pfp_left_pad_next_source. ff_h_pfp_left_pad_next_source + S (a) = S ((S (L)) * c)) /\ exists ff_q_pfp_left_pad_next_source. b = ff_q_pfp_left_pad_next_source * S ((S (L)) * c) + (a)))
  2. L29
    specialize beta_at_exists (b)
  3. L30
    specialize beta_at_exists (c)
  4. L31
    specialize beta_at_exists (L)
  5. L32
    apply beta_at_exists
14Separate the logical casesL33–33

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

  1. L33
    cases ha
15Establish hnL34–39

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

  1. L34
    have hn : ∃ d. ∃ e. BetaAt(d,e,t + L,x2) ∧ BetaPrefixEqual(x,x1,d,e,t + L)Definitions: BetaPrefixEqualBetaAt
  2. L35
    specialize beta_prefix_extend (t+L)
  3. L36
    specialize beta_prefix_extend (x)
  4. L37
    specialize beta_prefix_extend (x1)
  5. L38
    specialize beta_prefix_extend (x2)
  6. L39
    apply beta_prefix_extend
16Separate the logical casesL40–42

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

  1. L40
    cases hn
  2. L41
    cases hn_witness
  3. L42
    cases hn_witness_witness
17Construct an explicit witnessL43–44

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

  1. L43
    exists x3
  2. L44
    exists x4
18Separate the logical casesL45–45

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

  1. L45
    split
19Fix variables and assumptionsL46–47

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

  1. L46
    intro i
  2. L47
    intro hi
20Use earlier factsL48–57

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

  1. L48
    specialize hn_witness_witness_right (i)
  2. L49
    specialize hn_witness_witness_right (0)
  3. L50
    apply hn_witness_witness_right
  4. L51
    specialize lt_of_lt_of_le (i)
  5. L52
    specialize lt_of_lt_of_le (t)
  6. L53
    specialize lt_of_lt_of_le (t+L)
  7. L54
    apply lt_of_lt_of_le
  8. L55
    exact hi
  9. L56
    specialize le_add_right (t)
  10. L57
    specialize le_add_right (L)
21Use earlier factsL58–61

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

  1. L58
    apply le_add_right
  2. L59
    specialize hold_witness_witness_left (i)
  3. L60
    apply hold_witness_witness_left
  4. L61
    exact hi
22Fix variables and assumptionsL62–65

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

  1. L62
    intro i
  2. L63
    intro a
  3. L64
    intro hi
  4. L65
    intro ha0
23Establish hoL66–70

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. L66
    have ho : i=L \/ (exists pfa_gap_left_pad_old_index. pfa_gap_left_pad_old_index + S (i) = (L))
  2. L67
    specialize finite_lt_succ_eq_or_lt (L)
  3. L68
    specialize finite_lt_succ_eq_or_lt (i)
  4. L69
    apply finite_lt_succ_eq_or_lt
  5. L70
    exact hi
24Separate the logical casesL71–71

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

  1. L71
    cases ho
25Calculate and transport equalitiesL72–73

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

  1. L72
    rewrite ho_left
  2. L73
    rewrite ho_left
26Establish heqL74–83

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

  1. L74
    have heq : a=x2
  2. L75
    specialize beta_at_unique (b)
  3. L76
    specialize beta_at_unique (c)
  4. L77
    specialize beta_at_unique (L)
  5. L78
    specialize beta_at_unique (a)
  6. L79
    specialize beta_at_unique (x2)
  7. L80
    apply beta_at_unique
  8. L81
    rewrite ho_left at ha0
  9. L82
    rewrite ho_left at ha0
  10. L83
    exact ha0
27Use earlier factsL84–84

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

  1. L84
    exact ha_witness
28Calculate and transport equalitiesL85–86

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

  1. L85
    rewrite heq
  2. L86
    rewrite heq
29Use earlier factsL87–96

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

  1. L87
    exact hn_witness_witness_left
  2. L88
    specialize hn_witness_witness_right (t+i)
  3. L89
    specialize hn_witness_witness_right (a)
  4. L90
    apply hn_witness_witness_right
  5. L91
    specialize matrix_recursive_lt_add_left (i)
  6. L92
    specialize matrix_recursive_lt_add_left (L)
  7. L93
    specialize matrix_recursive_lt_add_left (t)
  8. L94
    apply matrix_recursive_lt_add_left
  9. L95
    exact ho_right
  10. L96
    specialize hold_witness_witness_right (i)
30Use earlier factsL97–100

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

  1. L97
    specialize hold_witness_witness_right (a)
  2. L98
    apply hold_witness_witness_right
  3. L99
    exact ho_right
  4. L100
    exact ha0

Library-wide reading audit

Original exact command ledger · 100 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004induction L
  5. 0005have hz : exists d e. (forall pfp_repeat_index_left_pad_empty_zeros. (exists pfa_gap_left_pad_empty_zerosindex. pfa_gap_left_pad_empty_zerosindex + S (pfp_repeat_index_left_pad_empty_zeros) = (t)) -> (((exists ff_h_pfp_left_pad_empty_zerosentry. ff_h_pfp_left_pad_empty_zerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_empty_zeros)) * e)) /\ exists ff_q_pfp_left_pad_empty_zerosentry. d = ff_q_pfp_left_pad_empty_zerosentry * S ((S (pfp_repeat_index_left_pad_empty_zeros)) * e) + (0))))
  6. 0006specialize beta_repeat_exists (0)
  7. 0007specialize beta_repeat_exists (t)
  8. 0008apply beta_repeat_exists
  9. 0009cases hz
  10. 0010cases hz_witness
  11. 0011exists x
  12. 0012exists x1
  13. 0013split
  14. 0014exact hz_witness_witness
  15. 0015intro i
  16. 0016intro a
  17. 0017intro hi
  18. 0018intro ha
  19. 0019exfalso
  20. 0020specialize matrix_rank_no_index_below_zero (i)
  21. 0021apply matrix_rank_no_index_below_zero
  22. 0022exact hi
  23. 0023have hold : exists d e. (((forall pfp_repeat_index_left_pad_previouszeros. (exists pfa_gap_left_pad_previouszerosindex. pfa_gap_left_pad_previouszerosindex + S (pfp_repeat_index_left_pad_previouszeros) = (t)) -> (((exists ff_h_pfp_left_pad_previouszerosentry. ff_h_pfp_left_pad_previouszerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_previouszeros)) * e)) /\ exists ff_q_pfp_left_pad_previouszerosentry. d = ff_q_pfp_left_pad_previouszerosentry * S ((S (pfp_repeat_index_left_pad_previouszeros)) * e) + (0)))) /\ ((forall pfrep_index_left_pad_previous pfrep_value_left_pad_previous. (exists pfa_gap_left_pad_previousbound. pfa_gap_left_pad_previousbound + S (pfrep_index_left_pad_previous) = (L)) -> (((exists ff_h_pfp_left_pad_previousinput. ff_h_pfp_left_pad_previousinput + S (pfrep_value_left_pad_previous) = S ((S (pfrep_index_left_pad_previous)) * c)) /\ exists ff_q_pfp_left_pad_previousinput. b = ff_q_pfp_left_pad_previousinput * S ((S (pfrep_index_left_pad_previous)) * c) + (pfrep_value_left_pad_previous))) -> (((exists ff_h_pfp_left_pad_previousoutput. ff_h_pfp_left_pad_previousoutput + S (pfrep_value_left_pad_previous) = S ((S ((t)+pfrep_index_left_pad_previous)) * e)) /\ exists ff_q_pfp_left_pad_previousoutput. d = ff_q_pfp_left_pad_previousoutput * S ((S ((t)+pfrep_index_left_pad_previous)) * e) + (pfrep_value_left_pad_previous)))))))
  24. 0024exact IH
  25. 0025cases hold
  26. 0026cases hold_witness
  27. 0027cases hold_witness_witness
  28. 0028have ha : exists a. (((exists ff_h_pfp_left_pad_next_source. ff_h_pfp_left_pad_next_source + S (a) = S ((S (L)) * c)) /\ exists ff_q_pfp_left_pad_next_source. b = ff_q_pfp_left_pad_next_source * S ((S (L)) * c) + (a)))
  29. 0029specialize beta_at_exists (b)
  30. 0030specialize beta_at_exists (c)
  31. 0031specialize beta_at_exists (L)
  32. 0032apply beta_at_exists
  33. 0033cases ha
  34. 0034have hn : exists d e. (((((exists ff_h_pfp_left_pad_next_entry. ff_h_pfp_left_pad_next_entry + S (x2) = S ((S (t+L)) * e)) /\ exists ff_q_pfp_left_pad_next_entry. d = ff_q_pfp_left_pad_next_entry * S ((S (t+L)) * e) + (x2))) /\ ((forall mdr_i_pfp_left_pad_preserved mdr_a_pfp_left_pad_preserved. (exists mdr_gap_pfp_left_pad_preservedb. mdr_gap_pfp_left_pad_preservedb + S (mdr_i_pfp_left_pad_preserved) = (t+L)) -> (((exists ff_h_mdr_pfp_left_pad_preservedo. ff_h_mdr_pfp_left_pad_preservedo + S (mdr_a_pfp_left_pad_preserved) = S ((S (mdr_i_pfp_left_pad_preserved)) * x1)) /\ exists ff_q_mdr_pfp_left_pad_preservedo. x = ff_q_mdr_pfp_left_pad_preservedo * S ((S (mdr_i_pfp_left_pad_preserved)) * x1) + (mdr_a_pfp_left_pad_preserved))) -> (((exists ff_h_mdr_pfp_left_pad_preservedn. ff_h_mdr_pfp_left_pad_preservedn + S (mdr_a_pfp_left_pad_preserved) = S ((S (mdr_i_pfp_left_pad_preserved)) * e)) /\ exists ff_q_mdr_pfp_left_pad_preservedn. d = ff_q_mdr_pfp_left_pad_preservedn * S ((S (mdr_i_pfp_left_pad_preserved)) * e) + (mdr_a_pfp_left_pad_preserved)))))))
  35. 0035specialize beta_prefix_extend (t+L)
  36. 0036specialize beta_prefix_extend (x)
  37. 0037specialize beta_prefix_extend (x1)
  38. 0038specialize beta_prefix_extend (x2)
  39. 0039apply beta_prefix_extend
  40. 0040cases hn
  41. 0041cases hn_witness
  42. 0042cases hn_witness_witness
  43. 0043exists x3
  44. 0044exists x4
  45. 0045split
  46. 0046intro i
  47. 0047intro hi
  48. 0048specialize hn_witness_witness_right (i)
  49. 0049specialize hn_witness_witness_right (0)
  50. 0050apply hn_witness_witness_right
  51. 0051specialize lt_of_lt_of_le (i)
  52. 0052specialize lt_of_lt_of_le (t)
  53. 0053specialize lt_of_lt_of_le (t+L)
  54. 0054apply lt_of_lt_of_le
  55. 0055exact hi
  56. 0056specialize le_add_right (t)
  57. 0057specialize le_add_right (L)
  58. 0058apply le_add_right
  59. 0059specialize hold_witness_witness_left (i)
  60. 0060apply hold_witness_witness_left
  61. 0061exact hi
  62. 0062intro i
  63. 0063intro a
  64. 0064intro hi
  65. 0065intro ha0
  66. 0066have ho : i=L \/ (exists pfa_gap_left_pad_old_index. pfa_gap_left_pad_old_index + S (i) = (L))
  67. 0067specialize finite_lt_succ_eq_or_lt (L)
  68. 0068specialize finite_lt_succ_eq_or_lt (i)
  69. 0069apply finite_lt_succ_eq_or_lt
  70. 0070exact hi
  71. 0071cases ho
  72. 0072rewrite ho_left
  73. 0073rewrite ho_left
  74. 0074have heq : a=x2
  75. 0075specialize beta_at_unique (b)
  76. 0076specialize beta_at_unique (c)
  77. 0077specialize beta_at_unique (L)
  78. 0078specialize beta_at_unique (a)
  79. 0079specialize beta_at_unique (x2)
  80. 0080apply beta_at_unique
  81. 0081rewrite ho_left at ha0
  82. 0082rewrite ho_left at ha0
  83. 0083exact ha0
  84. 0084exact ha_witness
  85. 0085rewrite heq
  86. 0086rewrite heq
  87. 0087exact hn_witness_witness_left
  88. 0088specialize hn_witness_witness_right (t+i)
  89. 0089specialize hn_witness_witness_right (a)
  90. 0090apply hn_witness_witness_right
  91. 0091specialize matrix_recursive_lt_add_left (i)
  92. 0092specialize matrix_recursive_lt_add_left (L)
  93. 0093specialize matrix_recursive_lt_add_left (t)
  94. 0094apply matrix_recursive_lt_add_left
  95. 0095exact ho_right
  96. 0096specialize hold_witness_witness_right (i)
  97. 0097specialize hold_witness_witness_right (a)
  98. 0098apply hold_witness_witness_right
  99. 0099exact ho_right
  100. 0100exact ha0