PQ0018

prime_field_polynomial_subtract_equal_zero

Subtracting extensionally equal canonical prefixes gives an actual all-zero prefix even when their beta encodings differ.

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. ∀ bb. ∀ bc. ∀ rb. ∀ rc. ∀ l. Prime(p) → (∀ x. ∀ y. Lt(x,l) → BetaAt(ab,ac,x,y) → BetaAt(bb,bc,x,y)) → FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l) → Repeat(rb,rc,0,l)

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

Definition DAG

FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 4Repeat(b,c,a,l) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_polynomial_subtract_equal_entry_zero
Original expanded first-order statement 
forall p ab ac bb bc rb rc l. (~((p) = 1) /\ forall pfa_factor_left_sub_equal_prime pfa_factor_right_sub_equal_prime. (p) = pfa_factor_left_sub_equal_prime * pfa_factor_right_sub_equal_prime -> pfa_factor_left_sub_equal_prime = 1 \/ pfa_factor_right_sub_equal_prime = 1) -> (forall mdr_i_pfp_sub_equal_inputs mdr_a_pfp_sub_equal_inputs. (exists mdr_gap_pfp_sub_equal_inputsb. mdr_gap_pfp_sub_equal_inputsb + S (mdr_i_pfp_sub_equal_inputs) = (l)) -> (((exists ff_h_mdr_pfp_sub_equal_inputso. ff_h_mdr_pfp_sub_equal_inputso + S (mdr_a_pfp_sub_equal_inputs) = S ((S (mdr_i_pfp_sub_equal_inputs)) * ac)) /\ exists ff_q_mdr_pfp_sub_equal_inputso. ab = ff_q_mdr_pfp_sub_equal_inputso * S ((S (mdr_i_pfp_sub_equal_inputs)) * ac) + (mdr_a_pfp_sub_equal_inputs))) -> (((exists ff_h_mdr_pfp_sub_equal_inputsn. ff_h_mdr_pfp_sub_equal_inputsn + S (mdr_a_pfp_sub_equal_inputs) = S ((S (mdr_i_pfp_sub_equal_inputs)) * bc)) /\ exists ff_q_mdr_pfp_sub_equal_inputsn. bb = ff_q_mdr_pfp_sub_equal_inputsn * S ((S (mdr_i_pfp_sub_equal_inputs)) * bc) + (mdr_a_pfp_sub_equal_inputs)))) -> (forall pfs_index_sub_equal_graph. (exists pfa_gap_sub_equal_graphindex. pfa_gap_sub_equal_graphindex + S (pfs_index_sub_equal_graph) = (l)) -> exists pfs_left_sub_equal_graph pfs_right_sub_equal_graph pfs_result_sub_equal_graph. ((((exists ff_h_pfp_sub_equal_graphleft. ff_h_pfp_sub_equal_graphleft + S (pfs_left_sub_equal_graph) = S ((S (pfs_index_sub_equal_graph)) * ac)) /\ exists ff_q_pfp_sub_equal_graphleft. ab = ff_q_pfp_sub_equal_graphleft * S ((S (pfs_index_sub_equal_graph)) * ac) + (pfs_left_sub_equal_graph))) /\ (((((exists ff_h_pfp_sub_equal_graphright. ff_h_pfp_sub_equal_graphright + S (pfs_right_sub_equal_graph) = S ((S (pfs_index_sub_equal_graph)) * bc)) /\ exists ff_q_pfp_sub_equal_graphright. bb = ff_q_pfp_sub_equal_graphright * S ((S (pfs_index_sub_equal_graph)) * bc) + (pfs_right_sub_equal_graph))) /\ (((((exists ff_h_pfp_sub_equal_graphresult. ff_h_pfp_sub_equal_graphresult + S (pfs_result_sub_equal_graph) = S ((S (pfs_index_sub_equal_graph)) * rc)) /\ exists ff_q_pfp_sub_equal_graphresult. rb = ff_q_pfp_sub_equal_graphresult * S ((S (pfs_index_sub_equal_graph)) * rc) + (pfs_result_sub_equal_graph))) /\ ((((exists pfa_gap_sub_equal_graphoperationleft. pfa_gap_sub_equal_graphoperationleft + S (pfs_right_sub_equal_graph) = (p)) /\ (((exists pfa_gap_sub_equal_graphoperationright. pfa_gap_sub_equal_graphoperationright + S (pfs_result_sub_equal_graph) = (p)) /\ ((((exists pfa_gap_sub_equal_graphoperationresultbound. pfa_gap_sub_equal_graphoperationresultbound + S (pfs_left_sub_equal_graph) = (p)) /\ ((exists pfa_offset_left_sub_equal_graphoperationresultcongruence pfa_offset_right_sub_equal_graphoperationresultcongruence. ((pfs_right_sub_equal_graph) + (pfs_result_sub_equal_graph)) + (p) * pfa_offset_left_sub_equal_graphoperationresultcongruence = (pfs_left_sub_equal_graph) + (p) * pfa_offset_right_sub_equal_graphoperationresultcongruence)))))))))))))))) -> (forall pfp_repeat_index_sub_equal_result. (exists pfa_gap_sub_equal_resultindex. pfa_gap_sub_equal_resultindex + S (pfp_repeat_index_sub_equal_result) = (l)) -> (((exists ff_h_pfp_sub_equal_resultentry. ff_h_pfp_sub_equal_resultentry + S (0) = S ((S (pfp_repeat_index_sub_equal_result)) * rc)) /\ exists ff_q_pfp_sub_equal_resultentry. rb = ff_q_pfp_sub_equal_resultentry * S ((S (pfp_repeat_index_sub_equal_result)) * rc) + (0))))

