PG001D

prime_field_polynomial_shift_scale_aligned_sum_exists

Construct actual shift and scalar outputs, harmless leading paddings to the common length L+S N, and their actual coefficient sum; the commuted S N+L bound is explicitly reconciled, including both empty inputs.

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

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ c. ∀ ab. ∀ ac. ∀ L. ∀ pb. ∀ pc. ∀ N. Prime(p) → Lt(c,p) → BetaPrefixInto(ab,ac,L,p) → BetaPrefixInto(pb,pc,N,p) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. ∃ v. PolynomialShift(pb,pc,N,x,y) ∧ (FpPolyScale(p,c,ab,ac,z,n,L) ∧ (PolynomialLeftPad(x,y,S N,L,m,k) ∧ (PolynomialLeftPad(z,n,L,S N,i,j) ∧ FpPolyAdd(p,m,k,i,j,u,v,L + S N))))

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 6FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 2FpPolyScale(p,k,ab,ac,bb,bc,l) · 2PolynomialLeftPad(b,c,L,t,d,e) · 4PolynomialShift(b,c,L,d,e) · 2Lt(a,b) · 1Prime(p) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_field_polynomial_shift_existsprime_field_polynomial_scale_exists · checked external prerequisiteprime_field_polynomial_left_pad_exists · checked external prerequisiteprime_field_polynomial_left_pad_bounded · checked external prerequisiteprime_field_polynomial_shift_boundedprime_field_polynomial_scale_bounded · checked external prerequisiteadd_comm · checked external prerequisiteprime_field_polynomial_add_exists · checked external prerequisite
Original expanded first-order statement 
forall p c ab ac L pb pc N. (~((p) = 1) /\ forall pfa_factor_left_append_alignment_prime pfa_factor_right_append_alignment_prime. (p) = pfa_factor_left_append_alignment_prime * pfa_factor_right_append_alignment_prime -> pfa_factor_left_append_alignment_prime = 1 \/ pfa_factor_right_append_alignment_prime = 1) -> (exists pfa_gap_append_alignment_scalar. pfa_gap_append_alignment_scalar + S (c) = (p)) -> (forall fom_index_pfp_append_alignment_A. (exists fom_gap_pfp_append_alignment_A_index_bound. fom_gap_pfp_append_alignment_A_index_bound + S (fom_index_pfp_append_alignment_A) = L) -> exists fom_value_pfp_append_alignment_A. ((((exists fom_beta_height_pfp_append_alignment_A_entry. fom_beta_height_pfp_append_alignment_A_entry + S (fom_value_pfp_append_alignment_A) = S ((S (fom_index_pfp_append_alignment_A)) * ac)) /\ exists fom_beta_quotient_pfp_append_alignment_A_entry. ab = fom_beta_quotient_pfp_append_alignment_A_entry * S ((S (fom_index_pfp_append_alignment_A)) * ac) + (fom_value_pfp_append_alignment_A))) /\ (exists fom_gap_pfp_append_alignment_A_value_bound. fom_gap_pfp_append_alignment_A_value_bound + S (fom_value_pfp_append_alignment_A) = p))) -> (forall fom_index_pfp_append_alignment_P. (exists fom_gap_pfp_append_alignment_P_index_bound. fom_gap_pfp_append_alignment_P_index_bound + S (fom_index_pfp_append_alignment_P) = N) -> exists fom_value_pfp_append_alignment_P. ((((exists fom_beta_height_pfp_append_alignment_P_entry. fom_beta_height_pfp_append_alignment_P_entry + S (fom_value_pfp_append_alignment_P) = S ((S (fom_index_pfp_append_alignment_P)) * pc)) /\ exists fom_beta_quotient_pfp_append_alignment_P_entry. pb = fom_beta_quotient_pfp_append_alignment_P_entry * S ((S (fom_index_pfp_append_alignment_P)) * pc) + (fom_value_pfp_append_alignment_P))) /\ (exists fom_gap_pfp_append_alignment_P_value_bound. fom_gap_pfp_append_alignment_P_value_bound + S (fom_value_pfp_append_alignment_P) = p))) -> (exists ub uc vb vc UB UC VB VC rb rc. ((((forall mdr_i_pfp_append_alignment_result_shiftprefix mdr_a_pfp_append_alignment_result_shiftprefix. (exists mdr_gap_pfp_append_alignment_result_shiftprefixb. mdr_gap_pfp_append_alignment_result_shiftprefixb + S (mdr_i_pfp_append_alignment_result_shiftprefix) = (N)) -> (((exists ff_h_mdr_pfp_append_alignment_result_shiftprefixo. ff_h_mdr_pfp_append_alignment_result_shiftprefixo + S (mdr_a_pfp_append_alignment_result_shiftprefix) = S ((S (mdr_i_pfp_append_alignment_result_shiftprefix)) * pc)) /\ exists ff_q_mdr_pfp_append_alignment_result_shiftprefixo. pb = ff_q_mdr_pfp_append_alignment_result_shiftprefixo * S ((S (mdr_i_pfp_append_alignment_result_shiftprefix)) * pc) + (mdr_a_pfp_append_alignment_result_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_alignment_result_shiftprefixn. ff_h_mdr_pfp_append_alignment_result_shiftprefixn + S (mdr_a_pfp_append_alignment_result_shiftprefix) = S ((S (mdr_i_pfp_append_alignment_result_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_alignment_result_shiftprefixn. ub = ff_q_mdr_pfp_append_alignment_result_shiftprefixn * S ((S (mdr_i_pfp_append_alignment_result_shiftprefix)) * uc) + (mdr_a_pfp_append_alignment_result_shiftprefix)))) /\ ((((exists ff_h_pfp_append_alignment_result_shiftlast. ff_h_pfp_append_alignment_result_shiftlast + S (0) = S ((S (N)) * uc)) /\ exists ff_q_pfp_append_alignment_result_shiftlast. ub = ff_q_pfp_append_alignment_result_shiftlast * S ((S (N)) * uc) + (0)))))) /\ (((((exists pfa_gap_append_alignment_result_scalescalar. pfa_gap_append_alignment_result_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_alignment_result_scale. (exists pfa_gap_append_alignment_result_scaleindex. pfa_gap_append_alignment_result_scaleindex + S (pfp_index_append_alignment_result_scale) = (L)) -> exists pfp_source_append_alignment_result_scale pfp_value_append_alignment_result_scale. ((((exists ff_h_pfp_append_alignment_result_scalesource. ff_h_pfp_append_alignment_result_scalesource + S (pfp_source_append_alignment_result_scale) = S ((S (pfp_index_append_alignment_result_scale)) * ac)) /\ exists ff_q_pfp_append_alignment_result_scalesource. ab = ff_q_pfp_append_alignment_result_scalesource * S ((S (pfp_index_append_alignment_result_scale)) * ac) + (pfp_source_append_alignment_result_scale))) /\ (((((exists ff_h_pfp_append_alignment_result_scaletarget. ff_h_pfp_append_alignment_result_scaletarget + S (pfp_value_append_alignment_result_scale) = S ((S (pfp_index_append_alignment_result_scale)) * vc)) /\ exists ff_q_pfp_append_alignment_result_scaletarget. vb = ff_q_pfp_append_alignment_result_scaletarget * S ((S (pfp_index_append_alignment_result_scale)) * vc) + (pfp_value_append_alignment_result_scale))) /\ ((((exists pfa_gap_append_alignment_result_scaleoperationleft. pfa_gap_append_alignment_result_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_alignment_result_scaleoperationright. pfa_gap_append_alignment_result_scaleoperationright + S (pfp_source_append_alignment_result_scale) = (p)) /\ ((((exists pfa_gap_append_alignment_result_scaleoperationresultbound. pfa_gap_append_alignment_result_scaleoperationresultbound + S (pfp_value_append_alignment_result_scale) = (p)) /\ ((exists pfa_offset_left_append_alignment_result_scaleoperationresultcongruence pfa_offset_right_append_alignment_result_scaleoperationresultcongruence. ((c) * (pfp_source_append_alignment_result_scale)) + (p) * pfa_offset_left_append_alignment_result_scaleoperationresultcongruence = (pfp_value_append_alignment_result_scale) + (p) * pfa_offset_right_append_alignment_result_scaleoperationresultcongruence))))))))))))))))) /\ (((((forall pfp_repeat_index_append_alignment_result_leftzeros. (exists pfa_gap_append_alignment_result_leftzerosindex. pfa_gap_append_alignment_result_leftzerosindex + S (pfp_repeat_index_append_alignment_result_leftzeros) = (L)) -> (((exists ff_h_pfp_append_alignment_result_leftzerosentry. ff_h_pfp_append_alignment_result_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_alignment_result_leftzeros)) * UC)) /\ exists ff_q_pfp_append_alignment_result_leftzerosentry. UB = ff_q_pfp_append_alignment_result_leftzerosentry * S ((S (pfp_repeat_index_append_alignment_result_leftzeros)) * UC) + (0)))) /\ ((forall pfrep_index_append_alignment_result_left pfrep_value_append_alignment_result_left. (exists pfa_gap_append_alignment_result_leftbound. pfa_gap_append_alignment_result_leftbound + S (pfrep_index_append_alignment_result_left) = (S N)) -> (((exists ff_h_pfp_append_alignment_result_leftinput. ff_h_pfp_append_alignment_result_leftinput + S (pfrep_value_append_alignment_result_left) = S ((S (pfrep_index_append_alignment_result_left)) * uc)) /\ exists ff_q_pfp_append_alignment_result_leftinput. ub = ff_q_pfp_append_alignment_result_leftinput * S ((S (pfrep_index_append_alignment_result_left)) * uc) + (pfrep_value_append_alignment_result_left))) -> (((exists ff_h_pfp_append_alignment_result_leftoutput. ff_h_pfp_append_alignment_result_leftoutput + S (pfrep_value_append_alignment_result_left) = S ((S ((L)+pfrep_index_append_alignment_result_left)) * UC)) /\ exists ff_q_pfp_append_alignment_result_leftoutput. UB = ff_q_pfp_append_alignment_result_leftoutput * S ((S ((L)+pfrep_index_append_alignment_result_left)) * UC) + (pfrep_value_append_alignment_result_left))))))) /\ (((((forall pfp_repeat_index_append_alignment_result_rightzeros. (exists pfa_gap_append_alignment_result_rightzerosindex. pfa_gap_append_alignment_result_rightzerosindex + S (pfp_repeat_index_append_alignment_result_rightzeros) = (S N)) -> (((exists ff_h_pfp_append_alignment_result_rightzerosentry. ff_h_pfp_append_alignment_result_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_alignment_result_rightzeros)) * VC)) /\ exists ff_q_pfp_append_alignment_result_rightzerosentry. VB = ff_q_pfp_append_alignment_result_rightzerosentry * S ((S (pfp_repeat_index_append_alignment_result_rightzeros)) * VC) + (0)))) /\ ((forall pfrep_index_append_alignment_result_right pfrep_value_append_alignment_result_right. (exists pfa_gap_append_alignment_result_rightbound. pfa_gap_append_alignment_result_rightbound + S (pfrep_index_append_alignment_result_right) = (L)) -> (((exists ff_h_pfp_append_alignment_result_rightinput. ff_h_pfp_append_alignment_result_rightinput + S (pfrep_value_append_alignment_result_right) = S ((S (pfrep_index_append_alignment_result_right)) * vc)) /\ exists ff_q_pfp_append_alignment_result_rightinput. vb = ff_q_pfp_append_alignment_result_rightinput * S ((S (pfrep_index_append_alignment_result_right)) * vc) + (pfrep_value_append_alignment_result_right))) -> (((exists ff_h_pfp_append_alignment_result_rightoutput. ff_h_pfp_append_alignment_result_rightoutput + S (pfrep_value_append_alignment_result_right) = S ((S ((S N)+pfrep_index_append_alignment_result_right)) * VC)) /\ exists ff_q_pfp_append_alignment_result_rightoutput. VB = ff_q_pfp_append_alignment_result_rightoutput * S ((S ((S N)+pfrep_index_append_alignment_result_right)) * VC) + (pfrep_value_append_alignment_result_right))))))) /\ ((forall pfp_index_append_alignment_result_sum. (exists pfa_gap_append_alignment_result_sumindex. pfa_gap_append_alignment_result_sumindex + S (pfp_index_append_alignment_result_sum) = (L+S N)) -> exists pfp_left_append_alignment_result_sum pfp_right_append_alignment_result_sum pfp_value_append_alignment_result_sum. ((((exists ff_h_pfp_append_alignment_result_sumleft. ff_h_pfp_append_alignment_result_sumleft + S (pfp_left_append_alignment_result_sum) = S ((S (pfp_index_append_alignment_result_sum)) * UC)) /\ exists ff_q_pfp_append_alignment_result_sumleft. UB = ff_q_pfp_append_alignment_result_sumleft * S ((S (pfp_index_append_alignment_result_sum)) * UC) + (pfp_left_append_alignment_result_sum))) /\ (((((exists ff_h_pfp_append_alignment_result_sumright. ff_h_pfp_append_alignment_result_sumright + S (pfp_right_append_alignment_result_sum) = S ((S (pfp_index_append_alignment_result_sum)) * VC)) /\ exists ff_q_pfp_append_alignment_result_sumright. VB = ff_q_pfp_append_alignment_result_sumright * S ((S (pfp_index_append_alignment_result_sum)) * VC) + (pfp_right_append_alignment_result_sum))) /\ (((((exists ff_h_pfp_append_alignment_result_sumtarget. ff_h_pfp_append_alignment_result_sumtarget + S (pfp_value_append_alignment_result_sum) = S ((S (pfp_index_append_alignment_result_sum)) * rc)) /\ exists ff_q_pfp_append_alignment_result_sumtarget. rb = ff_q_pfp_append_alignment_result_sumtarget * S ((S (pfp_index_append_alignment_result_sum)) * rc) + (pfp_value_append_alignment_result_sum))) /\ ((((exists pfa_gap_append_alignment_result_sumoperationleft. pfa_gap_append_alignment_result_sumoperationleft + S (pfp_left_append_alignment_result_sum) = (p)) /\ (((exists pfa_gap_append_alignment_result_sumoperationright. pfa_gap_append_alignment_result_sumoperationright + S (pfp_right_append_alignment_result_sum) = (p)) /\ ((((exists pfa_gap_append_alignment_result_sumoperationresultbound. pfa_gap_append_alignment_result_sumoperationresultbound + S (pfp_value_append_alignment_result_sum) = (p)) /\ ((exists pfa_offset_left_append_alignment_result_sumoperationresultcongruence pfa_offset_right_append_alignment_result_sumoperationresultcongruence. ((pfp_left_append_alignment_result_sum) + (pfp_right_append_alignment_result_sum)) + (p) * pfa_offset_left_append_alignment_result_sumoperationresultcongruence = (pfp_value_append_alignment_result_sum) + (p) * pfa_offset_right_append_alignment_result_sumoperationresultcongruence)))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

134 script commands · 31 reading checkpoints · 10 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 shift existsprime field polynomial shift bounded
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro c
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro L
  6. L6
    intro pb
  7. L7
    intro pc
  8. L8
    intro N
  9. L9
    intro hp
  10. L10
    intro hc
02Fix variables and assumptionsL11–12

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

  1. L11
    intro ha
  2. L12
    intro hb
03Establish hp0L13–18

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

  1. L13
    have hp0 : ~(p=0)
  2. L14
    intro hz
  3. L15
    specialize prime_nonzero (p)
  4. L16
    apply prime_nonzero
  5. L17
    exact hp
  6. L18
    exact hz
04Establish huL19–23

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

  1. L19
    have hu : ∃ ub. ∃ uc. PolynomialShift(pb,pc,N,ub,uc)Definitions: PolynomialShift(pb,pc,N,ub,uc)Original native command in the exact edition
  2. L20
    specialize prime_field_polynomial_shift_exists (pb)
  3. L21
    specialize prime_field_polynomial_shift_exists (pc)
  4. L22
    specialize prime_field_polynomial_shift_exists (N)
  5. L23
    apply prime_field_polynomial_shift_exists
05Separate the logical casesL24–25

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

  1. L24
    cases hu
  2. L25
    cases hu_witness
06Establish hvL26–35

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

  1. L26
    have hv : ∃ vb. ∃ vc. FpPolyScale(p,c,ab,ac,vb,vc,L)Definitions: FpPolyScale(p,c,ab,ac,vb,vc,L)Original native command in the exact edition
  2. L27
    specialize prime_field_polynomial_scale_exists (p)
  3. L28
    specialize prime_field_polynomial_scale_exists (c)
  4. L29
    specialize prime_field_polynomial_scale_exists (ab)
  5. L30
    specialize prime_field_polynomial_scale_exists (ac)
  6. L31
    specialize prime_field_polynomial_scale_exists (L)
  7. L32
    apply prime_field_polynomial_scale_exists
  8. L33
    exact hp0
  9. L34
    exact hc
  10. L35
    exact ha
07Separate the logical casesL36–37

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

  1. L36
    cases hv
  2. L37
    cases hv_witness
08Establish hleftL38–43

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

  1. L38
    have hleft : ∃ UB. ∃ UC. PolynomialLeftPad(x,x1,S N,L,UB,UC)Definitions: PolynomialLeftPad(x,x1,S N,L,UB,UC)Original native command in the exact edition
  2. L39
    specialize prime_field_polynomial_left_pad_exists (x)
  3. L40
    specialize prime_field_polynomial_left_pad_exists (x1)
  4. L41
    specialize prime_field_polynomial_left_pad_exists (L)
  5. L42
    specialize prime_field_polynomial_left_pad_exists (S N)
  6. L43
    apply prime_field_polynomial_left_pad_exists
09Separate the logical casesL44–45

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

  1. L44
    cases hleft
  2. L45
    cases hleft_witness
10Establish hrightL46–51

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

  1. L46
    have hright : ∃ VB. ∃ VC. PolynomialLeftPad(x2,x3,L,S N,VB,VC)Definitions: PolynomialLeftPad(x2,x3,L,S N,VB,VC)Original native command in the exact edition
  2. L47
    specialize prime_field_polynomial_left_pad_exists (x2)
  3. L48
    specialize prime_field_polynomial_left_pad_exists (x3)
  4. L49
    specialize prime_field_polynomial_left_pad_exists (S N)
  5. L50
    specialize prime_field_polynomial_left_pad_exists (L)
  6. L51
    apply prime_field_polynomial_left_pad_exists
11Separate the logical casesL52–53

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

  1. L52
    cases hright
  2. L53
    cases hright_witness
12Establish hleft_boundL54–63

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

  1. L54
    have hleft_bound : BetaPrefixInto(x4,x5,L + S N,p)Definitions: BetaPrefixInto(x4,x5,L + S N,p)Original native command in the exact edition
  2. L55
    specialize prime_field_polynomial_left_pad_bounded (p)
  3. L56
    specialize prime_field_polynomial_left_pad_bounded (x)
  4. L57
    specialize prime_field_polynomial_left_pad_bounded (x1)
  5. L58
    specialize prime_field_polynomial_left_pad_bounded (S N)
  6. L59
    specialize prime_field_polynomial_left_pad_bounded (L)
  7. L60
    specialize prime_field_polynomial_left_pad_bounded (x4)
  8. L61
    specialize prime_field_polynomial_left_pad_bounded (x5)
  9. L62
    apply prime_field_polynomial_left_pad_bounded
  10. L63
    exact hp
13Use earlier factsL64–73

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

  1. L64
    specialize prime_field_polynomial_shift_bounded (p)
  2. L65
    specialize prime_field_polynomial_shift_bounded (pb)
  3. L66
    specialize prime_field_polynomial_shift_bounded (pc)
  4. L67
    specialize prime_field_polynomial_shift_bounded (N)
  5. L68
    specialize prime_field_polynomial_shift_bounded (x)
  6. L69
    specialize prime_field_polynomial_shift_bounded (x1)
  7. L70
    apply prime_field_polynomial_shift_bounded
  8. L71
    exact hp
  9. L72
    exact hb
  10. L73
    exact hu_witness_witness
14Use earlier factsL74–74

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

  1. L74
    exact hleft_witness_witness
15Establish hscale_boundsL75–84

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

  1. L75
    have hscale_bounds : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(x2,x3,L,p)Definitions: BetaPrefixInto(ab,ac,L,p)BetaPrefixInto(x2,x3,L,p)Original native command in the exact edition
  2. L76
    specialize prime_field_polynomial_scale_bounded (p)
  3. L77
    specialize prime_field_polynomial_scale_bounded (c)
  4. L78
    specialize prime_field_polynomial_scale_bounded (ab)
  5. L79
    specialize prime_field_polynomial_scale_bounded (ac)
  6. L80
    specialize prime_field_polynomial_scale_bounded (x2)
  7. L81
    specialize prime_field_polynomial_scale_bounded (x3)
  8. L82
    specialize prime_field_polynomial_scale_bounded (L)
  9. L83
    apply prime_field_polynomial_scale_bounded
  10. L84
    exact hv_witness_witness
16Separate the logical casesL85–85

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

  1. L85
    cases hscale_bounds
17Establish hright_boundL86–95

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

  1. L86
    have hright_bound : BetaPrefixInto(x6,x7,S N + L,p)Definitions: BetaPrefixInto(x6,x7,S N + L,p)Original native command in the exact edition
  2. L87
    specialize prime_field_polynomial_left_pad_bounded (p)
  3. L88
    specialize prime_field_polynomial_left_pad_bounded (x2)
  4. L89
    specialize prime_field_polynomial_left_pad_bounded (x3)
  5. L90
    specialize prime_field_polynomial_left_pad_bounded (L)
  6. L91
    specialize prime_field_polynomial_left_pad_bounded (S N)
  7. L92
    specialize prime_field_polynomial_left_pad_bounded (x6)
  8. L93
    specialize prime_field_polynomial_left_pad_bounded (x7)
  9. L94
    apply prime_field_polynomial_left_pad_bounded
  10. L95
    exact hp
18Use earlier factsL96–97

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

  1. L96
    exact hscale_bounds_right
  2. L97
    exact hright_witness_witness
19Establish hcommL98–102

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

  1. L98
    have hcomm : S N+L=L+S N
  2. L99
    specialize add_comm (S N)
  3. L100
    specialize add_comm (L)
  4. L101
    apply add_comm
  5. L102
    rewrite hcomm at hright_bound
20Establish hsumL103–112

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

  1. L103
    have hsum : ∃ rb. ∃ rc. FpPolyAdd(p,x4,x5,x6,x7,rb,rc,L + S N)Definitions: FpPolyAdd(p,x4,x5,x6,x7,rb,rc,L + S N)Original native command in the exact edition
  2. L104
    specialize prime_field_polynomial_add_exists (p)
  3. L105
    specialize prime_field_polynomial_add_exists (x4)
  4. L106
    specialize prime_field_polynomial_add_exists (x5)
  5. L107
    specialize prime_field_polynomial_add_exists (x6)
  6. L108
    specialize prime_field_polynomial_add_exists (x7)
  7. L109
    specialize prime_field_polynomial_add_exists (L+S N)
  8. L110
    apply prime_field_polynomial_add_exists
  9. L111
    exact hp0
  10. L112
    exact hleft_bound
21Use earlier factsL113–113

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

  1. L113
    exact hright_bound
22Separate the logical casesL114–115

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

  1. L114
    cases hsum
  2. L115
    cases hsum_witness
23Construct an explicit witnessL116–125

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

  1. L116
    exists x
  2. L117
    exists x1
  3. L118
    exists x2
  4. L119
    exists x3
  5. L120
    exists x4
  6. L121
    exists x5
  7. L122
    exists x6
  8. L123
    exists x7
  9. L124
    exists x8
  10. L125
    exists x9
24Separate the logical casesL126–126

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

  1. L126
    split
25Use earlier factsL127–127

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

  1. L127
    exact hu_witness_witness
26Separate the logical casesL128–128

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

  1. L128
    split
27Use earlier factsL129–129

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

  1. L129
    exact hv_witness_witness
28Separate the logical casesL130–130

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

  1. L130
    split
29Use earlier factsL131–131

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

  1. L131
    exact hleft_witness_witness
30Separate the logical casesL132–132

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

  1. L132
    split
31Use earlier factsL133–134

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

  1. L133
    exact hright_witness_witness
  2. L134
    exact hsum_witness_witness

Library-wide reading audit

Original defined command ledger · 134 lines
  1. 0001intro p
  2. 0002intro c
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro L
  6. 0006intro pb
  7. 0007intro pc
  8. 0008intro N
  9. 0009intro hp
  10. 0010intro hc
  11. 0011intro ha
  12. 0012intro hb
  13. 0013have hp0 : ~(p=0)
  14. 0014intro hz
  15. 0015specialize prime_nonzero (p)
  16. 0016apply prime_nonzero
  17. 0017exact hp
  18. 0018exact hz
  19. 0019have hu : ∃ ub. ∃ uc. PolynomialShift(pb,pc,N,ub,uc)
  20. 0020specialize prime_field_polynomial_shift_exists (pb)
  21. 0021specialize prime_field_polynomial_shift_exists (pc)
  22. 0022specialize prime_field_polynomial_shift_exists (N)
  23. 0023apply prime_field_polynomial_shift_exists
  24. 0024cases hu
  25. 0025cases hu_witness
  26. 0026have hv : ∃ vb. ∃ vc. FpPolyScale(p,c,ab,ac,vb,vc,L)
  27. 0027specialize prime_field_polynomial_scale_exists (p)
  28. 0028specialize prime_field_polynomial_scale_exists (c)
  29. 0029specialize prime_field_polynomial_scale_exists (ab)
  30. 0030specialize prime_field_polynomial_scale_exists (ac)
  31. 0031specialize prime_field_polynomial_scale_exists (L)
  32. 0032apply prime_field_polynomial_scale_exists
  33. 0033exact hp0
  34. 0034exact hc
  35. 0035exact ha
  36. 0036cases hv
  37. 0037cases hv_witness
  38. 0038have hleft : ∃ UB. ∃ UC. PolynomialLeftPad(x,x1,S N,L,UB,UC)
  39. 0039specialize prime_field_polynomial_left_pad_exists (x)
  40. 0040specialize prime_field_polynomial_left_pad_exists (x1)
  41. 0041specialize prime_field_polynomial_left_pad_exists (L)
  42. 0042specialize prime_field_polynomial_left_pad_exists (S N)
  43. 0043apply prime_field_polynomial_left_pad_exists
  44. 0044cases hleft
  45. 0045cases hleft_witness
  46. 0046have hright : ∃ VB. ∃ VC. PolynomialLeftPad(x2,x3,L,S N,VB,VC)
  47. 0047specialize prime_field_polynomial_left_pad_exists (x2)
  48. 0048specialize prime_field_polynomial_left_pad_exists (x3)
  49. 0049specialize prime_field_polynomial_left_pad_exists (S N)
  50. 0050specialize prime_field_polynomial_left_pad_exists (L)
  51. 0051apply prime_field_polynomial_left_pad_exists
  52. 0052cases hright
  53. 0053cases hright_witness
  54. 0054have hleft_bound : BetaPrefixInto(x4,x5,L + S N,p)
  55. 0055specialize prime_field_polynomial_left_pad_bounded (p)
  56. 0056specialize prime_field_polynomial_left_pad_bounded (x)
  57. 0057specialize prime_field_polynomial_left_pad_bounded (x1)
  58. 0058specialize prime_field_polynomial_left_pad_bounded (S N)
  59. 0059specialize prime_field_polynomial_left_pad_bounded (L)
  60. 0060specialize prime_field_polynomial_left_pad_bounded (x4)
  61. 0061specialize prime_field_polynomial_left_pad_bounded (x5)
  62. 0062apply prime_field_polynomial_left_pad_bounded
  63. 0063exact hp
  64. 0064specialize prime_field_polynomial_shift_bounded (p)
  65. 0065specialize prime_field_polynomial_shift_bounded (pb)
  66. 0066specialize prime_field_polynomial_shift_bounded (pc)
  67. 0067specialize prime_field_polynomial_shift_bounded (N)
  68. 0068specialize prime_field_polynomial_shift_bounded (x)
  69. 0069specialize prime_field_polynomial_shift_bounded (x1)
  70. 0070apply prime_field_polynomial_shift_bounded
  71. 0071exact hp
  72. 0072exact hb
  73. 0073exact hu_witness_witness
  74. 0074exact hleft_witness_witness
  75. 0075have hscale_bounds : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(x2,x3,L,p)
  76. 0076specialize prime_field_polynomial_scale_bounded (p)
  77. 0077specialize prime_field_polynomial_scale_bounded (c)
  78. 0078specialize prime_field_polynomial_scale_bounded (ab)
  79. 0079specialize prime_field_polynomial_scale_bounded (ac)
  80. 0080specialize prime_field_polynomial_scale_bounded (x2)
  81. 0081specialize prime_field_polynomial_scale_bounded (x3)
  82. 0082specialize prime_field_polynomial_scale_bounded (L)
  83. 0083apply prime_field_polynomial_scale_bounded
  84. 0084exact hv_witness_witness
  85. 0085cases hscale_bounds
  86. 0086have hright_bound : BetaPrefixInto(x6,x7,S N + L,p)
  87. 0087specialize prime_field_polynomial_left_pad_bounded (p)
  88. 0088specialize prime_field_polynomial_left_pad_bounded (x2)
  89. 0089specialize prime_field_polynomial_left_pad_bounded (x3)
  90. 0090specialize prime_field_polynomial_left_pad_bounded (L)
  91. 0091specialize prime_field_polynomial_left_pad_bounded (S N)
  92. 0092specialize prime_field_polynomial_left_pad_bounded (x6)
  93. 0093specialize prime_field_polynomial_left_pad_bounded (x7)
  94. 0094apply prime_field_polynomial_left_pad_bounded
  95. 0095exact hp
  96. 0096exact hscale_bounds_right
  97. 0097exact hright_witness_witness
  98. 0098have hcomm : S N+L=L+S N
  99. 0099specialize add_comm (S N)
  100. 0100specialize add_comm (L)
  101. 0101apply add_comm
  102. 0102rewrite hcomm at hright_bound
  103. 0103have hsum : ∃ rb. ∃ rc. FpPolyAdd(p,x4,x5,x6,x7,rb,rc,L + S N)
  104. 0104specialize prime_field_polynomial_add_exists (p)
  105. 0105specialize prime_field_polynomial_add_exists (x4)
  106. 0106specialize prime_field_polynomial_add_exists (x5)
  107. 0107specialize prime_field_polynomial_add_exists (x6)
  108. 0108specialize prime_field_polynomial_add_exists (x7)
  109. 0109specialize prime_field_polynomial_add_exists (L+S N)
  110. 0110apply prime_field_polynomial_add_exists
  111. 0111exact hp0
  112. 0112exact hleft_bound
  113. 0113exact hright_bound
  114. 0114cases hsum
  115. 0115cases hsum_witness
  116. 0116exists x
  117. 0117exists x1
  118. 0118exists x2
  119. 0119exists x3
  120. 0120exists x4
  121. 0121exists x5
  122. 0122exists x6
  123. 0123exists x7
  124. 0124exists x8
  125. 0125exists x9
  126. 0126split
  127. 0127exact hu_witness_witness
  128. 0128split
  129. 0129exact hv_witness_witness
  130. 0130split
  131. 0131exact hleft_witness_witness
  132. 0132split
  133. 0133exact hright_witness_witness
  134. 0134exact hsum_witness_witness