PP000F

prime_field_polynomial_add_bounded

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

All three prefixes in an actual polynomial addition consist of canonical coefficients.

Exact expanded first-order arithmetic statement

forall p ab ac bb bc cb cc l. (forall pfp_index_add_bounded_table. (exists pfa_gap_add_bounded_tableindex. pfa_gap_add_bounded_tableindex + S (pfp_index_add_bounded_table) = (l)) -> exists pfp_left_add_bounded_table pfp_right_add_bounded_table pfp_value_add_bounded_table. ((((exists ff_h_pfp_add_bounded_tableleft. ff_h_pfp_add_bounded_tableleft + S (pfp_left_add_bounded_table) = S ((S (pfp_index_add_bounded_table)) * ac)) /\ exists ff_q_pfp_add_bounded_tableleft. ab = ff_q_pfp_add_bounded_tableleft * S ((S (pfp_index_add_bounded_table)) * ac) + (pfp_left_add_bounded_table))) /\ (((((exists ff_h_pfp_add_bounded_tableright. ff_h_pfp_add_bounded_tableright + S (pfp_right_add_bounded_table) = S ((S (pfp_index_add_bounded_table)) * bc)) /\ exists ff_q_pfp_add_bounded_tableright. bb = ff_q_pfp_add_bounded_tableright * S ((S (pfp_index_add_bounded_table)) * bc) + (pfp_right_add_bounded_table))) /\ (((((exists ff_h_pfp_add_bounded_tabletarget. ff_h_pfp_add_bounded_tabletarget + S (pfp_value_add_bounded_table) = S ((S (pfp_index_add_bounded_table)) * cc)) /\ exists ff_q_pfp_add_bounded_tabletarget. cb = ff_q_pfp_add_bounded_tabletarget * S ((S (pfp_index_add_bounded_table)) * cc) + (pfp_value_add_bounded_table))) /\ ((((exists pfa_gap_add_bounded_tableoperationleft. pfa_gap_add_bounded_tableoperationleft + S (pfp_left_add_bounded_table) = (p)) /\ (((exists pfa_gap_add_bounded_tableoperationright. pfa_gap_add_bounded_tableoperationright + S (pfp_right_add_bounded_table) = (p)) /\ ((((exists pfa_gap_add_bounded_tableoperationresultbound. pfa_gap_add_bounded_tableoperationresultbound + S (pfp_value_add_bounded_table) = (p)) /\ ((exists pfa_offset_left_add_bounded_tableoperationresultcongruence pfa_offset_right_add_bounded_tableoperationresultcongruence. ((pfp_left_add_bounded_table) + (pfp_right_add_bounded_table)) + (p) * pfa_offset_left_add_bounded_tableoperationresultcongruence = (pfp_value_add_bounded_table) + (p) * pfa_offset_right_add_bounded_tableoperationresultcongruence)))))))))))))))) -> ((forall fom_index_pfp_add_bounded_ab. (exists fom_gap_pfp_add_bounded_ab_index_bound. fom_gap_pfp_add_bounded_ab_index_bound + S (fom_index_pfp_add_bounded_ab) = l) -> exists fom_value_pfp_add_bounded_ab. ((((exists fom_beta_height_pfp_add_bounded_ab_entry. fom_beta_height_pfp_add_bounded_ab_entry + S (fom_value_pfp_add_bounded_ab) = S ((S (fom_index_pfp_add_bounded_ab)) * ac)) /\ exists fom_beta_quotient_pfp_add_bounded_ab_entry. ab = fom_beta_quotient_pfp_add_bounded_ab_entry * S ((S (fom_index_pfp_add_bounded_ab)) * ac) + (fom_value_pfp_add_bounded_ab))) /\ (exists fom_gap_pfp_add_bounded_ab_value_bound. fom_gap_pfp_add_bounded_ab_value_bound + S (fom_value_pfp_add_bounded_ab) = p))) /\ (((forall fom_index_pfp_add_bounded_bb. (exists fom_gap_pfp_add_bounded_bb_index_bound. fom_gap_pfp_add_bounded_bb_index_bound + S (fom_index_pfp_add_bounded_bb) = l) -> exists fom_value_pfp_add_bounded_bb. ((((exists fom_beta_height_pfp_add_bounded_bb_entry. fom_beta_height_pfp_add_bounded_bb_entry + S (fom_value_pfp_add_bounded_bb) = S ((S (fom_index_pfp_add_bounded_bb)) * bc)) /\ exists fom_beta_quotient_pfp_add_bounded_bb_entry. bb = fom_beta_quotient_pfp_add_bounded_bb_entry * S ((S (fom_index_pfp_add_bounded_bb)) * bc) + (fom_value_pfp_add_bounded_bb))) /\ (exists fom_gap_pfp_add_bounded_bb_value_bound. fom_gap_pfp_add_bounded_bb_value_bound + S (fom_value_pfp_add_bounded_bb) = p))) /\ ((forall fom_index_pfp_add_bounded_cb. (exists fom_gap_pfp_add_bounded_cb_index_bound. fom_gap_pfp_add_bounded_cb_index_bound + S (fom_index_pfp_add_bounded_cb) = l) -> exists fom_value_pfp_add_bounded_cb. ((((exists fom_beta_height_pfp_add_bounded_cb_entry. fom_beta_height_pfp_add_bounded_cb_entry + S (fom_value_pfp_add_bounded_cb) = S ((S (fom_index_pfp_add_bounded_cb)) * cc)) /\ exists fom_beta_quotient_pfp_add_bounded_cb_entry. cb = fom_beta_quotient_pfp_add_bounded_cb_entry * S ((S (fom_index_pfp_add_bounded_cb)) * cc) + (fom_value_pfp_add_bounded_cb))) /\ (exists fom_gap_pfp_add_bounded_cb_value_bound. fom_gap_pfp_add_bounded_cb_value_bound + S (fom_value_pfp_add_bounded_cb) = p)))))))

