PX0041

polynomial_zero_extended_add_congruent

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.

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

∀ p. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ cb. ∀ cc. ∀ L. ∀ i. ∀ a. ∀ b. ∀ r. FpPolyAdd(p,ab,ac,bb,bc,cb,cc,L) → BetaZeroExtend(ab,ac,L,i,a) → BetaZeroExtend(bb,bc,L,i,b) → BetaZeroExtend(cb,cc,L,i,r) → ModEq(p,a + b,r)

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

Definition DAG

FpAdd(p,a,b,c) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 1BetaZeroExtend(b,c,L,i,a) · 3ModEq(m,a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

polynomial_zero_extended_entry_inside · checked external prerequisiteprime_field_polynomial_add_entry · checked external prerequisitepolynomial_zero_extended_entry_functional · checked external prerequisite
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

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 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 : BetaAt(bb,bc,i,b)Definitions: BetaAt(bb,bc,i,b)Original native command in the exact edition
  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 : BetaAt(cb,cc,i,r)Definitions: BetaAt(cb,cc,i,r)Original native command in the exact edition
  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(p,a,b,r)Original native command in the exact edition
  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 defined 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 : BetaAt(bb,bc,i,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 : BetaAt(cb,cc,i,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 : FpAdd(p,a,b,r)
  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