PG001A

prime_field_polynomial_append_shift_constant_add

Every actual appended prefix is the actual aligned sum of a genuine trailing-zero shift and the leading-padded singleton constant; the last and earlier entries are proved separately, including M=0.

Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ bb. ∀ bc. ∀ M. ∀ c. ∀ db. ∀ dc. ∀ sb. ∀ sc. ∀ kb. ∀ kc. ∀ tb. ∀ tc. Prime(p) → BetaPrefixInto(bb,bc,M,p) → Lt(c,p) → BetaPrefixEqual(bb,bc,db,dc,M) → BetaAt(db,dc,M,c) → PolynomialShift(bb,bc,M,sb,sc) → BetaAt(kb,kc,0,c) → PolynomialLeftPad(kb,kc,1,M,tb,tc) → FpPolyAdd(p,sb,sc,tb,tc,db,dc,S M)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1BetaPrefixEqual(b,c,d,e,l) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 1PolynomialLeftPad(b,c,L,t,d,e) · 1PolynomialShift(b,c,L,d,e) · 1Lt(a,b) · 3Prime(p) · 1BetaAt(b,c,i,x) · 5

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisiteprime_field_add_zero_left · checked external prerequisiteprime_field_add_zero_right · checked external prerequisite
Original expanded first-order statement 
forall p bb bc M c db dc sb sc kb kc tb tc. (~((p) = 1) /\ forall pfa_factor_left_append_sum_prime pfa_factor_right_append_sum_prime. (p) = pfa_factor_left_append_sum_prime * pfa_factor_right_append_sum_prime -> pfa_factor_left_append_sum_prime = 1 \/ pfa_factor_right_append_sum_prime = 1) -> (forall fom_index_pfp_append_sum_old_coefficients. (exists fom_gap_pfp_append_sum_old_coefficients_index_bound. fom_gap_pfp_append_sum_old_coefficients_index_bound + S (fom_index_pfp_append_sum_old_coefficients) = M) -> exists fom_value_pfp_append_sum_old_coefficients. ((((exists fom_beta_height_pfp_append_sum_old_coefficients_entry. fom_beta_height_pfp_append_sum_old_coefficients_entry + S (fom_value_pfp_append_sum_old_coefficients) = S ((S (fom_index_pfp_append_sum_old_coefficients)) * bc)) /\ exists fom_beta_quotient_pfp_append_sum_old_coefficients_entry. bb = fom_beta_quotient_pfp_append_sum_old_coefficients_entry * S ((S (fom_index_pfp_append_sum_old_coefficients)) * bc) + (fom_value_pfp_append_sum_old_coefficients))) /\ (exists fom_gap_pfp_append_sum_old_coefficients_value_bound. fom_gap_pfp_append_sum_old_coefficients_value_bound + S (fom_value_pfp_append_sum_old_coefficients) = p))) -> (exists pfa_gap_append_sum_scalar. pfa_gap_append_sum_scalar + S (c) = (p)) -> (forall mdr_i_pfp_append_sum_preserve mdr_a_pfp_append_sum_preserve. (exists mdr_gap_pfp_append_sum_preserveb. mdr_gap_pfp_append_sum_preserveb + S (mdr_i_pfp_append_sum_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_sum_preserveo. ff_h_mdr_pfp_append_sum_preserveo + S (mdr_a_pfp_append_sum_preserve) = S ((S (mdr_i_pfp_append_sum_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_sum_preserveo. bb = ff_q_mdr_pfp_append_sum_preserveo * S ((S (mdr_i_pfp_append_sum_preserve)) * bc) + (mdr_a_pfp_append_sum_preserve))) -> (((exists ff_h_mdr_pfp_append_sum_preserven. ff_h_mdr_pfp_append_sum_preserven + S (mdr_a_pfp_append_sum_preserve) = S ((S (mdr_i_pfp_append_sum_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_sum_preserven. db = ff_q_mdr_pfp_append_sum_preserven * S ((S (mdr_i_pfp_append_sum_preserve)) * dc) + (mdr_a_pfp_append_sum_preserve)))) -> (((exists ff_h_pfp_append_sum_actual_last. ff_h_pfp_append_sum_actual_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_sum_actual_last. db = ff_q_pfp_append_sum_actual_last * S ((S (M)) * dc) + (c))) -> (((forall mdr_i_pfp_append_sum_shiftprefix mdr_a_pfp_append_sum_shiftprefix. (exists mdr_gap_pfp_append_sum_shiftprefixb. mdr_gap_pfp_append_sum_shiftprefixb + S (mdr_i_pfp_append_sum_shiftprefix) = (M)) -> (((exists ff_h_mdr_pfp_append_sum_shiftprefixo. ff_h_mdr_pfp_append_sum_shiftprefixo + S (mdr_a_pfp_append_sum_shiftprefix) = S ((S (mdr_i_pfp_append_sum_shiftprefix)) * bc)) /\ exists ff_q_mdr_pfp_append_sum_shiftprefixo. bb = ff_q_mdr_pfp_append_sum_shiftprefixo * S ((S (mdr_i_pfp_append_sum_shiftprefix)) * bc) + (mdr_a_pfp_append_sum_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_sum_shiftprefixn. ff_h_mdr_pfp_append_sum_shiftprefixn + S (mdr_a_pfp_append_sum_shiftprefix) = S ((S (mdr_i_pfp_append_sum_shiftprefix)) * sc)) /\ exists ff_q_mdr_pfp_append_sum_shiftprefixn. sb = ff_q_mdr_pfp_append_sum_shiftprefixn * S ((S (mdr_i_pfp_append_sum_shiftprefix)) * sc) + (mdr_a_pfp_append_sum_shiftprefix)))) /\ ((((exists ff_h_pfp_append_sum_shiftlast. ff_h_pfp_append_sum_shiftlast + S (0) = S ((S (M)) * sc)) /\ exists ff_q_pfp_append_sum_shiftlast. sb = ff_q_pfp_append_sum_shiftlast * S ((S (M)) * sc) + (0)))))) -> (((exists ff_h_pfp_append_sum_singleton. ff_h_pfp_append_sum_singleton + S (c) = S ((S (0)) * kc)) /\ exists ff_q_pfp_append_sum_singleton. kb = ff_q_pfp_append_sum_singleton * S ((S (0)) * kc) + (c))) -> (((forall pfp_repeat_index_append_sum_left_padzeros. (exists pfa_gap_append_sum_left_padzerosindex. pfa_gap_append_sum_left_padzerosindex + S (pfp_repeat_index_append_sum_left_padzeros) = (M)) -> (((exists ff_h_pfp_append_sum_left_padzerosentry. ff_h_pfp_append_sum_left_padzerosentry + S (0) = S ((S (pfp_repeat_index_append_sum_left_padzeros)) * tc)) /\ exists ff_q_pfp_append_sum_left_padzerosentry. tb = ff_q_pfp_append_sum_left_padzerosentry * S ((S (pfp_repeat_index_append_sum_left_padzeros)) * tc) + (0)))) /\ ((forall pfrep_index_append_sum_left_pad pfrep_value_append_sum_left_pad. (exists pfa_gap_append_sum_left_padbound. pfa_gap_append_sum_left_padbound + S (pfrep_index_append_sum_left_pad) = (1)) -> (((exists ff_h_pfp_append_sum_left_padinput. ff_h_pfp_append_sum_left_padinput + S (pfrep_value_append_sum_left_pad) = S ((S (pfrep_index_append_sum_left_pad)) * kc)) /\ exists ff_q_pfp_append_sum_left_padinput. kb = ff_q_pfp_append_sum_left_padinput * S ((S (pfrep_index_append_sum_left_pad)) * kc) + (pfrep_value_append_sum_left_pad))) -> (((exists ff_h_pfp_append_sum_left_padoutput. ff_h_pfp_append_sum_left_padoutput + S (pfrep_value_append_sum_left_pad) = S ((S ((M)+pfrep_index_append_sum_left_pad)) * tc)) /\ exists ff_q_pfp_append_sum_left_padoutput. tb = ff_q_pfp_append_sum_left_padoutput * S ((S ((M)+pfrep_index_append_sum_left_pad)) * tc) + (pfrep_value_append_sum_left_pad))))))) -> (forall pfp_index_append_sum_result. (exists pfa_gap_append_sum_resultindex. pfa_gap_append_sum_resultindex + S (pfp_index_append_sum_result) = (S M)) -> exists pfp_left_append_sum_result pfp_right_append_sum_result pfp_value_append_sum_result. ((((exists ff_h_pfp_append_sum_resultleft. ff_h_pfp_append_sum_resultleft + S (pfp_left_append_sum_result) = S ((S (pfp_index_append_sum_result)) * sc)) /\ exists ff_q_pfp_append_sum_resultleft. sb = ff_q_pfp_append_sum_resultleft * S ((S (pfp_index_append_sum_result)) * sc) + (pfp_left_append_sum_result))) /\ (((((exists ff_h_pfp_append_sum_resultright. ff_h_pfp_append_sum_resultright + S (pfp_right_append_sum_result) = S ((S (pfp_index_append_sum_result)) * tc)) /\ exists ff_q_pfp_append_sum_resultright. tb = ff_q_pfp_append_sum_resultright * S ((S (pfp_index_append_sum_result)) * tc) + (pfp_right_append_sum_result))) /\ (((((exists ff_h_pfp_append_sum_resulttarget. ff_h_pfp_append_sum_resulttarget + S (pfp_value_append_sum_result) = S ((S (pfp_index_append_sum_result)) * dc)) /\ exists ff_q_pfp_append_sum_resulttarget. db = ff_q_pfp_append_sum_resulttarget * S ((S (pfp_index_append_sum_result)) * dc) + (pfp_value_append_sum_result))) /\ ((((exists pfa_gap_append_sum_resultoperationleft. pfa_gap_append_sum_resultoperationleft + S (pfp_left_append_sum_result) = (p)) /\ (((exists pfa_gap_append_sum_resultoperationright. pfa_gap_append_sum_resultoperationright + S (pfp_right_append_sum_result) = (p)) /\ ((((exists pfa_gap_append_sum_resultoperationresultbound. pfa_gap_append_sum_resultoperationresultbound + S (pfp_value_append_sum_result) = (p)) /\ ((exists pfa_offset_left_append_sum_resultoperationresultcongruence pfa_offset_right_append_sum_resultoperationresultcongruence. ((pfp_left_append_sum_result) + (pfp_right_append_sum_result)) + (p) * pfa_offset_left_append_sum_resultoperationresultcongruence = (pfp_value_append_sum_result) + (p) * pfa_offset_right_append_sum_resultoperationresultcongruence))))))))))))))))

Complete tactic proof in conservative notation

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

94 script commands · 31 reading checkpoints · 5 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–10

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

  1. L1
    intro p
  2. L2
    intro bb
  3. L3
    intro bc
  4. L4
    intro M
  5. L5
    intro c
  6. L6
    intro db
  7. L7
    intro dc
  8. L8
    intro sb
  9. L9
    intro sc
  10. L10
    intro kb
02Fix variables and assumptionsL11–20

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

  1. L11
    intro kc
  2. L12
    intro tb
  3. L13
    intro tc
  4. L14
    intro hp
  5. L15
    intro hb
  6. L16
    intro hc
  7. L17
    intro he
  8. L18
    intro hlast
  9. L19
    intro hs
  10. L20
    intro hk
03Fix variables and assumptionsL21–21

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

  1. L21
    intro ht
04Separate the logical casesL22–23

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

  1. L22
    cases hs
  2. L23
    cases ht
05Establish hconstantL24–24

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

  1. L24
    have hconstant : BetaAt(tb,tc,M,c)Definitions: BetaAt(tb,tc,M,c)Original native command in the exact edition
06Establish hrawL25–28

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

  1. L25
    have hraw : BetaAt(tb,tc,M + 0,c)Definitions: BetaAt(tb,tc,M + 0,c)Original native command in the exact edition
  2. L26
    specialize ht_right (0)
  3. L27
    specialize ht_right (c)
  4. L28
    apply ht_right
07Construct an explicit witnessL29–29

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

  1. L29
    exists 0
08Calculate and transport equalitiesL30–30

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

  1. L30
    simp
09Use earlier factsL31–31

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

  1. L31
    exact hk
10Establish hindexL32–38

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

  1. L32
    have hindex : M+0=M
  2. L33
    simp
  3. L34
    rewrite hindex at hraw
  4. L35
    rewrite hindex at hraw
  5. L36
    exact hraw
  6. L37
    intro i
  7. L38
    intro hi
11Establish hcaseL39–43

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. L39
    have hcase : i = M ∨ Lt(i,M)Definitions: Lt(i,M)Original native command in the exact edition
  2. L40
    specialize finite_lt_succ_eq_or_lt (M)
  3. L41
    specialize finite_lt_succ_eq_or_lt (i)
  4. L42
    apply finite_lt_succ_eq_or_lt
  5. L43
    exact hi
12Separate the logical casesL44–44

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

  1. L44
    cases hcase
13Construct an explicit witnessL45–47

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

  1. L45
    exists 0
  2. L46
    exists c
  3. L47
    exists c
14Separate the logical casesL48–48

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

  1. L48
    split
15Calculate and transport equalitiesL49–50

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

  1. L49
    rewrite hcase_left
  2. L50
    rewrite hcase_left
16Use earlier factsL51–51

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

  1. L51
    exact hs_right
17Separate the logical casesL52–52

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

  1. L52
    split
18Calculate and transport equalitiesL53–54

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

  1. L53
    rewrite hcase_left
  2. L54
    rewrite hcase_left
19Use earlier factsL55–55

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

  1. L55
    exact hconstant
20Separate the logical casesL56–56

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

  1. L56
    split
21Calculate and transport equalitiesL57–58

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

  1. L57
    rewrite hcase_left
  2. L58
    rewrite hcase_left
22Use earlier factsL59–64

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

  1. L59
    exact hlast
  2. L60
    specialize prime_field_add_zero_left (p)
  3. L61
    specialize prime_field_add_zero_left (c)
  4. L62
    apply prime_field_add_zero_left
  5. L63
    exact hp
  6. L64
    exact hc
23Establish haL65–68

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

  1. L65
    have ha : ∃ a. BetaAt(bb,bc,i,a) ∧ Lt(a,p)Definitions: BetaAt(bb,bc,i,a)Lt(a,p)Original native command in the exact edition
  2. L66
    specialize hb (i)
  3. L67
    apply hb
  4. L68
    exact hcase_right
24Separate the logical casesL69–70

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

  1. L69
    cases ha
  2. L70
    cases ha_witness
25Construct an explicit witnessL71–73

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

  1. L71
    exists x
  2. L72
    exists 0
  3. L73
    exists x
26Separate the logical casesL74–74

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

  1. L74
    split
27Use earlier factsL75–79

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

  1. L75
    specialize hs_left (i)
  2. L76
    specialize hs_left (x)
  3. L77
    apply hs_left
  4. L78
    exact hcase_right
  5. L79
    exact ha_witness_left
28Separate the logical casesL80–80

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

  1. L80
    split
29Use earlier factsL81–83

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

  1. L81
    specialize ht_left (i)
  2. L82
    apply ht_left
  3. L83
    exact hcase_right
30Separate the logical casesL84–84

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

  1. L84
    split
31Use earlier factsL85–94

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

  1. L85
    specialize he (i)
  2. L86
    specialize he (x)
  3. L87
    apply he
  4. L88
    exact hcase_right
  5. L89
    exact ha_witness_left
  6. L90
    specialize prime_field_add_zero_right (p)
  7. L91
    specialize prime_field_add_zero_right (x)
  8. L92
    apply prime_field_add_zero_right
  9. L93
    exact hp
  10. L94
    exact ha_witness_right

Library-wide reading audit

Original defined command ledger · 94 lines
  1. 0001intro p
  2. 0002intro bb
  3. 0003intro bc
  4. 0004intro M
  5. 0005intro c
  6. 0006intro db
  7. 0007intro dc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro kb
  11. 0011intro kc
  12. 0012intro tb
  13. 0013intro tc
  14. 0014intro hp
  15. 0015intro hb
  16. 0016intro hc
  17. 0017intro he
  18. 0018intro hlast
  19. 0019intro hs
  20. 0020intro hk
  21. 0021intro ht
  22. 0022cases hs
  23. 0023cases ht
  24. 0024have hconstant : BetaAt(tb,tc,M,c)
  25. 0025have hraw : BetaAt(tb,tc,M + 0,c)
  26. 0026specialize ht_right (0)
  27. 0027specialize ht_right (c)
  28. 0028apply ht_right
  29. 0029exists 0
  30. 0030simp
  31. 0031exact hk
  32. 0032have hindex : M+0=M
  33. 0033simp
  34. 0034rewrite hindex at hraw
  35. 0035rewrite hindex at hraw
  36. 0036exact hraw
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hcase : i = M ∨ Lt(i,M)
  40. 0040specialize finite_lt_succ_eq_or_lt (M)
  41. 0041specialize finite_lt_succ_eq_or_lt (i)
  42. 0042apply finite_lt_succ_eq_or_lt
  43. 0043exact hi
  44. 0044cases hcase
  45. 0045exists 0
  46. 0046exists c
  47. 0047exists c
  48. 0048split
  49. 0049rewrite hcase_left
  50. 0050rewrite hcase_left
  51. 0051exact hs_right
  52. 0052split
  53. 0053rewrite hcase_left
  54. 0054rewrite hcase_left
  55. 0055exact hconstant
  56. 0056split
  57. 0057rewrite hcase_left
  58. 0058rewrite hcase_left
  59. 0059exact hlast
  60. 0060specialize prime_field_add_zero_left (p)
  61. 0061specialize prime_field_add_zero_left (c)
  62. 0062apply prime_field_add_zero_left
  63. 0063exact hp
  64. 0064exact hc
  65. 0065have ha : ∃ a. BetaAt(bb,bc,i,a) ∧ Lt(a,p)
  66. 0066specialize hb (i)
  67. 0067apply hb
  68. 0068exact hcase_right
  69. 0069cases ha
  70. 0070cases ha_witness
  71. 0071exists x
  72. 0072exists 0
  73. 0073exists x
  74. 0074split
  75. 0075specialize hs_left (i)
  76. 0076specialize hs_left (x)
  77. 0077apply hs_left
  78. 0078exact hcase_right
  79. 0079exact ha_witness_left
  80. 0080split
  81. 0081specialize ht_left (i)
  82. 0082apply ht_left
  83. 0083exact hcase_right
  84. 0084split
  85. 0085specialize he (i)
  86. 0086specialize he (x)
  87. 0087apply he
  88. 0088exact hcase_right
  89. 0089exact ha_witness_left
  90. 0090specialize prime_field_add_zero_right (p)
  91. 0091specialize prime_field_add_zero_right (x)
  92. 0092apply prime_field_add_zero_right
  93. 0093exact hp
  94. 0094exact ha_witness_right