PP000C

prime_field_polynomial_add_from_normalization

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

Normalize a genuine natural pointwise sum to obtain actual canonical field sums at every coefficient.

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 cb cc l. (forall fom_index_pfp_add_source_a. (exists fom_gap_pfp_add_source_a_index_bound. fom_gap_pfp_add_source_a_index_bound + S (fom_index_pfp_add_source_a) = l) -> exists fom_value_pfp_add_source_a. ((((exists fom_beta_height_pfp_add_source_a_entry. fom_beta_height_pfp_add_source_a_entry + S (fom_value_pfp_add_source_a) = S ((S (fom_index_pfp_add_source_a)) * ac)) /\ exists fom_beta_quotient_pfp_add_source_a_entry. ab = fom_beta_quotient_pfp_add_source_a_entry * S ((S (fom_index_pfp_add_source_a)) * ac) + (fom_value_pfp_add_source_a))) /\ (exists fom_gap_pfp_add_source_a_value_bound. fom_gap_pfp_add_source_a_value_bound + S (fom_value_pfp_add_source_a) = p))) -> (forall fom_index_pfp_add_source_b. (exists fom_gap_pfp_add_source_b_index_bound. fom_gap_pfp_add_source_b_index_bound + S (fom_index_pfp_add_source_b) = l) -> exists fom_value_pfp_add_source_b. ((((exists fom_beta_height_pfp_add_source_b_entry. fom_beta_height_pfp_add_source_b_entry + S (fom_value_pfp_add_source_b) = S ((S (fom_index_pfp_add_source_b)) * bc)) /\ exists fom_beta_quotient_pfp_add_source_b_entry. bb = fom_beta_quotient_pfp_add_source_b_entry * S ((S (fom_index_pfp_add_source_b)) * bc) + (fom_value_pfp_add_source_b))) /\ (exists fom_gap_pfp_add_source_b_value_bound. fom_gap_pfp_add_source_b_value_bound + S (fom_value_pfp_add_source_b) = p))) -> (forall ff_index_mcp_add_pfp_add_raw ff_left_mcp_add_pfp_add_raw ff_right_mcp_add_pfp_add_raw ff_target_mcp_add_pfp_add_raw. (exists mcp_gap_pfp_add_raw_bound. mcp_gap_pfp_add_raw_bound + S (ff_index_mcp_add_pfp_add_raw) = (l)) -> (((exists fs_h_mcp_pfp_add_raw_left. fs_h_mcp_pfp_add_raw_left + S (ff_left_mcp_add_pfp_add_raw) = S ((S (ff_index_mcp_add_pfp_add_raw)) * ac)) /\ exists fs_q_mcp_pfp_add_raw_left. ab = fs_q_mcp_pfp_add_raw_left * S ((S (ff_index_mcp_add_pfp_add_raw)) * ac) + (ff_left_mcp_add_pfp_add_raw))) -> (((exists fs_h_mcp_pfp_add_raw_right. fs_h_mcp_pfp_add_raw_right + S (ff_right_mcp_add_pfp_add_raw) = S ((S (ff_index_mcp_add_pfp_add_raw)) * bc)) /\ exists fs_q_mcp_pfp_add_raw_right. bb = fs_q_mcp_pfp_add_raw_right * S ((S (ff_index_mcp_add_pfp_add_raw)) * bc) + (ff_right_mcp_add_pfp_add_raw))) -> (((exists fs_h_mcp_pfp_add_raw_target. fs_h_mcp_pfp_add_raw_target + S (ff_target_mcp_add_pfp_add_raw) = S ((S (ff_index_mcp_add_pfp_add_raw)) * rc)) /\ exists fs_q_mcp_pfp_add_raw_target. rb = fs_q_mcp_pfp_add_raw_target * S ((S (ff_index_mcp_add_pfp_add_raw)) * rc) + (ff_target_mcp_add_pfp_add_raw))) -> ff_target_mcp_add_pfp_add_raw = ff_left_mcp_add_pfp_add_raw + ff_right_mcp_add_pfp_add_raw) -> (forall pfp_index_add_normalize. (exists pfa_gap_add_normalizeindex. pfa_gap_add_normalizeindex + S (pfp_index_add_normalize) = (l)) -> exists pfp_source_add_normalize pfp_residue_add_normalize. ((((exists ff_h_pfp_add_normalizesource. ff_h_pfp_add_normalizesource + S (pfp_source_add_normalize) = S ((S (pfp_index_add_normalize)) * rc)) /\ exists ff_q_pfp_add_normalizesource. rb = ff_q_pfp_add_normalizesource * S ((S (pfp_index_add_normalize)) * rc) + (pfp_source_add_normalize))) /\ (((((exists ff_h_pfp_add_normalizetarget. ff_h_pfp_add_normalizetarget + S (pfp_residue_add_normalize) = S ((S (pfp_index_add_normalize)) * cc)) /\ exists ff_q_pfp_add_normalizetarget. cb = ff_q_pfp_add_normalizetarget * S ((S (pfp_index_add_normalize)) * cc) + (pfp_residue_add_normalize))) /\ ((((exists pfa_gap_add_normalizeresiduebound. pfa_gap_add_normalizeresiduebound + S (pfp_residue_add_normalize) = (p)) /\ ((exists pfa_offset_left_add_normalizeresiduecongruence pfa_offset_right_add_normalizeresiduecongruence. (pfp_source_add_normalize) + (p) * pfa_offset_left_add_normalizeresiduecongruence = (pfp_residue_add_normalize) + (p) * pfa_offset_right_add_normalizeresiduecongruence))))))))) -> (forall pfp_index_add_result. (exists pfa_gap_add_resultindex. pfa_gap_add_resultindex + S (pfp_index_add_result) = (l)) -> exists pfp_left_add_result pfp_right_add_result pfp_value_add_result. ((((exists ff_h_pfp_add_resultleft. ff_h_pfp_add_resultleft + S (pfp_left_add_result) = S ((S (pfp_index_add_result)) * ac)) /\ exists ff_q_pfp_add_resultleft. ab = ff_q_pfp_add_resultleft * S ((S (pfp_index_add_result)) * ac) + (pfp_left_add_result))) /\ (((((exists ff_h_pfp_add_resultright. ff_h_pfp_add_resultright + S (pfp_right_add_result) = S ((S (pfp_index_add_result)) * bc)) /\ exists ff_q_pfp_add_resultright. bb = ff_q_pfp_add_resultright * S ((S (pfp_index_add_result)) * bc) + (pfp_right_add_result))) /\ (((((exists ff_h_pfp_add_resulttarget. ff_h_pfp_add_resulttarget + S (pfp_value_add_result) = S ((S (pfp_index_add_result)) * cc)) /\ exists ff_q_pfp_add_resulttarget. cb = ff_q_pfp_add_resulttarget * S ((S (pfp_index_add_result)) * cc) + (pfp_value_add_result))) /\ ((((exists pfa_gap_add_resultoperationleft. pfa_gap_add_resultoperationleft + S (pfp_left_add_result) = (p)) /\ (((exists pfa_gap_add_resultoperationright. pfa_gap_add_resultoperationright + S (pfp_right_add_result) = (p)) /\ ((((exists pfa_gap_add_resultoperationresultbound. pfa_gap_add_resultoperationresultbound + S (pfp_value_add_result) = (p)) /\ ((exists pfa_offset_left_add_resultoperationresultcongruence pfa_offset_right_add_resultoperationresultcongruence. ((pfp_left_add_result) + (pfp_right_add_result)) + (p) * pfa_offset_left_add_resultoperationresultcongruence = (pfp_value_add_result) + (p) * pfa_offset_right_add_resultoperationresultcongruence))))))))))))))))

