PP000D

prime_field_polynomial_add_exists

Construct the actual finite canonical coefficient sum, without supplying a table or an addition-law premise.

Alpha v34 checked-use · first admitted v31 · 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.

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ l. ¬p = 0 → BetaPrefixInto(ab,ac,l,p) → BetaPrefixInto(bb,bc,l,p) → ∃ x. ∃ y. FpPolyAdd(p,ab,ac,bb,bc,x,y,l)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2FpCoefficientReduction(p,b,c,d,e,l) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_pointwise_add_prefix_exists · checked external prerequisiteprime_field_polynomial_normalization_existsprime_field_polynomial_add_from_normalization
Original expanded first-order statement 
forall p ab ac bb bc l. ~(p=0) -> (forall fom_index_pfp_add_exists_a. (exists fom_gap_pfp_add_exists_a_index_bound. fom_gap_pfp_add_exists_a_index_bound + S (fom_index_pfp_add_exists_a) = l) -> exists fom_value_pfp_add_exists_a. ((((exists fom_beta_height_pfp_add_exists_a_entry. fom_beta_height_pfp_add_exists_a_entry + S (fom_value_pfp_add_exists_a) = S ((S (fom_index_pfp_add_exists_a)) * ac)) /\ exists fom_beta_quotient_pfp_add_exists_a_entry. ab = fom_beta_quotient_pfp_add_exists_a_entry * S ((S (fom_index_pfp_add_exists_a)) * ac) + (fom_value_pfp_add_exists_a))) /\ (exists fom_gap_pfp_add_exists_a_value_bound. fom_gap_pfp_add_exists_a_value_bound + S (fom_value_pfp_add_exists_a) = p))) -> (forall fom_index_pfp_add_exists_b. (exists fom_gap_pfp_add_exists_b_index_bound. fom_gap_pfp_add_exists_b_index_bound + S (fom_index_pfp_add_exists_b) = l) -> exists fom_value_pfp_add_exists_b. ((((exists fom_beta_height_pfp_add_exists_b_entry. fom_beta_height_pfp_add_exists_b_entry + S (fom_value_pfp_add_exists_b) = S ((S (fom_index_pfp_add_exists_b)) * bc)) /\ exists fom_beta_quotient_pfp_add_exists_b_entry. bb = fom_beta_quotient_pfp_add_exists_b_entry * S ((S (fom_index_pfp_add_exists_b)) * bc) + (fom_value_pfp_add_exists_b))) /\ (exists fom_gap_pfp_add_exists_b_value_bound. fom_gap_pfp_add_exists_b_value_bound + S (fom_value_pfp_add_exists_b) = p))) -> exists cb cc. (forall pfp_index_add_exists_result. (exists pfa_gap_add_exists_resultindex. pfa_gap_add_exists_resultindex + S (pfp_index_add_exists_result) = (l)) -> exists pfp_left_add_exists_result pfp_right_add_exists_result pfp_value_add_exists_result. ((((exists ff_h_pfp_add_exists_resultleft. ff_h_pfp_add_exists_resultleft + S (pfp_left_add_exists_result) = S ((S (pfp_index_add_exists_result)) * ac)) /\ exists ff_q_pfp_add_exists_resultleft. ab = ff_q_pfp_add_exists_resultleft * S ((S (pfp_index_add_exists_result)) * ac) + (pfp_left_add_exists_result))) /\ (((((exists ff_h_pfp_add_exists_resultright. ff_h_pfp_add_exists_resultright + S (pfp_right_add_exists_result) = S ((S (pfp_index_add_exists_result)) * bc)) /\ exists ff_q_pfp_add_exists_resultright. bb = ff_q_pfp_add_exists_resultright * S ((S (pfp_index_add_exists_result)) * bc) + (pfp_right_add_exists_result))) /\ (((((exists ff_h_pfp_add_exists_resulttarget. ff_h_pfp_add_exists_resulttarget + S (pfp_value_add_exists_result) = S ((S (pfp_index_add_exists_result)) * cc)) /\ exists ff_q_pfp_add_exists_resulttarget. cb = ff_q_pfp_add_exists_resulttarget * S ((S (pfp_index_add_exists_result)) * cc) + (pfp_value_add_exists_result))) /\ ((((exists pfa_gap_add_exists_resultoperationleft. pfa_gap_add_exists_resultoperationleft + S (pfp_left_add_exists_result) = (p)) /\ (((exists pfa_gap_add_exists_resultoperationright. pfa_gap_add_exists_resultoperationright + S (pfp_right_add_exists_result) = (p)) /\ ((((exists pfa_gap_add_exists_resultoperationresultbound. pfa_gap_add_exists_resultoperationresultbound + S (pfp_value_add_exists_result) = (p)) /\ ((exists pfa_offset_left_add_exists_resultoperationresultcongruence pfa_offset_right_add_exists_resultoperationresultcongruence. ((pfp_left_add_exists_result) + (pfp_right_add_exists_result)) + (p) * pfa_offset_left_add_exists_resultoperationresultcongruence = (pfp_value_add_exists_result) + (p) * pfa_offset_right_add_exists_resultoperationresultcongruence))))))))))))))))

Complete tactic proof in conservative notation

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

44 script commands · 8 reading checkpoints · 2 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.

Named ingredients (2)
prime field polynomial normalization existsprime field polynomial add from normalization
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 l
  7. L7
    intro hp
  8. L8
    intro ha
  9. L9
    intro hb
