PQ000E

prime_field_polynomial_subtract_entry

Every actual decoded tuple satisfies the bounded scalar graph, independently of its existential witnesses.

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. ∀ i. ∀ a. ∀ b. ∀ r. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l) → Lt(i,l) → BetaAt(ab,ac,i,a) → BetaAt(bb,bc,i,b) → BetaAt(rb,rc,i,r) → FpAdd(p,b,r,a)

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

Definition DAG

FpAdd(p,a,b,c) · 2FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 6

Actual proof prerequisites

beta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall p ab ac bb bc rb rc l i a b r. (forall pfs_index_subtract_entry_graph. (exists pfa_gap_subtract_entry_graphindex. pfa_gap_subtract_entry_graphindex + S (pfs_index_subtract_entry_graph) = (l)) -> exists pfs_left_subtract_entry_graph pfs_right_subtract_entry_graph pfs_result_subtract_entry_graph. ((((exists ff_h_pfp_subtract_entry_graphleft. ff_h_pfp_subtract_entry_graphleft + S (pfs_left_subtract_entry_graph) = S ((S (pfs_index_subtract_entry_graph)) * ac)) /\ exists ff_q_pfp_subtract_entry_graphleft. ab = ff_q_pfp_subtract_entry_graphleft * S ((S (pfs_index_subtract_entry_graph)) * ac) + (pfs_left_subtract_entry_graph))) /\ (((((exists ff_h_pfp_subtract_entry_graphright. ff_h_pfp_subtract_entry_graphright + S (pfs_right_subtract_entry_graph) = S ((S (pfs_index_subtract_entry_graph)) * bc)) /\ exists ff_q_pfp_subtract_entry_graphright. bb = ff_q_pfp_subtract_entry_graphright * S ((S (pfs_index_subtract_entry_graph)) * bc) + (pfs_right_subtract_entry_graph))) /\ (((((exists ff_h_pfp_subtract_entry_graphresult. ff_h_pfp_subtract_entry_graphresult + S (pfs_result_subtract_entry_graph) = S ((S (pfs_index_subtract_entry_graph)) * rc)) /\ exists ff_q_pfp_subtract_entry_graphresult. rb = ff_q_pfp_subtract_entry_graphresult * S ((S (pfs_index_subtract_entry_graph)) * rc) + (pfs_result_subtract_entry_graph))) /\ ((((exists pfa_gap_subtract_entry_graphoperationleft. pfa_gap_subtract_entry_graphoperationleft + S (pfs_right_subtract_entry_graph) = (p)) /\ (((exists pfa_gap_subtract_entry_graphoperationright. pfa_gap_subtract_entry_graphoperationright + S (pfs_result_subtract_entry_graph) = (p)) /\ ((((exists pfa_gap_subtract_entry_graphoperationresultbound. pfa_gap_subtract_entry_graphoperationresultbound + S (pfs_left_subtract_entry_graph) = (p)) /\ ((exists pfa_offset_left_subtract_entry_graphoperationresultcongruence pfa_offset_right_subtract_entry_graphoperationresultcongruence. ((pfs_right_subtract_entry_graph) + (pfs_result_subtract_entry_graph)) + (p) * pfa_offset_left_subtract_entry_graphoperationresultcongruence = (pfs_left_subtract_entry_graph) + (p) * pfa_offset_right_subtract_entry_graphoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_subtract_entry_index. pfa_gap_subtract_entry_index + S (i) = (l)) -> (((exists ff_h_pfp_subtract_entry_a. ff_h_pfp_subtract_entry_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_subtract_entry_a. ab = ff_q_pfp_subtract_entry_a * S ((S (i)) * ac) + (a))) -> (((exists ff_h_pfp_subtract_entry_b. ff_h_pfp_subtract_entry_b + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_subtract_entry_b. bb = ff_q_pfp_subtract_entry_b * S ((S (i)) * bc) + (b))) -> (((exists ff_h_pfp_subtract_entry_r. ff_h_pfp_subtract_entry_r + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_subtract_entry_r. rb = ff_q_pfp_subtract_entry_r * S ((S (i)) * rc) + (r))) -> (((exists pfa_gap_subtract_entry_resultleft. pfa_gap_subtract_entry_resultleft + S (b) = (p)) /\ (((exists pfa_gap_subtract_entry_resultright. pfa_gap_subtract_entry_resultright + S (r) = (p)) /\ ((((exists pfa_gap_subtract_entry_resultresultbound. pfa_gap_subtract_entry_resultresultbound + S (a) = (p)) /\ ((exists pfa_offset_left_subtract_entry_resultresultcongruence pfa_offset_right_subtract_entry_resultresultcongruence. ((b) + (r)) + (p) * pfa_offset_left_subtract_entry_resultresultcongruence = (a) + (p) * pfa_offset_right_subtract_entry_resultresultcongruence)))))))))

Complete tactic proof in conservative notation

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

61 script commands · 11 reading checkpoints · 4 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 rb
  7. L7
    intro rc
  8. L8
    intro l
  9. L9
    intro i
  10. L10
    intro a
02Fix variables and assumptionsL11–17

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

  1. L11
    intro b
  2. L12
    intro r
  3. L13
    intro h
  4. L14
    intro hi
  5. L15
    intro ha
  6. L16
    intro hb
  7. L17
    intro hr
03Establish hvL18–21

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

  1. L18
    have hv : ∃ u0. ∃ u1. ∃ u2. BetaAt(ab,ac,i,u0) ∧ (BetaAt(bb,bc,i,u1) ∧ (BetaAt(rb,rc,i,u2) ∧ FpAdd(p,u1,u2,u0)))Definitions: BetaAt(ab,ac,i,u0)BetaAt(bb,bc,i,u1)BetaAt(rb,rc,i,u2)FpAdd(p,u1,u2,u0)Original native command in the exact edition
  2. L19
    specialize h (i)
  3. L20
    apply h
  4. L21
    exact hi
04Separate the logical casesL22–27

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

  1. L22
    cases hv
  2. L23
    cases hv_witness
  3. L24
    cases hv_witness_witness
  4. L25
    cases hv_witness_witness_witness
  5. L26
    cases hv_witness_witness_witness_right
  6. L27
    cases hv_witness_witness_witness_right_right
05Establish heq0L28–37

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

  1. L28
    have heq0 : x=a
  2. L29
    specialize beta_at_unique (ab)
  3. L30
    specialize beta_at_unique (ac)
  4. L31
    specialize beta_at_unique (i)
  5. L32
    specialize beta_at_unique (x)
  6. L33
    specialize beta_at_unique (a)
  7. L34
    apply beta_at_unique
  8. L35
    exact hv_witness_witness_witness_left
  9. L36
    exact ha
  10. L37
    rewrite heq0 at hv_witness_witness_witness_right_right_right
06Calculate and transport equalitiesL38–38

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

  1. L38
    rewrite heq0 at hv_witness_witness_witness_right_right_right
07Establish heq1L39–48

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

  1. L39
    have heq1 : x1=b
  2. L40
    specialize beta_at_unique (bb)
  3. L41
    specialize beta_at_unique (bc)
  4. L42
    specialize beta_at_unique (i)
  5. L43
    specialize beta_at_unique (x1)
  6. L44
    specialize beta_at_unique (b)
  7. L45
    apply beta_at_unique
  8. L46
    exact hv_witness_witness_witness_right_left
  9. L47
    exact hb
  10. L48
    rewrite heq1 at hv_witness_witness_witness_right_right_right
08Calculate and transport equalitiesL49–49

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

  1. L49
    rewrite heq1 at hv_witness_witness_witness_right_right_right
09Establish heq2L50–59

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

  1. L50
    have heq2 : x2=r
  2. L51
    specialize beta_at_unique (rb)
  3. L52
    specialize beta_at_unique (rc)
  4. L53
    specialize beta_at_unique (i)
  5. L54
    specialize beta_at_unique (x2)
  6. L55
    specialize beta_at_unique (r)
  7. L56
    apply beta_at_unique
  8. L57
    exact hv_witness_witness_witness_right_right_left
  9. L58
    exact hr
  10. L59
    rewrite heq2 at hv_witness_witness_witness_right_right_right
10Calculate and transport equalitiesL60–60

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

  1. L60
    rewrite heq2 at hv_witness_witness_witness_right_right_right
11Use earlier factsL61–61

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

  1. L61
    exact hv_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 61 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 i
  10. 0010intro a
  11. 0011intro b
  12. 0012intro r
  13. 0013intro h
  14. 0014intro hi
  15. 0015intro ha
  16. 0016intro hb
  17. 0017intro hr
  18. 0018have hv : ∃ u0. ∃ u1. ∃ u2. BetaAt(ab,ac,i,u0) ∧ (BetaAt(bb,bc,i,u1) ∧ (BetaAt(rb,rc,i,u2) ∧ FpAdd(p,u1,u2,u0)))
  19. 0019specialize h (i)
  20. 0020apply h
  21. 0021exact hi
  22. 0022cases hv
  23. 0023cases hv_witness
  24. 0024cases hv_witness_witness
  25. 0025cases hv_witness_witness_witness
  26. 0026cases hv_witness_witness_witness_right
  27. 0027cases hv_witness_witness_witness_right_right
  28. 0028have heq0 : x=a
  29. 0029specialize beta_at_unique (ab)
  30. 0030specialize beta_at_unique (ac)
  31. 0031specialize beta_at_unique (i)
  32. 0032specialize beta_at_unique (x)
  33. 0033specialize beta_at_unique (a)
  34. 0034apply beta_at_unique
  35. 0035exact hv_witness_witness_witness_left
  36. 0036exact ha
  37. 0037rewrite heq0 at hv_witness_witness_witness_right_right_right
  38. 0038rewrite heq0 at hv_witness_witness_witness_right_right_right
  39. 0039have heq1 : x1=b
  40. 0040specialize beta_at_unique (bb)
  41. 0041specialize beta_at_unique (bc)
  42. 0042specialize beta_at_unique (i)
  43. 0043specialize beta_at_unique (x1)
  44. 0044specialize beta_at_unique (b)
  45. 0045apply beta_at_unique
  46. 0046exact hv_witness_witness_witness_right_left
  47. 0047exact hb
  48. 0048rewrite heq1 at hv_witness_witness_witness_right_right_right
  49. 0049rewrite heq1 at hv_witness_witness_witness_right_right_right
  50. 0050have heq2 : x2=r
  51. 0051specialize beta_at_unique (rb)
  52. 0052specialize beta_at_unique (rc)
  53. 0053specialize beta_at_unique (i)
  54. 0054specialize beta_at_unique (x2)
  55. 0055specialize beta_at_unique (r)
  56. 0056apply beta_at_unique
  57. 0057exact hv_witness_witness_witness_right_right_left
  58. 0058exact hr
  59. 0059rewrite heq2 at hv_witness_witness_witness_right_right_right
  60. 0060rewrite heq2 at hv_witness_witness_witness_right_right_right
  61. 0061exact hv_witness_witness_witness_right_right_right