PQ000E

prime_field_polynomial_subtract_entry

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

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

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 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)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 61 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized

Direct dependents

PQ0010 prime_field_polynomial_subtract_functional PQ0017 prime_field_polynomial_subtract_equal_entry_zero

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

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.

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 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: FpAddBetaAt
  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 exact 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 : exists u0 u1 u2. (((((exists ff_h_pfp_subtract_entry_chosen0. ff_h_pfp_subtract_entry_chosen0 + S (u0) = S ((S (i)) * ac)) /\ exists ff_q_pfp_subtract_entry_chosen0. ab = ff_q_pfp_subtract_entry_chosen0 * S ((S (i)) * ac) + (u0))) /\ (((((exists ff_h_pfp_subtract_entry_chosen1. ff_h_pfp_subtract_entry_chosen1 + S (u1) = S ((S (i)) * bc)) /\ exists ff_q_pfp_subtract_entry_chosen1. bb = ff_q_pfp_subtract_entry_chosen1 * S ((S (i)) * bc) + (u1))) /\ (((((exists ff_h_pfp_subtract_entry_chosen2. ff_h_pfp_subtract_entry_chosen2 + S (u2) = S ((S (i)) * rc)) /\ exists ff_q_pfp_subtract_entry_chosen2. rb = ff_q_pfp_subtract_entry_chosen2 * S ((S (i)) * rc) + (u2))) /\ ((((exists pfa_gap_subtract_entry_chosenoperationleft. pfa_gap_subtract_entry_chosenoperationleft + S (u1) = (p)) /\ (((exists pfa_gap_subtract_entry_chosenoperationright. pfa_gap_subtract_entry_chosenoperationright + S (u2) = (p)) /\ ((((exists pfa_gap_subtract_entry_chosenoperationresultbound. pfa_gap_subtract_entry_chosenoperationresultbound + S (u0) = (p)) /\ ((exists pfa_offset_left_subtract_entry_chosenoperationresultcongruence pfa_offset_right_subtract_entry_chosenoperationresultcongruence. ((u1) + (u2)) + (p) * pfa_offset_left_subtract_entry_chosenoperationresultcongruence = (u0) + (p) * pfa_offset_right_subtract_entry_chosenoperationresultcongruence))))))))))))))))
  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