02Establish hsL10–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta pointwise add prefix exists.

  1. L10
    have hs : ∃ rb. ∃ rc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(ab,ac,x,y) → BetaAt(bb,bc,x,z) → BetaAt(rb,rc,x,n) → n = y + zDefinitions: Lt(x,l)BetaAt(ab,ac,x,y)BetaAt(bb,bc,x,z)BetaAt(rb,rc,x,n)Original native command in the exact edition
  2. L11
    specialize beta_pointwise_add_prefix_exists (ab)
  3. L12
    specialize beta_pointwise_add_prefix_exists (ac)
  4. L13
    specialize beta_pointwise_add_prefix_exists (bb)
  5. L14
    specialize beta_pointwise_add_prefix_exists (bc)
  6. L15
    specialize beta_pointwise_add_prefix_exists (l)
  7. L16
    apply beta_pointwise_add_prefix_exists
03Separate the logical casesL17–18

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

  1. L17
    cases hs
  2. L18
    cases hs_witness
04Establish hnL19–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial normalization exists.

  1. L19
    have hn : ∃ cb. ∃ cc. FpCoefficientReduction(p,x,x1,cb,cc,l)Definitions: FpCoefficientReduction(p,x,x1,cb,cc,l)Original native command in the exact edition
  2. L20
    specialize prime_field_polynomial_normalization_exists (p)
  3. L21
    specialize prime_field_polynomial_normalization_exists (x)
  4. L22
    specialize prime_field_polynomial_normalization_exists (x1)
  5. L23
    specialize prime_field_polynomial_normalization_exists (l)
  6. L24
    apply prime_field_polynomial_normalization_exists
  7. L25
    exact hp
05Separate the logical casesL26–27

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

  1. L26
    cases hn
  2. L27
    cases hn_witness
06Construct an explicit witnessL28–29

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

  1. L28
    exists x2
  2. L29
    exists x3
07Use earlier factsL30–39

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

  1. L30
    specialize prime_field_polynomial_add_from_normalization (p)
  2. L31
    specialize prime_field_polynomial_add_from_normalization (ab)
  3. L32
    specialize prime_field_polynomial_add_from_normalization (ac)
  4. L33
    specialize prime_field_polynomial_add_from_normalization (bb)
  5. L34
    specialize prime_field_polynomial_add_from_normalization (bc)
  6. L35
    specialize prime_field_polynomial_add_from_normalization (x)
  7. L36
    specialize prime_field_polynomial_add_from_normalization (x1)
  8. L37
    specialize prime_field_polynomial_add_from_normalization (x2)
  9. L38
    specialize prime_field_polynomial_add_from_normalization (x3)
  10. L39
    specialize prime_field_polynomial_add_from_normalization (l)
08Use earlier factsL40–44

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

  1. L40
    apply prime_field_polynomial_add_from_normalization
  2. L41
    exact ha
  3. L42
    exact hb
  4. L43
    exact hs_witness_witness
  5. L44
    exact hn_witness_witness

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro l
  7. 0007intro hp
  8. 0008intro ha
  9. 0009intro hb
  10. 0010have hs : ∃ rb. ∃ rc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(ab,ac,x,y) → BetaAt(bb,bc,x,z) → BetaAt(rb,rc,x,n) → n = y + z
  11. 0011specialize beta_pointwise_add_prefix_exists (ab)
  12. 0012specialize beta_pointwise_add_prefix_exists (ac)
  13. 0013specialize beta_pointwise_add_prefix_exists (bb)
  14. 0014specialize beta_pointwise_add_prefix_exists (bc)
  15. 0015specialize beta_pointwise_add_prefix_exists (l)
  16. 0016apply beta_pointwise_add_prefix_exists
  17. 0017cases hs
  18. 0018cases hs_witness
  19. 0019have hn : ∃ cb. ∃ cc. FpCoefficientReduction(p,x,x1,cb,cc,l)
  20. 0020specialize prime_field_polynomial_normalization_exists (p)
  21. 0021specialize prime_field_polynomial_normalization_exists (x)
  22. 0022specialize prime_field_polynomial_normalization_exists (x1)
  23. 0023specialize prime_field_polynomial_normalization_exists (l)
  24. 0024apply prime_field_polynomial_normalization_exists
  25. 0025exact hp
  26. 0026cases hn
  27. 0027cases hn_witness
  28. 0028exists x2
  29. 0029exists x3
  30. 0030specialize prime_field_polynomial_add_from_normalization (p)
  31. 0031specialize prime_field_polynomial_add_from_normalization (ab)
  32. 0032specialize prime_field_polynomial_add_from_normalization (ac)
  33. 0033specialize prime_field_polynomial_add_from_normalization (bb)
  34. 0034specialize prime_field_polynomial_add_from_normalization (bc)
  35. 0035specialize prime_field_polynomial_add_from_normalization (x)
  36. 0036specialize prime_field_polynomial_add_from_normalization (x1)
  37. 0037specialize prime_field_polynomial_add_from_normalization (x2)
  38. 0038specialize prime_field_polynomial_add_from_normalization (x3)
  39. 0039specialize prime_field_polynomial_add_from_normalization (l)
  40. 0040apply prime_field_polynomial_add_from_normalization
  41. 0041exact ha
  42. 0042exact hb
  43. 0043exact hs_witness_witness
  44. 0044exact hn_witness_witness