PP000D

prime_field_polynomial_add_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 44 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_pointwise_add_prefix_exists Alpha theorem; checked-use authorized PP0002 prime_field_polynomial_normalization_exists PP000C prime_field_polynomial_add_from_normalization

Direct dependents

none

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

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.

Named ingredients (2)
prime field polynomial normalization existsprime field polynomial add from normalization

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 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: LtBetaAt
  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
  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 exact 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 : exists rb rc. (forall ff_index_mcp_add_pfp_add_exists_raw ff_left_mcp_add_pfp_add_exists_raw ff_right_mcp_add_pfp_add_exists_raw ff_target_mcp_add_pfp_add_exists_raw. (exists mcp_gap_pfp_add_exists_raw_bound. mcp_gap_pfp_add_exists_raw_bound + S (ff_index_mcp_add_pfp_add_exists_raw) = (l)) -> (((exists fs_h_mcp_pfp_add_exists_raw_left. fs_h_mcp_pfp_add_exists_raw_left + S (ff_left_mcp_add_pfp_add_exists_raw) = S ((S (ff_index_mcp_add_pfp_add_exists_raw)) * ac)) /\ exists fs_q_mcp_pfp_add_exists_raw_left. ab = fs_q_mcp_pfp_add_exists_raw_left * S ((S (ff_index_mcp_add_pfp_add_exists_raw)) * ac) + (ff_left_mcp_add_pfp_add_exists_raw))) -> (((exists fs_h_mcp_pfp_add_exists_raw_right. fs_h_mcp_pfp_add_exists_raw_right + S (ff_right_mcp_add_pfp_add_exists_raw) = S ((S (ff_index_mcp_add_pfp_add_exists_raw)) * bc)) /\ exists fs_q_mcp_pfp_add_exists_raw_right. bb = fs_q_mcp_pfp_add_exists_raw_right * S ((S (ff_index_mcp_add_pfp_add_exists_raw)) * bc) + (ff_right_mcp_add_pfp_add_exists_raw))) -> (((exists fs_h_mcp_pfp_add_exists_raw_target. fs_h_mcp_pfp_add_exists_raw_target + S (ff_target_mcp_add_pfp_add_exists_raw) = S ((S (ff_index_mcp_add_pfp_add_exists_raw)) * rc)) /\ exists fs_q_mcp_pfp_add_exists_raw_target. rb = fs_q_mcp_pfp_add_exists_raw_target * S ((S (ff_index_mcp_add_pfp_add_exists_raw)) * rc) + (ff_target_mcp_add_pfp_add_exists_raw))) -> ff_target_mcp_add_pfp_add_exists_raw = ff_left_mcp_add_pfp_add_exists_raw + ff_right_mcp_add_pfp_add_exists_raw)
  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 : exists cb cc. (forall pfp_index_add_exists_normalization. (exists pfa_gap_add_exists_normalizationindex. pfa_gap_add_exists_normalizationindex + S (pfp_index_add_exists_normalization) = (l)) -> exists pfp_source_add_exists_normalization pfp_residue_add_exists_normalization. ((((exists ff_h_pfp_add_exists_normalizationsource. ff_h_pfp_add_exists_normalizationsource + S (pfp_source_add_exists_normalization) = S ((S (pfp_index_add_exists_normalization)) * x1)) /\ exists ff_q_pfp_add_exists_normalizationsource. x = ff_q_pfp_add_exists_normalizationsource * S ((S (pfp_index_add_exists_normalization)) * x1) + (pfp_source_add_exists_normalization))) /\ (((((exists ff_h_pfp_add_exists_normalizationtarget. ff_h_pfp_add_exists_normalizationtarget + S (pfp_residue_add_exists_normalization) = S ((S (pfp_index_add_exists_normalization)) * cc)) /\ exists ff_q_pfp_add_exists_normalizationtarget. cb = ff_q_pfp_add_exists_normalizationtarget * S ((S (pfp_index_add_exists_normalization)) * cc) + (pfp_residue_add_exists_normalization))) /\ ((((exists pfa_gap_add_exists_normalizationresiduebound. pfa_gap_add_exists_normalizationresiduebound + S (pfp_residue_add_exists_normalization) = (p)) /\ ((exists pfa_offset_left_add_exists_normalizationresiduecongruence pfa_offset_right_add_exists_normalizationresiduecongruence. (pfp_source_add_exists_normalization) + (p) * pfa_offset_left_add_exists_normalizationresiduecongruence = (pfp_residue_add_exists_normalization) + (p) * pfa_offset_right_add_exists_normalizationresiduecongruence)))))))))
  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