PP000E

prime_field_polynomial_add_entry

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

Every decoded coefficient triple obeys the actual field-addition graph, independently of witness choices.

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 cb cc l i a b r. (forall pfp_index_add_entry_table. (exists pfa_gap_add_entry_tableindex. pfa_gap_add_entry_tableindex + S (pfp_index_add_entry_table) = (l)) -> exists pfp_left_add_entry_table pfp_right_add_entry_table pfp_value_add_entry_table. ((((exists ff_h_pfp_add_entry_tableleft. ff_h_pfp_add_entry_tableleft + S (pfp_left_add_entry_table) = S ((S (pfp_index_add_entry_table)) * ac)) /\ exists ff_q_pfp_add_entry_tableleft. ab = ff_q_pfp_add_entry_tableleft * S ((S (pfp_index_add_entry_table)) * ac) + (pfp_left_add_entry_table))) /\ (((((exists ff_h_pfp_add_entry_tableright. ff_h_pfp_add_entry_tableright + S (pfp_right_add_entry_table) = S ((S (pfp_index_add_entry_table)) * bc)) /\ exists ff_q_pfp_add_entry_tableright. bb = ff_q_pfp_add_entry_tableright * S ((S (pfp_index_add_entry_table)) * bc) + (pfp_right_add_entry_table))) /\ (((((exists ff_h_pfp_add_entry_tabletarget. ff_h_pfp_add_entry_tabletarget + S (pfp_value_add_entry_table) = S ((S (pfp_index_add_entry_table)) * cc)) /\ exists ff_q_pfp_add_entry_tabletarget. cb = ff_q_pfp_add_entry_tabletarget * S ((S (pfp_index_add_entry_table)) * cc) + (pfp_value_add_entry_table))) /\ ((((exists pfa_gap_add_entry_tableoperationleft. pfa_gap_add_entry_tableoperationleft + S (pfp_left_add_entry_table) = (p)) /\ (((exists pfa_gap_add_entry_tableoperationright. pfa_gap_add_entry_tableoperationright + S (pfp_right_add_entry_table) = (p)) /\ ((((exists pfa_gap_add_entry_tableoperationresultbound. pfa_gap_add_entry_tableoperationresultbound + S (pfp_value_add_entry_table) = (p)) /\ ((exists pfa_offset_left_add_entry_tableoperationresultcongruence pfa_offset_right_add_entry_tableoperationresultcongruence. ((pfp_left_add_entry_table) + (pfp_right_add_entry_table)) + (p) * pfa_offset_left_add_entry_tableoperationresultcongruence = (pfp_value_add_entry_table) + (p) * pfa_offset_right_add_entry_tableoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_add_entry_index. pfa_gap_add_entry_index + S (i) = (l)) -> (((exists ff_h_pfp_add_entry_input_a. ff_h_pfp_add_entry_input_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_entry_input_a. ab = ff_q_pfp_add_entry_input_a * S ((S (i)) * ac) + (a))) -> (((exists ff_h_pfp_add_entry_input_b. ff_h_pfp_add_entry_input_b + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_entry_input_b. bb = ff_q_pfp_add_entry_input_b * S ((S (i)) * bc) + (b))) -> (((exists ff_h_pfp_add_entry_output. ff_h_pfp_add_entry_output + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_add_entry_output. cb = ff_q_pfp_add_entry_output * S ((S (i)) * cc) + (r))) -> (((exists pfa_gap_add_entry_valueleft. pfa_gap_add_entry_valueleft + S (a) = (p)) /\ (((exists pfa_gap_add_entry_valueright. pfa_gap_add_entry_valueright + S (b) = (p)) /\ ((((exists pfa_gap_add_entry_valueresultbound. pfa_gap_add_entry_valueresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_add_entry_valueresultcongruence pfa_offset_right_add_entry_valueresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_add_entry_valueresultcongruence = (r) + (p) * pfa_offset_right_add_entry_valueresultcongruence)))))))))

Constructive proof overview

Generated structural guide

Every decoded coefficient triple obeys the actual field-addition graph, independently of witness choices.

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

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized

Direct dependents

PP0010 prime_field_polynomial_add_functional PP001C prime_field_polynomial_add_associative PP001E prime_field_polynomial_scale_distributes_over_add PP001F prime_field_polynomial_scalar_add_distributes

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 cb
  7. L7
    intro cc
  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 : ∃ u. ∃ v. ∃ w. BetaAt(ab,ac,i,u) ∧ (BetaAt(bb,bc,i,v) ∧ (BetaAt(cb,cc,i,w) ∧ FpAdd(p,u,v,w)))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 (cb)
  3. L52
    specialize beta_at_unique (cc)
  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 cb
  7. 0007intro cc
  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 u v w. ((((exists ff_h_pfp_add_entry_left. ff_h_pfp_add_entry_left + S (u) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_entry_left. ab = ff_q_pfp_add_entry_left * S ((S (i)) * ac) + (u))) /\ (((((exists ff_h_pfp_add_entry_right. ff_h_pfp_add_entry_right + S (v) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_entry_right. bb = ff_q_pfp_add_entry_right * S ((S (i)) * bc) + (v))) /\ (((((exists ff_h_pfp_add_entry_target. ff_h_pfp_add_entry_target + S (w) = S ((S (i)) * cc)) /\ exists ff_q_pfp_add_entry_target. cb = ff_q_pfp_add_entry_target * S ((S (i)) * cc) + (w))) /\ ((((exists pfa_gap_add_entry_operationleft. pfa_gap_add_entry_operationleft + S (u) = (p)) /\ (((exists pfa_gap_add_entry_operationright. pfa_gap_add_entry_operationright + S (v) = (p)) /\ ((((exists pfa_gap_add_entry_operationresultbound. pfa_gap_add_entry_operationresultbound + S (w) = (p)) /\ ((exists pfa_offset_left_add_entry_operationresultcongruence pfa_offset_right_add_entry_operationresultcongruence. ((u) + (v)) + (p) * pfa_offset_left_add_entry_operationresultcongruence = (w) + (p) * pfa_offset_right_add_entry_operationresultcongruence)))))))))))))))
  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 (cb)
  52. 0052specialize beta_at_unique (cc)
  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