Constructive proof overview

Generated structural guide

Normalize a genuine natural pointwise sum to obtain actual canonical field sums at every coefficient.

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

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

Proof neighborhood

Direct dependencies

prime_field_residue_input_equal Alpha theorem; checked-use authorized

Direct dependents

PP000D prime_field_polynomial_add_exists

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

65 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–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 cb
  9. L9
    intro cc
  10. L10
    intro l
02Fix variables and assumptionsL11–16

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

  1. L11
    intro ha
  2. L12
    intro hb
  3. L13
    intro hs
  4. L14
    intro hn
  5. L15
    intro i
  6. L16
    intro hi
03Establish hvaL17–20

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

  1. L17
    have hva : exists a. ((((exists ff_h_pfp_add_chosen_a. ff_h_pfp_add_chosen_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_chosen_a. ab = ff_q_pfp_add_chosen_a * S ((S (i)) * ac) + (a))) /\ ((exists pfa_gap_add_chosen_a_bound. pfa_gap_add_chosen_a_bound + S (a) = (p))))
  2. L18
    specialize ha (i)
  3. L19
    apply ha
  4. L20
    exact hi
04Separate the logical casesL21–22

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

  1. L21
    cases hva
  2. L22
    cases hva_witness
05Establish hvbL23–26

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

  1. L23
    have hvb : exists b. ((((exists ff_h_pfp_add_chosen_b. ff_h_pfp_add_chosen_b + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_chosen_b. bb = ff_q_pfp_add_chosen_b * S ((S (i)) * bc) + (b))) /\ ((exists pfa_gap_add_chosen_b_bound. pfa_gap_add_chosen_b_bound + S (b) = (p))))
  2. L24
    specialize hb (i)
  3. L25
    apply hb
  4. L26
    exact hi
06Separate the logical casesL27–28

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

  1. L27
    cases hvb
  2. L28
    cases hvb_witness
07Establish hvnL29–32

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

  1. L29
    have hvn : ∃ s. ∃ r. BetaAt(rb,rc,i,s) ∧ (BetaAt(cb,cc,i,r) ∧ CanonicalModularResidue(p,s,r))Definitions: CanonicalModularResidueBetaAt
  2. L30
    specialize hn (i)
  3. L31
    apply hn
  4. L32
    exact hi
08Separate the logical casesL33–36

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

  1. L33
    cases hvn
  2. L34
    cases hvn_witness
  3. L35
    cases hvn_witness_witness
  4. L36
    cases hvn_witness_witness_right
09Construct an explicit witnessL37–39

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

  1. L37
    exists x
  2. L38
    exists x1
  3. L39
    exists x3
10Separate the logical casesL40–40

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

  1. L40
    split
11Use earlier factsL41–41

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

  1. L41
    exact hva_witness_left
12Separate the logical casesL42–42

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

  1. L42
    split
13Use earlier factsL43–43

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

  1. L43
    exact hvb_witness_left
14Separate the logical casesL44–44

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

  1. L44
    split
15Use earlier factsL45–45

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

  1. L45
    exact hvn_witness_witness_right_left
16Separate the logical casesL46–46

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

  1. L46
    split
17Use earlier factsL47–47

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

  1. L47
    exact hva_witness_right
18Separate the logical casesL48–48

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

  1. L48
    split
19Use earlier factsL49–54

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

  1. L49
    exact hvb_witness_right
  2. L50
    specialize prime_field_residue_input_equal (p)
  3. L51
    specialize prime_field_residue_input_equal (x+x1)
  4. L52
    specialize prime_field_residue_input_equal (x2)
  5. L53
    specialize prime_field_residue_input_equal (x3)
  6. L54
    apply prime_field_residue_input_equal
20Calculate and transport equalitiesL55–55

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

  1. L55
    symm
21Use earlier factsL56–65

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

  1. L56
    specialize hs (i)
  2. L57
    specialize hs (x)
  3. L58
    specialize hs (x1)
  4. L59
    specialize hs (x2)
  5. L60
    apply hs
  6. L61
    exact hi
  7. L62
    exact hva_witness_left
  8. L63
    exact hvb_witness_left
  9. L64
    exact hvn_witness_witness_left
  10. L65
    exact hvn_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 65 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro l
  11. 0011intro ha
  12. 0012intro hb
  13. 0013intro hs
  14. 0014intro hn
  15. 0015intro i
  16. 0016intro hi
  17. 0017have hva : exists a. ((((exists ff_h_pfp_add_chosen_a. ff_h_pfp_add_chosen_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_add_chosen_a. ab = ff_q_pfp_add_chosen_a * S ((S (i)) * ac) + (a))) /\ ((exists pfa_gap_add_chosen_a_bound. pfa_gap_add_chosen_a_bound + S (a) = (p))))
  18. 0018specialize ha (i)
  19. 0019apply ha
  20. 0020exact hi
  21. 0021cases hva
  22. 0022cases hva_witness
  23. 0023have hvb : exists b. ((((exists ff_h_pfp_add_chosen_b. ff_h_pfp_add_chosen_b + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_add_chosen_b. bb = ff_q_pfp_add_chosen_b * S ((S (i)) * bc) + (b))) /\ ((exists pfa_gap_add_chosen_b_bound. pfa_gap_add_chosen_b_bound + S (b) = (p))))
  24. 0024specialize hb (i)
  25. 0025apply hb
  26. 0026exact hi
  27. 0027cases hvb
  28. 0028cases hvb_witness
  29. 0029have hvn : exists s r. ((((exists ff_h_pfp_add_chosen_sum. ff_h_pfp_add_chosen_sum + S (s) = S ((S (i)) * rc)) /\ exists ff_q_pfp_add_chosen_sum. rb = ff_q_pfp_add_chosen_sum * S ((S (i)) * rc) + (s))) /\ (((((exists ff_h_pfp_add_chosen_residue. ff_h_pfp_add_chosen_residue + S (r) = S ((S (i)) * cc)) /\ exists ff_q_pfp_add_chosen_residue. cb = ff_q_pfp_add_chosen_residue * S ((S (i)) * cc) + (r))) /\ ((((exists pfa_gap_add_chosen_reductionbound. pfa_gap_add_chosen_reductionbound + S (r) = (p)) /\ ((exists pfa_offset_left_add_chosen_reductioncongruence pfa_offset_right_add_chosen_reductioncongruence. (s) + (p) * pfa_offset_left_add_chosen_reductioncongruence = (r) + (p) * pfa_offset_right_add_chosen_reductioncongruence))))))))
  30. 0030specialize hn (i)
  31. 0031apply hn
  32. 0032exact hi
  33. 0033cases hvn
  34. 0034cases hvn_witness
  35. 0035cases hvn_witness_witness
  36. 0036cases hvn_witness_witness_right
  37. 0037exists x
  38. 0038exists x1
  39. 0039exists x3
  40. 0040split
  41. 0041exact hva_witness_left
  42. 0042split
  43. 0043exact hvb_witness_left
  44. 0044split
  45. 0045exact hvn_witness_witness_right_left
  46. 0046split
  47. 0047exact hva_witness_right
  48. 0048split
  49. 0049exact hvb_witness_right
  50. 0050specialize prime_field_residue_input_equal (p)
  51. 0051specialize prime_field_residue_input_equal (x+x1)
  52. 0052specialize prime_field_residue_input_equal (x2)
  53. 0053specialize prime_field_residue_input_equal (x3)
  54. 0054apply prime_field_residue_input_equal
  55. 0055symm
  56. 0056specialize hs (i)
  57. 0057specialize hs (x)
  58. 0058specialize hs (x1)
  59. 0059specialize hs (x2)
  60. 0060apply hs
  61. 0061exact hi
  62. 0062exact hva_witness_left
  63. 0063exact hvb_witness_left
  64. 0064exact hvn_witness_witness_left
  65. 0065exact hvn_witness_witness_right_right