Constructive proof overview

Generated structural guide

All three prefixes in an actual polynomial addition consist of canonical coefficients.

The unchanged tactic script uses 0 declared prerequisites and contains 68 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

none

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

68 script commands · 21 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.

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–9

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 h
02Separate the logical casesL10–10

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

  1. L10
    split
03Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
04Establish 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. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(cb,cc,i,r) ∧ FpAdd(p,a,b,r)))Definitions: FpAddBetaAt
  2. L14
    specialize h (i)
  3. L15
    apply h
  4. L16
    exact hi
05Separate the logical casesL17–25

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_witness
  5. L21
    cases hv_witness_witness_witness_right
  6. L22
    cases hv_witness_witness_witness_right_right
  7. L23
    cases hv_witness_witness_witness_right_right_right
  8. L24
    cases hv_witness_witness_witness_right_right_right_right
  9. L25
    cases hv_witness_witness_witness_right_right_right_right_right
06Construct an explicit witnessL26–26

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

  1. L26
    exists x
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–29

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

  1. L28
    exact hv_witness_witness_witness_left
  2. L29
    exact hv_witness_witness_witness_right_right_right_left
09Separate the logical casesL30–30

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

  1. L30
    split
10Fix variables and assumptionsL31–32

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

  1. L31
    intro i
  2. L32
    intro hi
11Establish hvL33–36

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

  1. L33
    have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(cb,cc,i,r) ∧ FpAdd(p,a,b,r)))Definitions: FpAddBetaAt
  2. L34
    specialize h (i)
  3. L35
    apply h
  4. L36
    exact hi
12Separate the logical casesL37–45

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

  1. L37
    cases hv
  2. L38
    cases hv_witness
  3. L39
    cases hv_witness_witness
  4. L40
    cases hv_witness_witness_witness
  5. L41
    cases hv_witness_witness_witness_right
  6. L42
    cases hv_witness_witness_witness_right_right
  7. L43
    cases hv_witness_witness_witness_right_right_right
  8. L44
    cases hv_witness_witness_witness_right_right_right_right
  9. L45
    cases hv_witness_witness_witness_right_right_right_right_right
13Construct an explicit witnessL46–46

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

  1. L46
    exists x1
14Separate the logical casesL47–47

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

  1. L47
    split
15Use earlier factsL48–49

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

  1. L48
    exact hv_witness_witness_witness_right_left
  2. L49
    exact hv_witness_witness_witness_right_right_right_right_left
16Fix variables and assumptionsL50–51

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

  1. L50
    intro i
  2. L51
    intro hi
17Establish hvL52–55

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

  1. L52
    have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(cb,cc,i,r) ∧ FpAdd(p,a,b,r)))Definitions: FpAddBetaAt
  2. L53
    specialize h (i)
  3. L54
    apply h
  4. L55
    exact hi
18Separate the logical casesL56–64

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

  1. L56
    cases hv
  2. L57
    cases hv_witness
  3. L58
    cases hv_witness_witness
  4. L59
    cases hv_witness_witness_witness
  5. L60
    cases hv_witness_witness_witness_right
  6. L61
    cases hv_witness_witness_witness_right_right
  7. L62
    cases hv_witness_witness_witness_right_right_right
  8. L63
    cases hv_witness_witness_witness_right_right_right_right
  9. L64
    cases hv_witness_witness_witness_right_right_right_right_right
19Construct an explicit witnessL65–65

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

  1. L65
    exists x2
20Separate the logical casesL66–66

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

  1. L66
    split
21Use earlier factsL67–68

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

  1. L67
    exact hv_witness_witness_witness_right_right_left
  2. L68
    exact hv_witness_witness_witness_right_right_right_right_right_left

Library-wide reading audit

