PX0014

prime_field_polynomial_left_pad_exists

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

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ t. ∀ L. ∃ d. ∃ e. PolynomialLeftPad(b,c,L,t,d,e)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1PolynomialLeftPad(b,c,L,t,d,e) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2Repeat(b,c,a,l) · 1

Actual proof prerequisites

beta_repeat_exists · checked external prerequisitematrix_rank_no_index_below_zero · checked external prerequisitebeta_at_exists · checked external prerequisitebeta_prefix_extend · checked external prerequisitelt_of_lt_of_le · checked external prerequisitele_add_right · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisitematrix_recursive_lt_add_left · checked external prerequisite
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 100 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

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.

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–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 : ∃ d. ∃ e. Repeat(d,e,0,t)Definitions: Repeat(d,e,0,t)Original native command in the exact edition
  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(b,c,L,t,d,e)Original native command in the exact edition
  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 : ∃ a. BetaAt(b,c,L,a)Definitions: BetaAt(b,c,L,a)Original native command in the exact edition
  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: BetaAt(d,e,t + L,x2)BetaPrefixEqual(x,x1,d,e,t + L)Original native command in the exact edition
  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 ∨ Lt(i,L)Definitions: Lt(i,L)Original native command in the exact edition
  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 defined command ledger · 100 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004induction L
  5. 0005have hz : ∃ d. ∃ e. Repeat(d,e,0,t)
  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 : ∃ d. ∃ e. PolynomialLeftPad(b,c,L,t,d,e)
  24. 0024exact IH
  25. 0025cases hold
  26. 0026cases hold_witness
  27. 0027cases hold_witness_witness
  28. 0028have ha : ∃ a. BetaAt(b,c,L,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 : ∃ d. ∃ e. BetaAt(d,e,t + L,x2) ∧ BetaPrefixEqual(x,x1,d,e,t + L)
  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 ∨ Lt(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