PG0042

prime_field_polynomial_aligned_add_exists

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

Construct a genuine canonical aligned sum at the explicit length L+M from any two canonical inputs, rather than assuming operation witnesses.

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 L bb bc M. (~((p) = 1) /\ forall pfa_factor_left_aligned_exists_prime pfa_factor_right_aligned_exists_prime. (p) = pfa_factor_left_aligned_exists_prime * pfa_factor_right_aligned_exists_prime -> pfa_factor_left_aligned_exists_prime = 1 \/ pfa_factor_right_aligned_exists_prime = 1) -> (forall fom_index_pfp_aligned_exists_A. (exists fom_gap_pfp_aligned_exists_A_index_bound. fom_gap_pfp_aligned_exists_A_index_bound + S (fom_index_pfp_aligned_exists_A) = L) -> exists fom_value_pfp_aligned_exists_A. ((((exists fom_beta_height_pfp_aligned_exists_A_entry. fom_beta_height_pfp_aligned_exists_A_entry + S (fom_value_pfp_aligned_exists_A) = S ((S (fom_index_pfp_aligned_exists_A)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_exists_A_entry. ab = fom_beta_quotient_pfp_aligned_exists_A_entry * S ((S (fom_index_pfp_aligned_exists_A)) * ac) + (fom_value_pfp_aligned_exists_A))) /\ (exists fom_gap_pfp_aligned_exists_A_value_bound. fom_gap_pfp_aligned_exists_A_value_bound + S (fom_value_pfp_aligned_exists_A) = p))) -> (forall fom_index_pfp_aligned_exists_B. (exists fom_gap_pfp_aligned_exists_B_index_bound. fom_gap_pfp_aligned_exists_B_index_bound + S (fom_index_pfp_aligned_exists_B) = M) -> exists fom_value_pfp_aligned_exists_B. ((((exists fom_beta_height_pfp_aligned_exists_B_entry. fom_beta_height_pfp_aligned_exists_B_entry + S (fom_value_pfp_aligned_exists_B) = S ((S (fom_index_pfp_aligned_exists_B)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_exists_B_entry. bb = fom_beta_quotient_pfp_aligned_exists_B_entry * S ((S (fom_index_pfp_aligned_exists_B)) * bc) + (fom_value_pfp_aligned_exists_B))) /\ (exists fom_gap_pfp_aligned_exists_B_value_bound. fom_gap_pfp_aligned_exists_B_value_bound + S (fom_value_pfp_aligned_exists_B) = p))) -> (exists rb rc. ((forall fom_index_pfp_aligned_exists_output_left_bounded. (exists fom_gap_pfp_aligned_exists_output_left_bounded_index_bound. fom_gap_pfp_aligned_exists_output_left_bounded_index_bound + S (fom_index_pfp_aligned_exists_output_left_bounded) = L) -> exists fom_value_pfp_aligned_exists_output_left_bounded. ((((exists fom_beta_height_pfp_aligned_exists_output_left_bounded_entry. fom_beta_height_pfp_aligned_exists_output_left_bounded_entry + S (fom_value_pfp_aligned_exists_output_left_bounded) = S ((S (fom_index_pfp_aligned_exists_output_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_exists_output_left_bounded_entry. ab = fom_beta_quotient_pfp_aligned_exists_output_left_bounded_entry * S ((S (fom_index_pfp_aligned_exists_output_left_bounded)) * ac) + (fom_value_pfp_aligned_exists_output_left_bounded))) /\ (exists fom_gap_pfp_aligned_exists_output_left_bounded_value_bound. fom_gap_pfp_aligned_exists_output_left_bounded_value_bound + S (fom_value_pfp_aligned_exists_output_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_exists_output_right_bounded. (exists fom_gap_pfp_aligned_exists_output_right_bounded_index_bound. fom_gap_pfp_aligned_exists_output_right_bounded_index_bound + S (fom_index_pfp_aligned_exists_output_right_bounded) = M) -> exists fom_value_pfp_aligned_exists_output_right_bounded. ((((exists fom_beta_height_pfp_aligned_exists_output_right_bounded_entry. fom_beta_height_pfp_aligned_exists_output_right_bounded_entry + S (fom_value_pfp_aligned_exists_output_right_bounded) = S ((S (fom_index_pfp_aligned_exists_output_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_exists_output_right_bounded_entry. bb = fom_beta_quotient_pfp_aligned_exists_output_right_bounded_entry * S ((S (fom_index_pfp_aligned_exists_output_right_bounded)) * bc) + (fom_value_pfp_aligned_exists_output_right_bounded))) /\ (exists fom_gap_pfp_aligned_exists_output_right_bounded_value_bound. fom_gap_pfp_aligned_exists_output_right_bounded_value_bound + S (fom_value_pfp_aligned_exists_output_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_exists_output_result_bounded. (exists fom_gap_pfp_aligned_exists_output_result_bounded_index_bound. fom_gap_pfp_aligned_exists_output_result_bounded_index_bound + S (fom_index_pfp_aligned_exists_output_result_bounded) = L+M) -> exists fom_value_pfp_aligned_exists_output_result_bounded. ((((exists fom_beta_height_pfp_aligned_exists_output_result_bounded_entry. fom_beta_height_pfp_aligned_exists_output_result_bounded_entry + S (fom_value_pfp_aligned_exists_output_result_bounded) = S ((S (fom_index_pfp_aligned_exists_output_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_exists_output_result_bounded_entry. rb = fom_beta_quotient_pfp_aligned_exists_output_result_bounded_entry * S ((S (fom_index_pfp_aligned_exists_output_result_bounded)) * rc) + (fom_value_pfp_aligned_exists_output_result_bounded))) /\ (exists fom_gap_pfp_aligned_exists_output_result_bounded_value_bound. fom_gap_pfp_aligned_exists_output_result_bounded_value_bound + S (fom_value_pfp_aligned_exists_output_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_exists_output pfaa_left_c_aligned_exists_output pfaa_right_b_aligned_exists_output pfaa_right_c_aligned_exists_output pfaa_sum_b_aligned_exists_output pfaa_sum_c_aligned_exists_output pfaa_length_aligned_exists_output. ((((forall pfrep_power_aligned_exists_output_witness_common_left pfrep_left_aligned_exists_output_witness_common_left pfrep_right_aligned_exists_output_witness_common_left. ((exists pfrep_position_aligned_exists_output_witness_common_leftfirst. ((pfrep_position_aligned_exists_output_witness_common_leftfirst+S (pfrep_power_aligned_exists_output_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_exists_output_witness_common_leftfirstentry. ff_h_pfp_aligned_exists_output_witness_common_leftfirstentry + S (pfrep_left_aligned_exists_output_witness_common_left) = S ((S (pfrep_position_aligned_exists_output_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_aligned_exists_output_witness_common_leftfirstentry. ab = ff_q_pfp_aligned_exists_output_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_exists_output_witness_common_leftfirst)) * ac) + (pfrep_left_aligned_exists_output_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_exists_output_witness_common_leftfirstoutside. pfrep_gap_aligned_exists_output_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_exists_output_witness_common_left)) /\ (((pfrep_left_aligned_exists_output_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_exists_output_witness_common_leftsecond. ((pfrep_position_aligned_exists_output_witness_common_leftsecond+S (pfrep_power_aligned_exists_output_witness_common_left)=(pfaa_length_aligned_exists_output)) /\ ((((exists ff_h_pfp_aligned_exists_output_witness_common_leftsecondentry. ff_h_pfp_aligned_exists_output_witness_common_leftsecondentry + S (pfrep_right_aligned_exists_output_witness_common_left) = S ((S (pfrep_position_aligned_exists_output_witness_common_leftsecond)) * pfaa_left_c_aligned_exists_output)) /\ exists ff_q_pfp_aligned_exists_output_witness_common_leftsecondentry. pfaa_left_b_aligned_exists_output = ff_q_pfp_aligned_exists_output_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_exists_output_witness_common_leftsecond)) * pfaa_left_c_aligned_exists_output) + (pfrep_right_aligned_exists_output_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_exists_output_witness_common_leftsecondoutside. pfrep_gap_aligned_exists_output_witness_common_leftsecondoutside+(pfaa_length_aligned_exists_output)=(pfrep_power_aligned_exists_output_witness_common_left)) /\ (((pfrep_right_aligned_exists_output_witness_common_left)=0))))) -> pfrep_left_aligned_exists_output_witness_common_left=pfrep_right_aligned_exists_output_witness_common_left) /\ ((forall pfrep_power_aligned_exists_output_witness_common_right pfrep_left_aligned_exists_output_witness_common_right pfrep_right_aligned_exists_output_witness_common_right. ((exists pfrep_position_aligned_exists_output_witness_common_rightfirst. ((pfrep_position_aligned_exists_output_witness_common_rightfirst+S (pfrep_power_aligned_exists_output_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_exists_output_witness_common_rightfirstentry. ff_h_pfp_aligned_exists_output_witness_common_rightfirstentry + S (pfrep_left_aligned_exists_output_witness_common_right) = S ((S (pfrep_position_aligned_exists_output_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_aligned_exists_output_witness_common_rightfirstentry. bb = ff_q_pfp_aligned_exists_output_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_exists_output_witness_common_rightfirst)) * bc) + (pfrep_left_aligned_exists_output_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_exists_output_witness_common_rightfirstoutside. pfrep_gap_aligned_exists_output_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_exists_output_witness_common_right)) /\ (((pfrep_left_aligned_exists_output_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_exists_output_witness_common_rightsecond. ((pfrep_position_aligned_exists_output_witness_common_rightsecond+S (pfrep_power_aligned_exists_output_witness_common_right)=(pfaa_length_aligned_exists_output)) /\ ((((exists ff_h_pfp_aligned_exists_output_witness_common_rightsecondentry. ff_h_pfp_aligned_exists_output_witness_common_rightsecondentry + S (pfrep_right_aligned_exists_output_witness_common_right) = S ((S (pfrep_position_aligned_exists_output_witness_common_rightsecond)) * pfaa_right_c_aligned_exists_output)) /\ exists ff_q_pfp_aligned_exists_output_witness_common_rightsecondentry. pfaa_right_b_aligned_exists_output = ff_q_pfp_aligned_exists_output_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_exists_output_witness_common_rightsecond)) * pfaa_right_c_aligned_exists_output) + (pfrep_right_aligned_exists_output_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_exists_output_witness_common_rightsecondoutside. pfrep_gap_aligned_exists_output_witness_common_rightsecondoutside+(pfaa_length_aligned_exists_output)=(pfrep_power_aligned_exists_output_witness_common_right)) /\ (((pfrep_right_aligned_exists_output_witness_common_right)=0))))) -> pfrep_left_aligned_exists_output_witness_common_right=pfrep_right_aligned_exists_output_witness_common_right)))) /\ (((forall pfp_index_aligned_exists_output_witness_operation. (exists pfa_gap_aligned_exists_output_witness_operationindex. pfa_gap_aligned_exists_output_witness_operationindex + S (pfp_index_aligned_exists_output_witness_operation) = (pfaa_length_aligned_exists_output)) -> exists pfp_left_aligned_exists_output_witness_operation pfp_right_aligned_exists_output_witness_operation pfp_value_aligned_exists_output_witness_operation. ((((exists ff_h_pfp_aligned_exists_output_witness_operationleft. ff_h_pfp_aligned_exists_output_witness_operationleft + S (pfp_left_aligned_exists_output_witness_operation) = S ((S (pfp_index_aligned_exists_output_witness_operation)) * pfaa_left_c_aligned_exists_output)) /\ exists ff_q_pfp_aligned_exists_output_witness_operationleft. pfaa_left_b_aligned_exists_output = ff_q_pfp_aligned_exists_output_witness_operationleft * S ((S (pfp_index_aligned_exists_output_witness_operation)) * pfaa_left_c_aligned_exists_output) + (pfp_left_aligned_exists_output_witness_operation))) /\ (((((exists ff_h_pfp_aligned_exists_output_witness_operationright. ff_h_pfp_aligned_exists_output_witness_operationright + S (pfp_right_aligned_exists_output_witness_operation) = S ((S (pfp_index_aligned_exists_output_witness_operation)) * pfaa_right_c_aligned_exists_output)) /\ exists ff_q_pfp_aligned_exists_output_witness_operationright. pfaa_right_b_aligned_exists_output = ff_q_pfp_aligned_exists_output_witness_operationright * S ((S (pfp_index_aligned_exists_output_witness_operation)) * pfaa_right_c_aligned_exists_output) + (pfp_right_aligned_exists_output_witness_operation))) /\ (((((exists ff_h_pfp_aligned_exists_output_witness_operationtarget. ff_h_pfp_aligned_exists_output_witness_operationtarget + S (pfp_value_aligned_exists_output_witness_operation) = S ((S (pfp_index_aligned_exists_output_witness_operation)) * pfaa_sum_c_aligned_exists_output)) /\ exists ff_q_pfp_aligned_exists_output_witness_operationtarget. pfaa_sum_b_aligned_exists_output = ff_q_pfp_aligned_exists_output_witness_operationtarget * S ((S (pfp_index_aligned_exists_output_witness_operation)) * pfaa_sum_c_aligned_exists_output) + (pfp_value_aligned_exists_output_witness_operation))) /\ ((((exists pfa_gap_aligned_exists_output_witness_operationoperationleft. pfa_gap_aligned_exists_output_witness_operationoperationleft + S (pfp_left_aligned_exists_output_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_exists_output_witness_operationoperationright. pfa_gap_aligned_exists_output_witness_operationoperationright + S (pfp_right_aligned_exists_output_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_exists_output_witness_operationoperationresultbound. pfa_gap_aligned_exists_output_witness_operationoperationresultbound + S (pfp_value_aligned_exists_output_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_exists_output_witness_operationoperationresultcongruence pfa_offset_right_aligned_exists_output_witness_operationoperationresultcongruence. ((pfp_left_aligned_exists_output_witness_operation) + (pfp_right_aligned_exists_output_witness_operation)) + (p) * pfa_offset_left_aligned_exists_output_witness_operationoperationresultcongruence = (pfp_value_aligned_exists_output_witness_operation) + (p) * pfa_offset_right_aligned_exists_output_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_exists_output_witness_output pfrep_left_aligned_exists_output_witness_output pfrep_right_aligned_exists_output_witness_output. ((exists pfrep_position_aligned_exists_output_witness_outputfirst. ((pfrep_position_aligned_exists_output_witness_outputfirst+S (pfrep_power_aligned_exists_output_witness_output)=(pfaa_length_aligned_exists_output)) /\ ((((exists ff_h_pfp_aligned_exists_output_witness_outputfirstentry. ff_h_pfp_aligned_exists_output_witness_outputfirstentry + S (pfrep_left_aligned_exists_output_witness_output) = S ((S (pfrep_position_aligned_exists_output_witness_outputfirst)) * pfaa_sum_c_aligned_exists_output)) /\ exists ff_q_pfp_aligned_exists_output_witness_outputfirstentry. pfaa_sum_b_aligned_exists_output = ff_q_pfp_aligned_exists_output_witness_outputfirstentry * S ((S (pfrep_position_aligned_exists_output_witness_outputfirst)) * pfaa_sum_c_aligned_exists_output) + (pfrep_left_aligned_exists_output_witness_output)))))) \/ (((exists pfrep_gap_aligned_exists_output_witness_outputfirstoutside. pfrep_gap_aligned_exists_output_witness_outputfirstoutside+(pfaa_length_aligned_exists_output)=(pfrep_power_aligned_exists_output_witness_output)) /\ (((pfrep_left_aligned_exists_output_witness_output)=0))))) -> ((exists pfrep_position_aligned_exists_output_witness_outputsecond. ((pfrep_position_aligned_exists_output_witness_outputsecond+S (pfrep_power_aligned_exists_output_witness_output)=(L+M)) /\ ((((exists ff_h_pfp_aligned_exists_output_witness_outputsecondentry. ff_h_pfp_aligned_exists_output_witness_outputsecondentry + S (pfrep_right_aligned_exists_output_witness_output) = S ((S (pfrep_position_aligned_exists_output_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_aligned_exists_output_witness_outputsecondentry. rb = ff_q_pfp_aligned_exists_output_witness_outputsecondentry * S ((S (pfrep_position_aligned_exists_output_witness_outputsecond)) * rc) + (pfrep_right_aligned_exists_output_witness_output)))))) \/ (((exists pfrep_gap_aligned_exists_output_witness_outputsecondoutside. pfrep_gap_aligned_exists_output_witness_outputsecondoutside+(L+M)=(pfrep_power_aligned_exists_output_witness_output)) /\ (((pfrep_right_aligned_exists_output_witness_output)=0))))) -> pfrep_left_aligned_exists_output_witness_output=pfrep_right_aligned_exists_output_witness_output)))))))))))))

Constructive proof overview

Generated structural guide

Construct a genuine canonical aligned sum at the explicit length L+M from any two canonical inputs, rather than assuming operation witnesses.

The unchanged tactic script uses 6 declared prerequisites and contains 87 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG0039 prime_field_polynomial_common_representatives_exists prime_field_polynomial_add_exists Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized prime_field_polynomial_add_bounded Alpha theorem; checked-use authorized PG003C prime_field_polynomial_aligned_add_from_common prime_field_polynomial_power_coefficient_functional Alpha theorem; checked-use authorized

Direct dependents

PG0058 prime_field_polynomial_right_divides_aligned_add PG005D prime_field_polynomial_euclidean_backward_coefficient_identity

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

87 script commands · 14 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.

Named ingredients (2)
prime field polynomial common representatives existsprime field polynomial aligned add from common

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 L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro hp
  9. L9
    intro ha
  10. L10
    intro hb
02Establish hcL11–20

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

  1. L11
    have hc : ∃ ub. ∃ uc. ∃ vb. ∃ vc. BetaPrefixInto(ub,uc,L + M,p) ∧ (BetaPrefixInto(vb,vc,L + M,p) ∧ CommonRepresentatives(ab,ac,L,bb,bc,M,ub,uc,vb,vc,L + M))Definitions: BetaPrefixIntoCommonRepresentatives
  2. L12
    specialize prime_field_polynomial_common_representatives_exists (p)
  3. L13
    specialize prime_field_polynomial_common_representatives_exists (ab)
  4. L14
    specialize prime_field_polynomial_common_representatives_exists (ac)
  5. L15
    specialize prime_field_polynomial_common_representatives_exists (L)
  6. L16
    specialize prime_field_polynomial_common_representatives_exists (bb)
  7. L17
    specialize prime_field_polynomial_common_representatives_exists (bc)
  8. L18
    specialize prime_field_polynomial_common_representatives_exists (M)
  9. L19
    apply prime_field_polynomial_common_representatives_exists
  10. L20
    exact hp
03Use earlier factsL21–22

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

  1. L21
    exact ha
  2. L22
    exact hb
04Separate the logical casesL23–28

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

  1. L23
    cases hc
  2. L24
    cases hc_witness
  3. L25
    cases hc_witness_witness
  4. L26
    cases hc_witness_witness_witness
  5. L27
    cases hc_witness_witness_witness_witness
  6. L28
    cases hc_witness_witness_witness_witness_right
05Establish hsL29–38

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

  1. L29
    have hs : ∃ rb. ∃ rc. FpPolyAdd(p,x,x1,x2,x3,rb,rc,L + M)Definitions: FpPolyAdd
  2. L30
    specialize prime_field_polynomial_add_exists (p)
  3. L31
    specialize prime_field_polynomial_add_exists (x)
  4. L32
    specialize prime_field_polynomial_add_exists (x1)
  5. L33
    specialize prime_field_polynomial_add_exists (x2)
  6. L34
    specialize prime_field_polynomial_add_exists (x3)
  7. L35
    specialize prime_field_polynomial_add_exists (L+M)
  8. L36
    apply prime_field_polynomial_add_exists
  9. L37
    intro hz
  10. L38
    specialize prime_nonzero (p)
06Use earlier factsL39–43

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

  1. L39
    apply prime_nonzero
  2. L40
    exact hp
  3. L41
    exact hz
  4. L42
    exact hc_witness_witness_witness_witness_left
  5. L43
    exact hc_witness_witness_witness_witness_right_left
07Separate the logical casesL44–45

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

  1. L44
    cases hs
  2. L45
    cases hs_witness
08Establish hsboundL46–55

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

  1. L46
    have hsbound : BetaPrefixInto(x,x1,L + M,p) ∧ (BetaPrefixInto(x2,x3,L + M,p) ∧ BetaPrefixInto(x4,x5,L + M,p))Definitions: BetaPrefixInto
  2. L47
    specialize prime_field_polynomial_add_bounded (p)
  3. L48
    specialize prime_field_polynomial_add_bounded (x)
  4. L49
    specialize prime_field_polynomial_add_bounded (x1)
  5. L50
    specialize prime_field_polynomial_add_bounded (x2)
  6. L51
    specialize prime_field_polynomial_add_bounded (x3)
  7. L52
    specialize prime_field_polynomial_add_bounded (x4)
  8. L53
    specialize prime_field_polynomial_add_bounded (x5)
  9. L54
    specialize prime_field_polynomial_add_bounded (L+M)
  10. L55
    apply prime_field_polynomial_add_bounded
09Use earlier factsL56–56

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

  1. L56
    exact hs_witness_witness
10Separate the logical casesL57–58

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

  1. L57
    cases hsbound
  2. L58
    cases hsbound_right
11Construct an explicit witnessL59–60

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

  1. L59
    exists x4
  2. L60
    exists x5
12Use earlier factsL61–70

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

  1. L61
    specialize prime_field_polynomial_aligned_add_from_common (p)
  2. L62
    specialize prime_field_polynomial_aligned_add_from_common (ab)
  3. L63
    specialize prime_field_polynomial_aligned_add_from_common (ac)
  4. L64
    specialize prime_field_polynomial_aligned_add_from_common (L)
  5. L65
    specialize prime_field_polynomial_aligned_add_from_common (bb)
  6. L66
    specialize prime_field_polynomial_aligned_add_from_common (bc)
  7. L67
    specialize prime_field_polynomial_aligned_add_from_common (M)
  8. L68
    specialize prime_field_polynomial_aligned_add_from_common (x4)
  9. L69
    specialize prime_field_polynomial_aligned_add_from_common (x5)
  10. L70
    specialize prime_field_polynomial_aligned_add_from_common (L+M)
13Use earlier factsL71–80

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

  1. L71
    specialize prime_field_polynomial_aligned_add_from_common (x)
  2. L72
    specialize prime_field_polynomial_aligned_add_from_common (x1)
  3. L73
    specialize prime_field_polynomial_aligned_add_from_common (x2)
  4. L74
    specialize prime_field_polynomial_aligned_add_from_common (x3)
  5. L75
    specialize prime_field_polynomial_aligned_add_from_common (x4)
  6. L76
    specialize prime_field_polynomial_aligned_add_from_common (x5)
  7. L77
    specialize prime_field_polynomial_aligned_add_from_common (L+M)
  8. L78
    apply prime_field_polynomial_aligned_add_from_common
  9. L79
    exact ha
  10. L80
    exact hb
14Use earlier factsL81–87

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

  1. L81
    exact hsbound_right_right
  2. L82
    exact hc_witness_witness_witness_witness_right_right
  3. L83
    exact hs_witness_witness
  4. L84
    specialize prime_field_polynomial_power_coefficient_functional (x4)
  5. L85
    specialize prime_field_polynomial_power_coefficient_functional (x5)
  6. L86
    specialize prime_field_polynomial_power_coefficient_functional (L+M)
  7. L87
    apply prime_field_polynomial_power_coefficient_functional

Library-wide reading audit

Original exact command ledger · 87 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hb
  11. 0011have hc : exists ub uc vb vc. ((forall fom_index_pfp_aligned_exists_left_bound. (exists fom_gap_pfp_aligned_exists_left_bound_index_bound. fom_gap_pfp_aligned_exists_left_bound_index_bound + S (fom_index_pfp_aligned_exists_left_bound) = L+M) -> exists fom_value_pfp_aligned_exists_left_bound. ((((exists fom_beta_height_pfp_aligned_exists_left_bound_entry. fom_beta_height_pfp_aligned_exists_left_bound_entry + S (fom_value_pfp_aligned_exists_left_bound) = S ((S (fom_index_pfp_aligned_exists_left_bound)) * uc)) /\ exists fom_beta_quotient_pfp_aligned_exists_left_bound_entry. ub = fom_beta_quotient_pfp_aligned_exists_left_bound_entry * S ((S (fom_index_pfp_aligned_exists_left_bound)) * uc) + (fom_value_pfp_aligned_exists_left_bound))) /\ (exists fom_gap_pfp_aligned_exists_left_bound_value_bound. fom_gap_pfp_aligned_exists_left_bound_value_bound + S (fom_value_pfp_aligned_exists_left_bound) = p))) /\ (((forall fom_index_pfp_aligned_exists_right_bound. (exists fom_gap_pfp_aligned_exists_right_bound_index_bound. fom_gap_pfp_aligned_exists_right_bound_index_bound + S (fom_index_pfp_aligned_exists_right_bound) = L+M) -> exists fom_value_pfp_aligned_exists_right_bound. ((((exists fom_beta_height_pfp_aligned_exists_right_bound_entry. fom_beta_height_pfp_aligned_exists_right_bound_entry + S (fom_value_pfp_aligned_exists_right_bound) = S ((S (fom_index_pfp_aligned_exists_right_bound)) * vc)) /\ exists fom_beta_quotient_pfp_aligned_exists_right_bound_entry. vb = fom_beta_quotient_pfp_aligned_exists_right_bound_entry * S ((S (fom_index_pfp_aligned_exists_right_bound)) * vc) + (fom_value_pfp_aligned_exists_right_bound))) /\ (exists fom_gap_pfp_aligned_exists_right_bound_value_bound. fom_gap_pfp_aligned_exists_right_bound_value_bound + S (fom_value_pfp_aligned_exists_right_bound) = p))) /\ ((((forall pfrep_power_aligned_exists_common_left pfrep_left_aligned_exists_common_left pfrep_right_aligned_exists_common_left. ((exists pfrep_position_aligned_exists_common_leftfirst. ((pfrep_position_aligned_exists_common_leftfirst+S (pfrep_power_aligned_exists_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_exists_common_leftfirstentry. ff_h_pfp_aligned_exists_common_leftfirstentry + S (pfrep_left_aligned_exists_common_left) = S ((S (pfrep_position_aligned_exists_common_leftfirst)) * ac)) /\ exists ff_q_pfp_aligned_exists_common_leftfirstentry. ab = ff_q_pfp_aligned_exists_common_leftfirstentry * S ((S (pfrep_position_aligned_exists_common_leftfirst)) * ac) + (pfrep_left_aligned_exists_common_left)))))) \/ (((exists pfrep_gap_aligned_exists_common_leftfirstoutside. pfrep_gap_aligned_exists_common_leftfirstoutside+(L)=(pfrep_power_aligned_exists_common_left)) /\ (((pfrep_left_aligned_exists_common_left)=0))))) -> ((exists pfrep_position_aligned_exists_common_leftsecond. ((pfrep_position_aligned_exists_common_leftsecond+S (pfrep_power_aligned_exists_common_left)=(L+M)) /\ ((((exists ff_h_pfp_aligned_exists_common_leftsecondentry. ff_h_pfp_aligned_exists_common_leftsecondentry + S (pfrep_right_aligned_exists_common_left) = S ((S (pfrep_position_aligned_exists_common_leftsecond)) * uc)) /\ exists ff_q_pfp_aligned_exists_common_leftsecondentry. ub = ff_q_pfp_aligned_exists_common_leftsecondentry * S ((S (pfrep_position_aligned_exists_common_leftsecond)) * uc) + (pfrep_right_aligned_exists_common_left)))))) \/ (((exists pfrep_gap_aligned_exists_common_leftsecondoutside. pfrep_gap_aligned_exists_common_leftsecondoutside+(L+M)=(pfrep_power_aligned_exists_common_left)) /\ (((pfrep_right_aligned_exists_common_left)=0))))) -> pfrep_left_aligned_exists_common_left=pfrep_right_aligned_exists_common_left) /\ ((forall pfrep_power_aligned_exists_common_right pfrep_left_aligned_exists_common_right pfrep_right_aligned_exists_common_right. ((exists pfrep_position_aligned_exists_common_rightfirst. ((pfrep_position_aligned_exists_common_rightfirst+S (pfrep_power_aligned_exists_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_exists_common_rightfirstentry. ff_h_pfp_aligned_exists_common_rightfirstentry + S (pfrep_left_aligned_exists_common_right) = S ((S (pfrep_position_aligned_exists_common_rightfirst)) * bc)) /\ exists ff_q_pfp_aligned_exists_common_rightfirstentry. bb = ff_q_pfp_aligned_exists_common_rightfirstentry * S ((S (pfrep_position_aligned_exists_common_rightfirst)) * bc) + (pfrep_left_aligned_exists_common_right)))))) \/ (((exists pfrep_gap_aligned_exists_common_rightfirstoutside. pfrep_gap_aligned_exists_common_rightfirstoutside+(M)=(pfrep_power_aligned_exists_common_right)) /\ (((pfrep_left_aligned_exists_common_right)=0))))) -> ((exists pfrep_position_aligned_exists_common_rightsecond. ((pfrep_position_aligned_exists_common_rightsecond+S (pfrep_power_aligned_exists_common_right)=(L+M)) /\ ((((exists ff_h_pfp_aligned_exists_common_rightsecondentry. ff_h_pfp_aligned_exists_common_rightsecondentry + S (pfrep_right_aligned_exists_common_right) = S ((S (pfrep_position_aligned_exists_common_rightsecond)) * vc)) /\ exists ff_q_pfp_aligned_exists_common_rightsecondentry. vb = ff_q_pfp_aligned_exists_common_rightsecondentry * S ((S (pfrep_position_aligned_exists_common_rightsecond)) * vc) + (pfrep_right_aligned_exists_common_right)))))) \/ (((exists pfrep_gap_aligned_exists_common_rightsecondoutside. pfrep_gap_aligned_exists_common_rightsecondoutside+(L+M)=(pfrep_power_aligned_exists_common_right)) /\ (((pfrep_right_aligned_exists_common_right)=0))))) -> pfrep_left_aligned_exists_common_right=pfrep_right_aligned_exists_common_right))))))))
  12. 0012specialize prime_field_polynomial_common_representatives_exists (p)
  13. 0013specialize prime_field_polynomial_common_representatives_exists (ab)
  14. 0014specialize prime_field_polynomial_common_representatives_exists (ac)
  15. 0015specialize prime_field_polynomial_common_representatives_exists (L)
  16. 0016specialize prime_field_polynomial_common_representatives_exists (bb)
  17. 0017specialize prime_field_polynomial_common_representatives_exists (bc)
  18. 0018specialize prime_field_polynomial_common_representatives_exists (M)
  19. 0019apply prime_field_polynomial_common_representatives_exists
  20. 0020exact hp
  21. 0021exact ha
  22. 0022exact hb
  23. 0023cases hc
  24. 0024cases hc_witness
  25. 0025cases hc_witness_witness
  26. 0026cases hc_witness_witness_witness
  27. 0027cases hc_witness_witness_witness_witness
  28. 0028cases hc_witness_witness_witness_witness_right
  29. 0029have hs : exists rb rc. forall pfp_index_aligned_exists_sum. (exists pfa_gap_aligned_exists_sumindex. pfa_gap_aligned_exists_sumindex + S (pfp_index_aligned_exists_sum) = (L+M)) -> exists pfp_left_aligned_exists_sum pfp_right_aligned_exists_sum pfp_value_aligned_exists_sum. ((((exists ff_h_pfp_aligned_exists_sumleft. ff_h_pfp_aligned_exists_sumleft + S (pfp_left_aligned_exists_sum) = S ((S (pfp_index_aligned_exists_sum)) * x1)) /\ exists ff_q_pfp_aligned_exists_sumleft. x = ff_q_pfp_aligned_exists_sumleft * S ((S (pfp_index_aligned_exists_sum)) * x1) + (pfp_left_aligned_exists_sum))) /\ (((((exists ff_h_pfp_aligned_exists_sumright. ff_h_pfp_aligned_exists_sumright + S (pfp_right_aligned_exists_sum) = S ((S (pfp_index_aligned_exists_sum)) * x3)) /\ exists ff_q_pfp_aligned_exists_sumright. x2 = ff_q_pfp_aligned_exists_sumright * S ((S (pfp_index_aligned_exists_sum)) * x3) + (pfp_right_aligned_exists_sum))) /\ (((((exists ff_h_pfp_aligned_exists_sumtarget. ff_h_pfp_aligned_exists_sumtarget + S (pfp_value_aligned_exists_sum) = S ((S (pfp_index_aligned_exists_sum)) * rc)) /\ exists ff_q_pfp_aligned_exists_sumtarget. rb = ff_q_pfp_aligned_exists_sumtarget * S ((S (pfp_index_aligned_exists_sum)) * rc) + (pfp_value_aligned_exists_sum))) /\ ((((exists pfa_gap_aligned_exists_sumoperationleft. pfa_gap_aligned_exists_sumoperationleft + S (pfp_left_aligned_exists_sum) = (p)) /\ (((exists pfa_gap_aligned_exists_sumoperationright. pfa_gap_aligned_exists_sumoperationright + S (pfp_right_aligned_exists_sum) = (p)) /\ ((((exists pfa_gap_aligned_exists_sumoperationresultbound. pfa_gap_aligned_exists_sumoperationresultbound + S (pfp_value_aligned_exists_sum) = (p)) /\ ((exists pfa_offset_left_aligned_exists_sumoperationresultcongruence pfa_offset_right_aligned_exists_sumoperationresultcongruence. ((pfp_left_aligned_exists_sum) + (pfp_right_aligned_exists_sum)) + (p) * pfa_offset_left_aligned_exists_sumoperationresultcongruence = (pfp_value_aligned_exists_sum) + (p) * pfa_offset_right_aligned_exists_sumoperationresultcongruence)))))))))))))))
  30. 0030specialize prime_field_polynomial_add_exists (p)
  31. 0031specialize prime_field_polynomial_add_exists (x)
  32. 0032specialize prime_field_polynomial_add_exists (x1)
  33. 0033specialize prime_field_polynomial_add_exists (x2)
  34. 0034specialize prime_field_polynomial_add_exists (x3)
  35. 0035specialize prime_field_polynomial_add_exists (L+M)
  36. 0036apply prime_field_polynomial_add_exists
  37. 0037intro hz
  38. 0038specialize prime_nonzero (p)
  39. 0039apply prime_nonzero
  40. 0040exact hp
  41. 0041exact hz
  42. 0042exact hc_witness_witness_witness_witness_left
  43. 0043exact hc_witness_witness_witness_witness_right_left
  44. 0044cases hs
  45. 0045cases hs_witness
  46. 0046have hsbound : ((forall fom_index_pfp_aligned_exists_sum_left. (exists fom_gap_pfp_aligned_exists_sum_left_index_bound. fom_gap_pfp_aligned_exists_sum_left_index_bound + S (fom_index_pfp_aligned_exists_sum_left) = L+M) -> exists fom_value_pfp_aligned_exists_sum_left. ((((exists fom_beta_height_pfp_aligned_exists_sum_left_entry. fom_beta_height_pfp_aligned_exists_sum_left_entry + S (fom_value_pfp_aligned_exists_sum_left) = S ((S (fom_index_pfp_aligned_exists_sum_left)) * x1)) /\ exists fom_beta_quotient_pfp_aligned_exists_sum_left_entry. x = fom_beta_quotient_pfp_aligned_exists_sum_left_entry * S ((S (fom_index_pfp_aligned_exists_sum_left)) * x1) + (fom_value_pfp_aligned_exists_sum_left))) /\ (exists fom_gap_pfp_aligned_exists_sum_left_value_bound. fom_gap_pfp_aligned_exists_sum_left_value_bound + S (fom_value_pfp_aligned_exists_sum_left) = p))) /\ (((forall fom_index_pfp_aligned_exists_sum_right. (exists fom_gap_pfp_aligned_exists_sum_right_index_bound. fom_gap_pfp_aligned_exists_sum_right_index_bound + S (fom_index_pfp_aligned_exists_sum_right) = L+M) -> exists fom_value_pfp_aligned_exists_sum_right. ((((exists fom_beta_height_pfp_aligned_exists_sum_right_entry. fom_beta_height_pfp_aligned_exists_sum_right_entry + S (fom_value_pfp_aligned_exists_sum_right) = S ((S (fom_index_pfp_aligned_exists_sum_right)) * x3)) /\ exists fom_beta_quotient_pfp_aligned_exists_sum_right_entry. x2 = fom_beta_quotient_pfp_aligned_exists_sum_right_entry * S ((S (fom_index_pfp_aligned_exists_sum_right)) * x3) + (fom_value_pfp_aligned_exists_sum_right))) /\ (exists fom_gap_pfp_aligned_exists_sum_right_value_bound. fom_gap_pfp_aligned_exists_sum_right_value_bound + S (fom_value_pfp_aligned_exists_sum_right) = p))) /\ ((forall fom_index_pfp_aligned_exists_sum_output. (exists fom_gap_pfp_aligned_exists_sum_output_index_bound. fom_gap_pfp_aligned_exists_sum_output_index_bound + S (fom_index_pfp_aligned_exists_sum_output) = L+M) -> exists fom_value_pfp_aligned_exists_sum_output. ((((exists fom_beta_height_pfp_aligned_exists_sum_output_entry. fom_beta_height_pfp_aligned_exists_sum_output_entry + S (fom_value_pfp_aligned_exists_sum_output) = S ((S (fom_index_pfp_aligned_exists_sum_output)) * x5)) /\ exists fom_beta_quotient_pfp_aligned_exists_sum_output_entry. x4 = fom_beta_quotient_pfp_aligned_exists_sum_output_entry * S ((S (fom_index_pfp_aligned_exists_sum_output)) * x5) + (fom_value_pfp_aligned_exists_sum_output))) /\ (exists fom_gap_pfp_aligned_exists_sum_output_value_bound. fom_gap_pfp_aligned_exists_sum_output_value_bound + S (fom_value_pfp_aligned_exists_sum_output) = p)))))))
  47. 0047specialize prime_field_polynomial_add_bounded (p)
  48. 0048specialize prime_field_polynomial_add_bounded (x)
  49. 0049specialize prime_field_polynomial_add_bounded (x1)
  50. 0050specialize prime_field_polynomial_add_bounded (x2)
  51. 0051specialize prime_field_polynomial_add_bounded (x3)
  52. 0052specialize prime_field_polynomial_add_bounded (x4)
  53. 0053specialize prime_field_polynomial_add_bounded (x5)
  54. 0054specialize prime_field_polynomial_add_bounded (L+M)
  55. 0055apply prime_field_polynomial_add_bounded
  56. 0056exact hs_witness_witness
  57. 0057cases hsbound
  58. 0058cases hsbound_right
  59. 0059exists x4
  60. 0060exists x5
  61. 0061specialize prime_field_polynomial_aligned_add_from_common (p)
  62. 0062specialize prime_field_polynomial_aligned_add_from_common (ab)
  63. 0063specialize prime_field_polynomial_aligned_add_from_common (ac)
  64. 0064specialize prime_field_polynomial_aligned_add_from_common (L)
  65. 0065specialize prime_field_polynomial_aligned_add_from_common (bb)
  66. 0066specialize prime_field_polynomial_aligned_add_from_common (bc)
  67. 0067specialize prime_field_polynomial_aligned_add_from_common (M)
  68. 0068specialize prime_field_polynomial_aligned_add_from_common (x4)
  69. 0069specialize prime_field_polynomial_aligned_add_from_common (x5)
  70. 0070specialize prime_field_polynomial_aligned_add_from_common (L+M)
  71. 0071specialize prime_field_polynomial_aligned_add_from_common (x)
  72. 0072specialize prime_field_polynomial_aligned_add_from_common (x1)
  73. 0073specialize prime_field_polynomial_aligned_add_from_common (x2)
  74. 0074specialize prime_field_polynomial_aligned_add_from_common (x3)
  75. 0075specialize prime_field_polynomial_aligned_add_from_common (x4)
  76. 0076specialize prime_field_polynomial_aligned_add_from_common (x5)
  77. 0077specialize prime_field_polynomial_aligned_add_from_common (L+M)
  78. 0078apply prime_field_polynomial_aligned_add_from_common
  79. 0079exact ha
  80. 0080exact hb
  81. 0081exact hsbound_right_right
  82. 0082exact hc_witness_witness_witness_witness_right_right
  83. 0083exact hs_witness_witness
  84. 0084specialize prime_field_polynomial_power_coefficient_functional (x4)
  85. 0085specialize prime_field_polynomial_power_coefficient_functional (x5)
  86. 0086specialize prime_field_polynomial_power_coefficient_functional (L+M)
  87. 0087apply prime_field_polynomial_power_coefficient_functional