Complete tactic proof in conservative notation

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

51 script commands · 11 reading checkpoints · 3 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.

Named ingredients (1)
prime field polynomial subtract equal entry zero
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 rb
  7. L7
    intro rc
  8. L8
    intro l
  9. L9
    intro hp
  10. L10
    intro he
02Fix variables and assumptionsL11–13

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

  1. L11
    intro h
  2. L12
    intro i
  3. L13
    intro hi
03Establish haL14–18

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

  1. L14
    have ha : ∃ a. BetaAt(ab,ac,i,a)Definitions: BetaAt(ab,ac,i,a)Original native command in the exact edition
  2. L15
    specialize beta_at_exists (ab)
  3. L16
    specialize beta_at_exists (ac)
  4. L17
    specialize beta_at_exists (i)
  5. L18
    apply beta_at_exists
04Separate the logical casesL19–19

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

  1. L19
    cases ha
05Establish hrL20–24

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

  1. L20
    have hr : ∃ r. BetaAt(rb,rc,i,r)Definitions: BetaAt(rb,rc,i,r)Original native command in the exact edition
  2. L21
    specialize beta_at_exists (rb)
  3. L22
    specialize beta_at_exists (rc)
  4. L23
    specialize beta_at_exists (i)
  5. L24
    apply beta_at_exists
06Separate the logical casesL25–25

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

  1. L25
    cases hr
07Establish hzL26–35

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

  1. L26
    have hz : x1=0
  2. L27
    specialize prime_field_polynomial_subtract_equal_entry_zero (p)
  3. L28
    specialize prime_field_polynomial_subtract_equal_entry_zero (ab)
  4. L29
    specialize prime_field_polynomial_subtract_equal_entry_zero (ac)
  5. L30
    specialize prime_field_polynomial_subtract_equal_entry_zero (bb)
  6. L31
    specialize prime_field_polynomial_subtract_equal_entry_zero (bc)
  7. L32
    specialize prime_field_polynomial_subtract_equal_entry_zero (rb)
  8. L33
    specialize prime_field_polynomial_subtract_equal_entry_zero (rc)
  9. L34
    specialize prime_field_polynomial_subtract_equal_entry_zero (l)
  10. L35
    specialize prime_field_polynomial_subtract_equal_entry_zero (i)
08Use earlier factsL36–45

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

  1. L36
    specialize prime_field_polynomial_subtract_equal_entry_zero (x)
  2. L37
    specialize prime_field_polynomial_subtract_equal_entry_zero (x1)
  3. L38
    apply prime_field_polynomial_subtract_equal_entry_zero
  4. L39
    exact hp
  5. L40
    exact h
  6. L41
    exact hi
  7. L42
    exact ha_witness
  8. L43
    specialize he (i)
  9. L44
    specialize he (x)
  10. L45
    apply he
09Use earlier factsL46–48

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

  1. L46
    exact hi
  2. L47
    exact ha_witness
  3. L48
    exact hr_witness
10Calculate and transport equalitiesL49–50

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

  1. L49
    rewrite hz at hr_witness
  2. L50
    rewrite hz at hr_witness
11Use earlier factsL51–51

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

  1. L51
    exact hr_witness

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro l
  9. 0009intro hp
  10. 0010intro he
  11. 0011intro h
  12. 0012intro i
  13. 0013intro hi
  14. 0014have ha : ∃ a. BetaAt(ab,ac,i,a)
  15. 0015specialize beta_at_exists (ab)
  16. 0016specialize beta_at_exists (ac)
  17. 0017specialize beta_at_exists (i)
  18. 0018apply beta_at_exists
  19. 0019cases ha
  20. 0020have hr : ∃ r. BetaAt(rb,rc,i,r)
  21. 0021specialize beta_at_exists (rb)
  22. 0022specialize beta_at_exists (rc)
  23. 0023specialize beta_at_exists (i)
  24. 0024apply beta_at_exists
  25. 0025cases hr
  26. 0026have hz : x1=0
  27. 0027specialize prime_field_polynomial_subtract_equal_entry_zero (p)
  28. 0028specialize prime_field_polynomial_subtract_equal_entry_zero (ab)
  29. 0029specialize prime_field_polynomial_subtract_equal_entry_zero (ac)
  30. 0030specialize prime_field_polynomial_subtract_equal_entry_zero (bb)
  31. 0031specialize prime_field_polynomial_subtract_equal_entry_zero (bc)
  32. 0032specialize prime_field_polynomial_subtract_equal_entry_zero (rb)
  33. 0033specialize prime_field_polynomial_subtract_equal_entry_zero (rc)
  34. 0034specialize prime_field_polynomial_subtract_equal_entry_zero (l)
  35. 0035specialize prime_field_polynomial_subtract_equal_entry_zero (i)
  36. 0036specialize prime_field_polynomial_subtract_equal_entry_zero (x)
  37. 0037specialize prime_field_polynomial_subtract_equal_entry_zero (x1)
  38. 0038apply prime_field_polynomial_subtract_equal_entry_zero
  39. 0039exact hp
  40. 0040exact h
  41. 0041exact hi
  42. 0042exact ha_witness
  43. 0043specialize he (i)
  44. 0044specialize he (x)
  45. 0045apply he
  46. 0046exact hi
  47. 0047exact ha_witness
  48. 0048exact hr_witness
  49. 0049rewrite hz at hr_witness
  50. 0050rewrite hz at hr_witness
  51. 0051exact hr_witness