PX0041

polynomial_zero_extended_add_congruent

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

An actual coefficient sum extends by actual zeros to an additive congruence at every index; no claim is made about arbitrary decoded entries outside the original prefixes.

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 p ab ac bb bc cb cc L i a b r. (forall pfp_index_padded_add_source. (exists pfa_gap_padded_add_sourceindex. pfa_gap_padded_add_sourceindex + S (pfp_index_padded_add_source) = (L)) -> exists pfp_left_padded_add_source pfp_right_padded_add_source pfp_value_padded_add_source. ((((exists ff_h_pfp_padded_add_sourceleft. ff_h_pfp_padded_add_sourceleft + S (pfp_left_padded_add_source) = S ((S (pfp_index_padded_add_source)) * ac)) /\ exists ff_q_pfp_padded_add_sourceleft. ab = ff_q_pfp_padded_add_sourceleft * S ((S (pfp_index_padded_add_source)) * ac) + (pfp_left_padded_add_source))) /\ (((((exists ff_h_pfp_padded_add_sourceright. ff_h_pfp_padded_add_sourceright + S (pfp_right_padded_add_source) = S ((S (pfp_index_padded_add_source)) * bc)) /\ exists ff_q_pfp_padded_add_sourceright. bb = ff_q_pfp_padded_add_sourceright * S ((S (pfp_index_padded_add_source)) * bc) + (pfp_right_padded_add_source))) /\ (((((exists ff_h_pfp_padded_add_sourcetarget. ff_h_pfp_padded_add_sourcetarget + S (pfp_value_padded_add_source) = S ((S (pfp_index_padded_add_source)) * cc)) /\ exists ff_q_pfp_padded_add_sourcetarget. cb = ff_q_pfp_padded_add_sourcetarget * S ((S (pfp_index_padded_add_source)) * cc) + (pfp_value_padded_add_source))) /\ ((((exists pfa_gap_padded_add_sourceoperationleft. pfa_gap_padded_add_sourceoperationleft + S (pfp_left_padded_add_source) = (p)) /\ (((exists pfa_gap_padded_add_sourceoperationright. pfa_gap_padded_add_sourceoperationright + S (pfp_right_padded_add_source) = (p)) /\ ((((exists pfa_gap_padded_add_sourceoperationresultbound. pfa_gap_padded_add_sourceoperationresultbound + S (pfp_value_padded_add_source) = (p)) /\ ((exists pfa_offset_left_padded_add_sourceoperationresultcongruence pfa_offset_right_padded_add_sourceoperationresultcongruence. ((pfp_left_padded_add_source) + (pfp_right_padded_add_source)) + (p) * pfa_offset_left_padded_add_sourceoperationresultcongruence = (pfp_value_padded_add_source) + (p) * pfa_offset_right_padded_add_sourceoperationresultcongruence)))))))))))))))) -> ((((exists pfa_gap_padded_add_ainside. pfa_gap_padded_add_ainside + S (i) = (L)) /\ ((((exists ff_h_pfp_padded_add_aentry. ff_h_pfp_padded_add_aentry + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_padded_add_aentry. ab = ff_q_pfp_padded_add_aentry * S ((S (i)) * ac) + (a)))))) \/ (((exists pfc_gap_padded_add_aoutside. pfc_gap_padded_add_aoutside+(L)=(i)) /\ (((a)=0))))) -> ((((exists pfa_gap_padded_add_binside. pfa_gap_padded_add_binside + S (i) = (L)) /\ ((((exists ff_h_pfp_padded_add_bentry. ff_h_pfp_padded_add_bentry + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_padded_add_bentry. bb = ff_q_pfp_padded_add_bentry * S ((S (i)) * bc) + (b)))))) \/ (((exists pfc_gap_padded_add_boutside. pfc_gap_padded_add_boutside+(L)=(i)) /\ (((b)=0))))) -> ((((exists pfa_gap_padded_add_rinside. pfa_gap_padded_add_rinside + S (i) = (L)) /\ ((((exists ff_h_pfp_padded_add_rentry. ff_h_pfp_padded_add_rentry + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_padded_add_rentry. cb = ff_q_pfp_padded_add_rentry * S ((S (i)) * cc) + (r)))))) \/ (((exists pfc_gap_padded_add_routside. pfc_gap_padded_add_routside+(L)=(i)) /\ (((r)=0))))) -> (exists pfa_offset_left_padded_add_result pfa_offset_right_padded_add_result. (a+b) + (p) * pfa_offset_left_padded_add_result = (r) + (p) * pfa_offset_right_padded_add_result)

Constructive proof overview

Generated structural guide

An actual coefficient sum extends by actual zeros to an additive congruence at every index; no claim is made about arbitrary decoded entries outside the original prefixes.

The unchanged tactic script uses 3 declared prerequisites and contains 92 exact native proof lines.

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

Proof neighborhood

Direct dependencies

polynomial_zero_extended_entry_inside Alpha theorem; checked-use authorized prime_field_polynomial_add_entry Alpha theorem; checked-use authorized polynomial_zero_extended_entry_functional Alpha theorem; checked-use authorized

Direct dependents

PX0042 polynomial_diagonal_term_left_add_congruent PX0043 polynomial_diagonal_term_right_add_congruent

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

92 script commands · 20 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.

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–10

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro L
  9. L9
    intro i
  10. L10
    intro a
02Fix variables and assumptionsL11–16

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

  1. L11
    intro b
  2. L12
    intro r
  3. L13
    intro hs
  4. L14
    intro ha
  5. L15
    intro hb
  6. L16
    intro hr
03Separate the logical casesL17–18

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

  1. L17
    cases ha
  2. L18
    cases ha_left
04Establish hebL19–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry inside.

  1. L19
    have heb : ((exists ff_h_pfp_padded_add_heb. ff_h_pfp_padded_add_heb + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_padded_add_heb. bb = ff_q_pfp_padded_add_heb * S ((S (i)) * bc) + (b))
  2. L20
    specialize polynomial_zero_extended_entry_inside (bb)
  3. L21
    specialize polynomial_zero_extended_entry_inside (bc)
  4. L22
    specialize polynomial_zero_extended_entry_inside (L)
  5. L23
    specialize polynomial_zero_extended_entry_inside (i)
  6. L24
    specialize polynomial_zero_extended_entry_inside (b)
  7. L25
    apply polynomial_zero_extended_entry_inside
  8. L26
    exact ha_left_left
  9. L27
    exact hb
05Establish herL28–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry inside.

  1. L28
    have her : ((exists ff_h_pfp_padded_add_her. ff_h_pfp_padded_add_her + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_padded_add_her. cb = ff_q_pfp_padded_add_her * S ((S (i)) * cc) + (r))
  2. L29
    specialize polynomial_zero_extended_entry_inside (cb)
  3. L30
    specialize polynomial_zero_extended_entry_inside (cc)
  4. L31
    specialize polynomial_zero_extended_entry_inside (L)
  5. L32
    specialize polynomial_zero_extended_entry_inside (i)
  6. L33
    specialize polynomial_zero_extended_entry_inside (r)
  7. L34
    apply polynomial_zero_extended_entry_inside
  8. L35
    exact ha_left_left
  9. L36
    exact hr
06Establish hfieldL37–46

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

  1. L37
    have hfield : FpAdd(p,a,b,r)Definitions: FpAdd
  2. L38
    specialize prime_field_polynomial_add_entry (p)
  3. L39
    specialize prime_field_polynomial_add_entry (ab)
  4. L40
    specialize prime_field_polynomial_add_entry (ac)
  5. L41
    specialize prime_field_polynomial_add_entry (bb)
  6. L42
    specialize prime_field_polynomial_add_entry (bc)
  7. L43
    specialize prime_field_polynomial_add_entry (cb)
  8. L44
    specialize prime_field_polynomial_add_entry (cc)
  9. L45
    specialize prime_field_polynomial_add_entry (L)
  10. L46
    specialize prime_field_polynomial_add_entry (i)
07Use earlier factsL47–55

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

  1. L47
    specialize prime_field_polynomial_add_entry (a)
  2. L48
    specialize prime_field_polynomial_add_entry (b)
  3. L49
    specialize prime_field_polynomial_add_entry (r)
  4. L50
    apply prime_field_polynomial_add_entry
  5. L51
    exact hs
  6. L52
    exact ha_left_left
  7. L53
    exact ha_left_right
  8. L54
    exact heb
  9. L55
    exact her
08Separate the logical casesL56–58

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

  1. L56
    cases hfield
  2. L57
    cases hfield_right
  3. L58
    cases hfield_right_right
09Use earlier factsL59–59

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

  1. L59
    exact hfield_right_right_right
10Separate the logical casesL60–60

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

  1. L60
    cases ha_right
11Establish hbzeroL61–69

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry functional.

  1. L61
    have hbzero : b=0
  2. L62
    specialize polynomial_zero_extended_entry_functional (bb)
  3. L63
    specialize polynomial_zero_extended_entry_functional (bc)
  4. L64
    specialize polynomial_zero_extended_entry_functional (L)
  5. L65
    specialize polynomial_zero_extended_entry_functional (i)
  6. L66
    specialize polynomial_zero_extended_entry_functional (b)
  7. L67
    specialize polynomial_zero_extended_entry_functional (0)
  8. L68
    apply polynomial_zero_extended_entry_functional
  9. L69
    exact hb
12Separate the logical casesL70–71

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

  1. L70
    right
  2. L71
    split
13Use earlier factsL72–72

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

  1. L72
    exact ha_right_left
14Calculate and transport equalitiesL73–73

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

  1. L73
    refl
15Establish hrzeroL74–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry functional.

  1. L74
    have hrzero : r=0
  2. L75
    specialize polynomial_zero_extended_entry_functional (cb)
  3. L76
    specialize polynomial_zero_extended_entry_functional (cc)
  4. L77
    specialize polynomial_zero_extended_entry_functional (L)
  5. L78
    specialize polynomial_zero_extended_entry_functional (i)
  6. L79
    specialize polynomial_zero_extended_entry_functional (r)
  7. L80
    specialize polynomial_zero_extended_entry_functional (0)
  8. L81
    apply polynomial_zero_extended_entry_functional
  9. L82
    exact hr
16Separate the logical casesL83–84

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

  1. L83
    right
  2. L84
    split
17Use earlier factsL85–85

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

  1. L85
    exact ha_right_left
18Calculate and transport equalitiesL86–89

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

  1. L86
    refl
  2. L87
    rewrite ha_right_right
  3. L88
    rewrite hbzero
  4. L89
    rewrite hrzero
19Construct an explicit witnessL90–91

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

  1. L90
    exists 0
  2. L91
    exists 0
20Calculate and transport equalitiesL92–92

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

  1. L92
    simp

Library-wide reading audit

Original exact command ledger · 92 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro L
  9. 0009intro i
  10. 0010intro a
  11. 0011intro b
  12. 0012intro r
  13. 0013intro hs
  14. 0014intro ha
  15. 0015intro hb
  16. 0016intro hr
  17. 0017cases ha
  18. 0018cases ha_left
  19. 0019have heb : ((exists ff_h_pfp_padded_add_heb. ff_h_pfp_padded_add_heb + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_padded_add_heb. bb = ff_q_pfp_padded_add_heb * S ((S (i)) * bc) + (b))
  20. 0020specialize polynomial_zero_extended_entry_inside (bb)
  21. 0021specialize polynomial_zero_extended_entry_inside (bc)
  22. 0022specialize polynomial_zero_extended_entry_inside (L)
  23. 0023specialize polynomial_zero_extended_entry_inside (i)
  24. 0024specialize polynomial_zero_extended_entry_inside (b)
  25. 0025apply polynomial_zero_extended_entry_inside
  26. 0026exact ha_left_left
  27. 0027exact hb
  28. 0028have her : ((exists ff_h_pfp_padded_add_her. ff_h_pfp_padded_add_her + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_padded_add_her. cb = ff_q_pfp_padded_add_her * S ((S (i)) * cc) + (r))
  29. 0029specialize polynomial_zero_extended_entry_inside (cb)
  30. 0030specialize polynomial_zero_extended_entry_inside (cc)
  31. 0031specialize polynomial_zero_extended_entry_inside (L)
  32. 0032specialize polynomial_zero_extended_entry_inside (i)
  33. 0033specialize polynomial_zero_extended_entry_inside (r)
  34. 0034apply polynomial_zero_extended_entry_inside
  35. 0035exact ha_left_left
  36. 0036exact hr
  37. 0037have hfield : ((exists pfa_gap_padded_add_inside_valueleft. pfa_gap_padded_add_inside_valueleft + S (a) = (p)) /\ (((exists pfa_gap_padded_add_inside_valueright. pfa_gap_padded_add_inside_valueright + S (b) = (p)) /\ ((((exists pfa_gap_padded_add_inside_valueresultbound. pfa_gap_padded_add_inside_valueresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_padded_add_inside_valueresultcongruence pfa_offset_right_padded_add_inside_valueresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_padded_add_inside_valueresultcongruence = (r) + (p) * pfa_offset_right_padded_add_inside_valueresultcongruence))))))))
  38. 0038specialize prime_field_polynomial_add_entry (p)
  39. 0039specialize prime_field_polynomial_add_entry (ab)
  40. 0040specialize prime_field_polynomial_add_entry (ac)
  41. 0041specialize prime_field_polynomial_add_entry (bb)
  42. 0042specialize prime_field_polynomial_add_entry (bc)
  43. 0043specialize prime_field_polynomial_add_entry (cb)
  44. 0044specialize prime_field_polynomial_add_entry (cc)
  45. 0045specialize prime_field_polynomial_add_entry (L)
  46. 0046specialize prime_field_polynomial_add_entry (i)
  47. 0047specialize prime_field_polynomial_add_entry (a)
  48. 0048specialize prime_field_polynomial_add_entry (b)
  49. 0049specialize prime_field_polynomial_add_entry (r)
  50. 0050apply prime_field_polynomial_add_entry
  51. 0051exact hs
  52. 0052exact ha_left_left
  53. 0053exact ha_left_right
  54. 0054exact heb
  55. 0055exact her
  56. 0056cases hfield
  57. 0057cases hfield_right
  58. 0058cases hfield_right_right
  59. 0059exact hfield_right_right_right
  60. 0060cases ha_right
  61. 0061have hbzero : b=0
  62. 0062specialize polynomial_zero_extended_entry_functional (bb)
  63. 0063specialize polynomial_zero_extended_entry_functional (bc)
  64. 0064specialize polynomial_zero_extended_entry_functional (L)
  65. 0065specialize polynomial_zero_extended_entry_functional (i)
  66. 0066specialize polynomial_zero_extended_entry_functional (b)
  67. 0067specialize polynomial_zero_extended_entry_functional (0)
  68. 0068apply polynomial_zero_extended_entry_functional
  69. 0069exact hb
  70. 0070right
  71. 0071split
  72. 0072exact ha_right_left
  73. 0073refl
  74. 0074have hrzero : r=0
  75. 0075specialize polynomial_zero_extended_entry_functional (cb)
  76. 0076specialize polynomial_zero_extended_entry_functional (cc)
  77. 0077specialize polynomial_zero_extended_entry_functional (L)
  78. 0078specialize polynomial_zero_extended_entry_functional (i)
  79. 0079specialize polynomial_zero_extended_entry_functional (r)
  80. 0080specialize polynomial_zero_extended_entry_functional (0)
  81. 0081apply polynomial_zero_extended_entry_functional
  82. 0082exact hr
  83. 0083right
  84. 0084split
  85. 0085exact ha_right_left
  86. 0086refl
  87. 0087rewrite ha_right_right
  88. 0088rewrite hbzero
  89. 0089rewrite hrzero
  90. 0090exists 0
  91. 0091exists 0
  92. 0092simp