PQ000B

prime_field_polynomial_negate_add_zero

Adding actual opposite coefficient values produces any genuine zero-prefix encoding.

Alpha v34 checked-use · first admitted v32 · 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 coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ rb. ∀ rc. ∀ zb. ∀ zc. ∀ l. FpCoefficientNegation(p,ab,ac,rb,rc,l) → Repeat(zb,zc,0,l) → FpPolyAdd(p,ab,ac,rb,rc,zb,zc,l)

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) · 1FpCoefficientNegation(p,ab,ac,rb,rc,L) · 1BetaAt(b,c,i,x) · 2Repeat(b,c,a,l) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall p ab ac rb rc zb zc l. (forall pfs_index_neg_add_graph. (exists pfa_gap_neg_add_graphindex. pfa_gap_neg_add_graphindex + S (pfs_index_neg_add_graph) = (l)) -> exists pfs_source_neg_add_graph pfs_result_neg_add_graph. ((((exists ff_h_pfp_neg_add_graphsource. ff_h_pfp_neg_add_graphsource + S (pfs_source_neg_add_graph) = S ((S (pfs_index_neg_add_graph)) * ac)) /\ exists ff_q_pfp_neg_add_graphsource. ab = ff_q_pfp_neg_add_graphsource * S ((S (pfs_index_neg_add_graph)) * ac) + (pfs_source_neg_add_graph))) /\ (((((exists ff_h_pfp_neg_add_graphresult. ff_h_pfp_neg_add_graphresult + S (pfs_result_neg_add_graph) = S ((S (pfs_index_neg_add_graph)) * rc)) /\ exists ff_q_pfp_neg_add_graphresult. rb = ff_q_pfp_neg_add_graphresult * S ((S (pfs_index_neg_add_graph)) * rc) + (pfs_result_neg_add_graph))) /\ ((((exists pfa_gap_neg_add_graphoperationadditionleft. pfa_gap_neg_add_graphoperationadditionleft + S (pfs_source_neg_add_graph) = (p)) /\ (((exists pfa_gap_neg_add_graphoperationadditionright. pfa_gap_neg_add_graphoperationadditionright + S (pfs_result_neg_add_graph) = (p)) /\ ((((exists pfa_gap_neg_add_graphoperationadditionresultbound. pfa_gap_neg_add_graphoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_neg_add_graphoperationadditionresultcongruence pfa_offset_right_neg_add_graphoperationadditionresultcongruence. ((pfs_source_neg_add_graph) + (pfs_result_neg_add_graph)) + (p) * pfa_offset_left_neg_add_graphoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_neg_add_graphoperationadditionresultcongruence)))))))))))))) -> (forall pfp_repeat_index_neg_add_zero. (exists pfa_gap_neg_add_zeroindex. pfa_gap_neg_add_zeroindex + S (pfp_repeat_index_neg_add_zero) = (l)) -> (((exists ff_h_pfp_neg_add_zeroentry. ff_h_pfp_neg_add_zeroentry + S (0) = S ((S (pfp_repeat_index_neg_add_zero)) * zc)) /\ exists ff_q_pfp_neg_add_zeroentry. zb = ff_q_pfp_neg_add_zeroentry * S ((S (pfp_repeat_index_neg_add_zero)) * zc) + (0)))) -> (forall pfp_index_neg_add_result. (exists pfa_gap_neg_add_resultindex. pfa_gap_neg_add_resultindex + S (pfp_index_neg_add_result) = (l)) -> exists pfp_left_neg_add_result pfp_right_neg_add_result pfp_value_neg_add_result. ((((exists ff_h_pfp_neg_add_resultleft. ff_h_pfp_neg_add_resultleft + S (pfp_left_neg_add_result) = S ((S (pfp_index_neg_add_result)) * ac)) /\ exists ff_q_pfp_neg_add_resultleft. ab = ff_q_pfp_neg_add_resultleft * S ((S (pfp_index_neg_add_result)) * ac) + (pfp_left_neg_add_result))) /\ (((((exists ff_h_pfp_neg_add_resultright. ff_h_pfp_neg_add_resultright + S (pfp_right_neg_add_result) = S ((S (pfp_index_neg_add_result)) * rc)) /\ exists ff_q_pfp_neg_add_resultright. rb = ff_q_pfp_neg_add_resultright * S ((S (pfp_index_neg_add_result)) * rc) + (pfp_right_neg_add_result))) /\ (((((exists ff_h_pfp_neg_add_resulttarget. ff_h_pfp_neg_add_resulttarget + S (pfp_value_neg_add_result) = S ((S (pfp_index_neg_add_result)) * zc)) /\ exists ff_q_pfp_neg_add_resulttarget. zb = ff_q_pfp_neg_add_resulttarget * S ((S (pfp_index_neg_add_result)) * zc) + (pfp_value_neg_add_result))) /\ ((((exists pfa_gap_neg_add_resultoperationleft. pfa_gap_neg_add_resultoperationleft + S (pfp_left_neg_add_result) = (p)) /\ (((exists pfa_gap_neg_add_resultoperationright. pfa_gap_neg_add_resultoperationright + S (pfp_right_neg_add_result) = (p)) /\ ((((exists pfa_gap_neg_add_resultoperationresultbound. pfa_gap_neg_add_resultoperationresultbound + S (pfp_value_neg_add_result) = (p)) /\ ((exists pfa_offset_left_neg_add_resultoperationresultcongruence pfa_offset_right_neg_add_resultoperationresultcongruence. ((pfp_left_neg_add_result) + (pfp_right_neg_add_result)) + (p) * pfa_offset_left_neg_add_resultoperationresultcongruence = (pfp_value_neg_add_result) + (p) * pfa_offset_right_neg_add_resultoperationresultcongruence))))))))))))))))