Original exact command ledger · 68 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 h
  10. 0010split
  11. 0011intro i
  12. 0012intro hi
  13. 0013have hv : exists a b r. ((((exists ff_h_pfp_add_bound_left. ff_h_pfp_add_bound_left + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_bound_left. ab = ff_q_pfp_add_bound_left * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_add_bound_right. ff_h_pfp_add_bound_right + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_bound_right. bb = ff_q_pfp_add_bound_right * S ((S (i)) * bc) + (b))) /\ (((((exists ff_h_pfp_add_bound_target. ff_h_pfp_add_bound_target + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_add_bound_target. cb = ff_q_pfp_add_bound_target * S ((S (i)) * cc) + (r))) /\ ((((exists pfa_gap_add_bound_operationleft. pfa_gap_add_bound_operationleft + S (a) = (p)) /\ (((exists pfa_gap_add_bound_operationright. pfa_gap_add_bound_operationright + S (b) = (p)) /\ ((((exists pfa_gap_add_bound_operationresultbound. pfa_gap_add_bound_operationresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_add_bound_operationresultcongruence pfa_offset_right_add_bound_operationresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_add_bound_operationresultcongruence = (r) + (p) * pfa_offset_right_add_bound_operationresultcongruence)))))))))))))))
  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_witness
  21. 0021cases hv_witness_witness_witness_right
  22. 0022cases hv_witness_witness_witness_right_right
  23. 0023cases hv_witness_witness_witness_right_right_right
  24. 0024cases hv_witness_witness_witness_right_right_right_right
  25. 0025cases hv_witness_witness_witness_right_right_right_right_right
  26. 0026exists x
  27. 0027split
  28. 0028exact hv_witness_witness_witness_left
  29. 0029exact hv_witness_witness_witness_right_right_right_left
  30. 0030split
  31. 0031intro i
  32. 0032intro hi
  33. 0033have hv : exists a b r. ((((exists ff_h_pfp_add_bound_left. ff_h_pfp_add_bound_left + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_bound_left. ab = ff_q_pfp_add_bound_left * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_add_bound_right. ff_h_pfp_add_bound_right + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_bound_right. bb = ff_q_pfp_add_bound_right * S ((S (i)) * bc) + (b))) /\ (((((exists ff_h_pfp_add_bound_target. ff_h_pfp_add_bound_target + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_add_bound_target. cb = ff_q_pfp_add_bound_target * S ((S (i)) * cc) + (r))) /\ ((((exists pfa_gap_add_bound_operationleft. pfa_gap_add_bound_operationleft + S (a) = (p)) /\ (((exists pfa_gap_add_bound_operationright. pfa_gap_add_bound_operationright + S (b) = (p)) /\ ((((exists pfa_gap_add_bound_operationresultbound. pfa_gap_add_bound_operationresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_add_bound_operationresultcongruence pfa_offset_right_add_bound_operationresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_add_bound_operationresultcongruence = (r) + (p) * pfa_offset_right_add_bound_operationresultcongruence)))))))))))))))
  34. 0034specialize h (i)
  35. 0035apply h
  36. 0036exact hi
  37. 0037cases hv
  38. 0038cases hv_witness
  39. 0039cases hv_witness_witness
  40. 0040cases hv_witness_witness_witness
  41. 0041cases hv_witness_witness_witness_right
  42. 0042cases hv_witness_witness_witness_right_right
  43. 0043cases hv_witness_witness_witness_right_right_right
  44. 0044cases hv_witness_witness_witness_right_right_right_right
  45. 0045cases hv_witness_witness_witness_right_right_right_right_right
  46. 0046exists x1
  47. 0047split
  48. 0048exact hv_witness_witness_witness_right_left
  49. 0049exact hv_witness_witness_witness_right_right_right_right_left
  50. 0050intro i
  51. 0051intro hi
  52. 0052have hv : exists a b r. ((((exists ff_h_pfp_add_bound_left. ff_h_pfp_add_bound_left + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_bound_left. ab = ff_q_pfp_add_bound_left * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_add_bound_right. ff_h_pfp_add_bound_right + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_bound_right. bb = ff_q_pfp_add_bound_right * S ((S (i)) * bc) + (b))) /\ (((((exists ff_h_pfp_add_bound_target. ff_h_pfp_add_bound_target + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_add_bound_target. cb = ff_q_pfp_add_bound_target * S ((S (i)) * cc) + (r))) /\ ((((exists pfa_gap_add_bound_operationleft. pfa_gap_add_bound_operationleft + S (a) = (p)) /\ (((exists pfa_gap_add_bound_operationright. pfa_gap_add_bound_operationright + S (b) = (p)) /\ ((((exists pfa_gap_add_bound_operationresultbound. pfa_gap_add_bound_operationresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_add_bound_operationresultcongruence pfa_offset_right_add_bound_operationresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_add_bound_operationresultcongruence = (r) + (p) * pfa_offset_right_add_bound_operationresultcongruence)))))))))))))))
  53. 0053specialize h (i)
  54. 0054apply h
  55. 0055exact hi
  56. 0056cases hv
  57. 0057cases hv_witness
  58. 0058cases hv_witness_witness
  59. 0059cases hv_witness_witness_witness
  60. 0060cases hv_witness_witness_witness_right
  61. 0061cases hv_witness_witness_witness_right_right
  62. 0062cases hv_witness_witness_witness_right_right_right
  63. 0063cases hv_witness_witness_witness_right_right_right_right
  64. 0064cases hv_witness_witness_witness_right_right_right_right_right
  65. 0065exists x2
  66. 0066split
  67. 0067exact hv_witness_witness_witness_right_right_left
  68. 0068exact hv_witness_witness_witness_right_right_right_right_right_left