Complete tactic proof in conservative notation

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

32 script commands · 11 reading checkpoints · 1 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 rb
  5. L5
    intro rc
  6. L6
    intro zb
  7. L7
    intro zc
  8. L8
    intro l
  9. L9
    intro h
  10. L10
    intro hz
02Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
03Establish hvL13–16

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

  1. L13
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))Definitions: BetaAt(ab,ac,i,a)BetaAt(rb,rc,i,r)FpAdd(p,a,r,0)Original native command in the exact edition
  2. L14
    specialize h (i)
  3. L15
    apply h
  4. L16
    exact hi
04Separate the logical casesL17–20

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

  1. L17
    cases hv
  2. L18
    cases hv_witness
  3. L19
    cases hv_witness_witness
  4. L20
    cases hv_witness_witness_right
05Construct an explicit witnessL21–23

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

  1. L21
    exists x
  2. L22
    exists x1
  3. L23
    exists 0
06Separate the logical casesL24–24

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

  1. L24
    split
07Use earlier factsL25–25

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

  1. L25
    exact hv_witness_witness_left
08Separate the logical casesL26–26

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

  1. L26
    split
09Use earlier factsL27–27

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

  1. L27
    exact hv_witness_witness_right_left
10Separate the logical casesL28–28

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

  1. L28
    split
11Use earlier factsL29–32

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

  1. L29
    specialize hz (i)
  2. L30
    apply hz
  3. L31
    exact hi
  4. L32
    exact hv_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro zb
  7. 0007intro zc
  8. 0008intro l
  9. 0009intro h
  10. 0010intro hz
  11. 0011intro i
  12. 0012intro hi
  13. 0013have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))
  14. 0014specialize h (i)
  15. 0015apply h
  16. 0016exact hi
  17. 0017cases hv
  18. 0018cases hv_witness
  19. 0019cases hv_witness_witness
  20. 0020cases hv_witness_witness_right
  21. 0021exists x
  22. 0022exists x1
  23. 0023exists 0
  24. 0024split
  25. 0025exact hv_witness_witness_left
  26. 0026split
  27. 0027exact hv_witness_witness_right_left
  28. 0028split
  29. 0029specialize hz (i)
  30. 0030apply hz
  31. 0031exact hi
  32. 0032exact hv_witness_witness_right_right