PX002E

prime_field_polynomial_quotient_prefix_exists

Construct every quotient coefficient with actual sum, subtraction, inverse-scaling and beta-extension witnesses, by ordinary finite induction.

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

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ M. ∀ N. Prime(p) → Lt(k,p) → BetaPrefixInto(ab,ac,N,p) → ∃ x. ∃ y. FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,x,y,N)

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

Definition DAG

FpAdd(p,a,b,c) · 1FpMul(p,a,b,c) · 1BetaPrefixInto(b,c,l,B) · 1BetaPrefixEqual(b,c,d,e,l) · 1FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) · 1FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N) · 2Lt(a,b) · 2Prime(p) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_quotient_prefix_emptyle_succ · checked external prerequisitele_refl · checked external prerequisiteprime_field_convolution_coefficient_exists · checked external prerequisiteprime_nonzero · checked external prerequisiteprime_field_subtract_exists · checked external prerequisiteprime_field_convolution_coefficient_bounded · checked external prerequisiteprime_field_multiply_exists · checked external prerequisitebeta_prefix_extend · checked external prerequisiteprime_field_polynomial_quotient_prefix_append
Original expanded first-order statement 
forall p k ab ac bb bc M N. (~((p) = 1) /\ forall pfa_factor_left_division_exists_prime pfa_factor_right_division_exists_prime. (p) = pfa_factor_left_division_exists_prime * pfa_factor_right_division_exists_prime -> pfa_factor_left_division_exists_prime = 1 \/ pfa_factor_right_division_exists_prime = 1) -> (exists pfa_gap_division_exists_scalar. pfa_gap_division_exists_scalar + S (k) = (p)) -> (forall fom_index_pfp_division_exists_source. (exists fom_gap_pfp_division_exists_source_index_bound. fom_gap_pfp_division_exists_source_index_bound + S (fom_index_pfp_division_exists_source) = N) -> exists fom_value_pfp_division_exists_source. ((((exists fom_beta_height_pfp_division_exists_source_entry. fom_beta_height_pfp_division_exists_source_entry + S (fom_value_pfp_division_exists_source) = S ((S (fom_index_pfp_division_exists_source)) * ac)) /\ exists fom_beta_quotient_pfp_division_exists_source_entry. ab = fom_beta_quotient_pfp_division_exists_source_entry * S ((S (fom_index_pfp_division_exists_source)) * ac) + (fom_value_pfp_division_exists_source))) /\ (exists fom_gap_pfp_division_exists_source_value_bound. fom_gap_pfp_division_exists_source_value_bound + S (fom_value_pfp_division_exists_source) = p))) -> exists qb qc. (forall pfd_index_division_exists_result. (exists pfa_gap_division_exists_resultbound. pfa_gap_division_exists_resultbound + S (pfd_index_division_exists_result) = (N)) -> exists pfd_value_division_exists_result. ((((exists ff_h_pfp_division_exists_resultentry. ff_h_pfp_division_exists_resultentry + S (pfd_value_division_exists_result) = S ((S (pfd_index_division_exists_result)) * qc)) /\ exists ff_q_pfp_division_exists_resultentry. qb = ff_q_pfp_division_exists_resultentry * S ((S (pfd_index_division_exists_result)) * qc) + (pfd_value_division_exists_result))) /\ ((exists pfd_input_division_exists_resultstep pfd_previous_division_exists_resultstep pfd_difference_division_exists_resultstep. ((((exists ff_h_pfp_division_exists_resultstepinput. ff_h_pfp_division_exists_resultstepinput + S (pfd_input_division_exists_resultstep) = S ((S (pfd_index_division_exists_result)) * ac)) /\ exists ff_q_pfp_division_exists_resultstepinput. ab = ff_q_pfp_division_exists_resultstepinput * S ((S (pfd_index_division_exists_result)) * ac) + (pfd_input_division_exists_resultstep))) /\ (((exists pfc_terms_code_division_exists_resultstepprevious pfc_terms_scale_division_exists_resultstepprevious pfc_natural_sum_division_exists_resultstepprevious. ((forall pfc_index_division_exists_resultsteppreviousdiagonal. (exists pfa_gap_division_exists_resultsteppreviousdiagonalbound. pfa_gap_division_exists_resultsteppreviousdiagonalbound + S (pfc_index_division_exists_resultsteppreviousdiagonal) = (S (pfd_index_division_exists_result))) -> exists pfc_value_division_exists_resultsteppreviousdiagonal. ((((exists ff_h_pfp_division_exists_resultsteppreviousdiagonalentry. ff_h_pfp_division_exists_resultsteppreviousdiagonalentry + S (pfc_value_division_exists_resultsteppreviousdiagonal) = S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * pfc_terms_scale_division_exists_resultstepprevious)) /\ exists ff_q_pfp_division_exists_resultsteppreviousdiagonalentry. pfc_terms_code_division_exists_resultstepprevious = ff_q_pfp_division_exists_resultsteppreviousdiagonalentry * S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * pfc_terms_scale_division_exists_resultstepprevious) + (pfc_value_division_exists_resultsteppreviousdiagonal))) /\ ((exists pfc_complement_division_exists_resultsteppreviousdiagonalterm pfc_left_division_exists_resultsteppreviousdiagonalterm pfc_right_division_exists_resultsteppreviousdiagonalterm. (((pfc_index_division_exists_resultsteppreviousdiagonal)+pfc_complement_division_exists_resultsteppreviousdiagonalterm=(pfd_index_division_exists_result)) /\ ((((((exists pfa_gap_division_exists_resultsteppreviousdiagonaltermleftinside. pfa_gap_division_exists_resultsteppreviousdiagonaltermleftinside + S (pfc_index_division_exists_resultsteppreviousdiagonal) = (pfd_index_division_exists_result)) /\ ((((exists ff_h_pfp_division_exists_resultsteppreviousdiagonaltermleftentry. ff_h_pfp_division_exists_resultsteppreviousdiagonaltermleftentry + S (pfc_left_division_exists_resultsteppreviousdiagonalterm) = S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_exists_resultsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_exists_resultsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_exists_resultsteppreviousdiagonal)) * qc) + (pfc_left_division_exists_resultsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_resultsteppreviousdiagonaltermleftoutside. pfc_gap_division_exists_resultsteppreviousdiagonaltermleftoutside+(pfd_index_division_exists_result)=(pfc_index_division_exists_resultsteppreviousdiagonal)) /\ (((pfc_left_division_exists_resultsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_exists_resultsteppreviousdiagonaltermrightinside. pfa_gap_division_exists_resultsteppreviousdiagonaltermrightinside + S (pfc_complement_division_exists_resultsteppreviousdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_division_exists_resultsteppreviousdiagonaltermrightentry. ff_h_pfp_division_exists_resultsteppreviousdiagonaltermrightentry + S (pfc_right_division_exists_resultsteppreviousdiagonalterm) = S ((S (pfc_complement_division_exists_resultsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_exists_resultsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_exists_resultsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_exists_resultsteppreviousdiagonalterm)) * bc) + (pfc_right_division_exists_resultsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_exists_resultsteppreviousdiagonaltermrightoutside. pfc_gap_division_exists_resultsteppreviousdiagonaltermrightoutside+(M)=(pfc_complement_division_exists_resultsteppreviousdiagonalterm)) /\ (((pfc_right_division_exists_resultsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_exists_resultsteppreviousdiagonal)=pfc_left_division_exists_resultsteppreviousdiagonalterm*pfc_right_division_exists_resultsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_exists_resultstepprevioussum fs_v_pfc_division_exists_resultstepprevioussum. ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_start. fs_h_pfc_division_exists_resultstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_start. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_exists_resultstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_terminal. fs_h_pfc_division_exists_resultstepprevioussum_body_terminal + S (pfc_natural_sum_division_exists_resultstepprevious) = S ((S (S (pfd_index_division_exists_result))) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_terminal. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_terminal * S ((S (S (pfd_index_division_exists_result))) * fs_v_pfc_division_exists_resultstepprevioussum) + (pfc_natural_sum_division_exists_resultstepprevious))) /\ forall fs_i_pfc_division_exists_resultstepprevioussum_body_steps. (exists fs_lt_pfc_division_exists_resultstepprevioussum_body_steps_bound. fs_lt_pfc_division_exists_resultstepprevioussum_body_steps_bound + S fs_i_pfc_division_exists_resultstepprevioussum_body_steps = S (pfd_index_division_exists_result)) -> exists fs_a_pfc_division_exists_resultstepprevioussum_body_steps fs_r_pfc_division_exists_resultstepprevioussum_body_steps fs_s_pfc_division_exists_resultstepprevioussum_body_steps. ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_steps_summand. fs_h_pfc_division_exists_resultstepprevioussum_body_steps_summand + S (fs_a_pfc_division_exists_resultstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * pfc_terms_scale_division_exists_resultstepprevious)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_steps_summand. pfc_terms_code_division_exists_resultstepprevious = fs_q_pfc_division_exists_resultstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * pfc_terms_scale_division_exists_resultstepprevious) + (fs_a_pfc_division_exists_resultstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_steps_partial. fs_h_pfc_division_exists_resultstepprevioussum_body_steps_partial + S (fs_r_pfc_division_exists_resultstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_steps_partial. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum) + (fs_r_pfc_division_exists_resultstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_exists_resultstepprevioussum_body_steps_successor. fs_h_pfc_division_exists_resultstepprevioussum_body_steps_successor + S (fs_s_pfc_division_exists_resultstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum)) /\ exists fs_q_pfc_division_exists_resultstepprevioussum_body_steps_successor. fs_u_pfc_division_exists_resultstepprevioussum = fs_q_pfc_division_exists_resultstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_exists_resultstepprevioussum_body_steps)) * fs_v_pfc_division_exists_resultstepprevioussum) + (fs_s_pfc_division_exists_resultstepprevioussum_body_steps))) /\ fs_s_pfc_division_exists_resultstepprevioussum_body_steps = fs_r_pfc_division_exists_resultstepprevioussum_body_steps + fs_a_pfc_division_exists_resultstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_exists_resultsteppreviousresiduebound. pfa_gap_division_exists_resultsteppreviousresiduebound + S (pfd_previous_division_exists_resultstep) = (p)) /\ ((exists pfa_offset_left_division_exists_resultsteppreviousresiduecongruence pfa_offset_right_division_exists_resultsteppreviousresiduecongruence. (pfc_natural_sum_division_exists_resultstepprevious) + (p) * pfa_offset_left_division_exists_resultsteppreviousresiduecongruence = (pfd_previous_division_exists_resultstep) + (p) * pfa_offset_right_division_exists_resultsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_exists_resultstepsubtractleft. pfa_gap_division_exists_resultstepsubtractleft + S (pfd_previous_division_exists_resultstep) = (p)) /\ (((exists pfa_gap_division_exists_resultstepsubtractright. pfa_gap_division_exists_resultstepsubtractright + S (pfd_difference_division_exists_resultstep) = (p)) /\ ((((exists pfa_gap_division_exists_resultstepsubtractresultbound. pfa_gap_division_exists_resultstepsubtractresultbound + S (pfd_input_division_exists_resultstep) = (p)) /\ ((exists pfa_offset_left_division_exists_resultstepsubtractresultcongruence pfa_offset_right_division_exists_resultstepsubtractresultcongruence. ((pfd_previous_division_exists_resultstep) + (pfd_difference_division_exists_resultstep)) + (p) * pfa_offset_left_division_exists_resultstepsubtractresultcongruence = (pfd_input_division_exists_resultstep) + (p) * pfa_offset_right_division_exists_resultstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_exists_resultstepmultiplyleft. pfa_gap_division_exists_resultstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_exists_resultstepmultiplyright. pfa_gap_division_exists_resultstepmultiplyright + S (pfd_difference_division_exists_resultstep) = (p)) /\ ((((exists pfa_gap_division_exists_resultstepmultiplyresultbound. pfa_gap_division_exists_resultstepmultiplyresultbound + S (pfd_value_division_exists_result) = (p)) /\ ((exists pfa_offset_left_division_exists_resultstepmultiplyresultcongruence pfa_offset_right_division_exists_resultstepmultiplyresultcongruence. ((k) * (pfd_difference_division_exists_resultstep)) + (p) * pfa_offset_left_division_exists_resultstepmultiplyresultcongruence = (pfd_value_division_exists_result) + (p) * pfa_offset_right_division_exists_resultstepmultiplyresultcongruence)))))))))))))))))))

Complete tactic proof in conservative notation

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

128 script commands · 32 reading checkpoints · 6 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 quotient prefix emptyprime field polynomial quotient prefix append
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro N
  9. L9
    intro hp
  10. L10
    intro hk
02Induction on NL11–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L11
    induction N
  2. L12
    intro ha
03Construct an explicit witnessL13–14

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

  1. L13
    exists 0
  2. L14
    exists 0
04Use earlier factsL15–24

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

  1. L15
    specialize prime_field_polynomial_quotient_prefix_empty (p)
  2. L16
    specialize prime_field_polynomial_quotient_prefix_empty (k)
  3. L17
    specialize prime_field_polynomial_quotient_prefix_empty (ab)
  4. L18
    specialize prime_field_polynomial_quotient_prefix_empty (ac)
  5. L19
    specialize prime_field_polynomial_quotient_prefix_empty (bb)
  6. L20
    specialize prime_field_polynomial_quotient_prefix_empty (bc)
  7. L21
    specialize prime_field_polynomial_quotient_prefix_empty (M)
  8. L22
    specialize prime_field_polynomial_quotient_prefix_empty (0)
  9. L23
    specialize prime_field_polynomial_quotient_prefix_empty (0)
  10. L24
    apply prime_field_polynomial_quotient_prefix_empty
05Fix variables and assumptionsL25–25

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

  1. L25
    intro ha
06Establish holdL26–35

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

  1. L26
    have hold : ∃ qb. ∃ qc. FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)Definitions: FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)Original native command in the exact edition
  2. L27
    apply IH
  3. L28
    intro i
  4. L29
    intro hi
  5. L30
    specialize ha (i)
  6. L31
    apply ha
  7. L32
    specialize le_succ (S i)
  8. L33
    specialize le_succ (N)
  9. L34
    apply le_succ
  10. L35
    exact hi
07Separate the logical casesL36–37

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

  1. L36
    cases hold
  2. L37
    cases hold_witness
08Establish hinputL38–42

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

  1. L38
    have hinput : ∃ a. BetaAt(ab,ac,N,a) ∧ Lt(a,p)Definitions: BetaAt(ab,ac,N,a)Lt(a,p)Original native command in the exact edition
  2. L39
    specialize ha (N)
  3. L40
    apply ha
  4. L41
    specialize le_refl (S N)
  5. L42
    apply le_refl
09Separate the logical casesL43–44

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

  1. L43
    cases hinput
  2. L44
    cases hinput_witness
10Establish hcL45–54

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

  1. L45
    have hc : ∃ c. FpConvolutionCoefficient(p,x,x1,N,bb,bc,M,N,c)Definitions: FpConvolutionCoefficient(p,x,x1,N,bb,bc,M,N,c)Original native command in the exact edition
  2. L46
    specialize prime_field_convolution_coefficient_exists (p)
  3. L47
    specialize prime_field_convolution_coefficient_exists (x)
  4. L48
    specialize prime_field_convolution_coefficient_exists (x1)
  5. L49
    specialize prime_field_convolution_coefficient_exists (N)
  6. L50
    specialize prime_field_convolution_coefficient_exists (bb)
  7. L51
    specialize prime_field_convolution_coefficient_exists (bc)
  8. L52
    specialize prime_field_convolution_coefficient_exists (M)
  9. L53
    specialize prime_field_convolution_coefficient_exists (N)
  10. L54
    apply prime_field_convolution_coefficient_exists
11Fix variables and assumptionsL55–55

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

  1. L55
    intro hz
12Use earlier factsL56–59

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

  1. L56
    specialize prime_nonzero (p)
  2. L57
    apply prime_nonzero
  3. L58
    exact hp
  4. L59
    exact hz
13Separate the logical casesL60–60

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

  1. L60
    cases hc
14Establish hsL61–70

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

  1. L61
    have hs : ∃ s. FpAdd(p,x3,s,x2)Definitions: FpAdd(p,x3,s,x2)Original native command in the exact edition
  2. L62
    specialize prime_field_subtract_exists (p)
  3. L63
    specialize prime_field_subtract_exists (x2)
  4. L64
    specialize prime_field_subtract_exists (x3)
  5. L65
    apply prime_field_subtract_exists
  6. L66
    exact hp
  7. L67
    exact hinput_witness_right
  8. L68
    specialize prime_field_convolution_coefficient_bounded (p)
  9. L69
    specialize prime_field_convolution_coefficient_bounded (x)
  10. L70
    specialize prime_field_convolution_coefficient_bounded (x1)
15Use earlier factsL71–78

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

  1. L71
    specialize prime_field_convolution_coefficient_bounded (N)
  2. L72
    specialize prime_field_convolution_coefficient_bounded (bb)
  3. L73
    specialize prime_field_convolution_coefficient_bounded (bc)
  4. L74
    specialize prime_field_convolution_coefficient_bounded (M)
  5. L75
    specialize prime_field_convolution_coefficient_bounded (N)
  6. L76
    specialize prime_field_convolution_coefficient_bounded (x3)
  7. L77
    apply prime_field_convolution_coefficient_bounded
  8. L78
    exact hc_witness
16Separate the logical casesL79–79

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

  1. L79
    cases hs
17Establish hqL80–86

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

  1. L80
    have hq : ∃ q. FpMul(p,k,x4,q)Definitions: FpMul(p,k,x4,q)Original native command in the exact edition
  2. L81
    specialize prime_field_multiply_exists (p)
  3. L82
    specialize prime_field_multiply_exists (k)
  4. L83
    specialize prime_field_multiply_exists (x4)
  5. L84
    apply prime_field_multiply_exists
  6. L85
    exact hp
  7. L86
    exact hk
18Separate the logical casesL87–88

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

  1. L87
    cases hs_witness
  2. L88
    cases hs_witness_right
19Use earlier factsL89–89

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

  1. L89
    exact hs_witness_right_left
20Separate the logical casesL90–90

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

  1. L90
    cases hq
21Establish hnewL91–96

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

  1. L91
    have hnew : ∃ QB. ∃ QC. BetaAt(QB,QC,N,x5) ∧ BetaPrefixEqual(x,x1,QB,QC,N)Definitions: BetaAt(QB,QC,N,x5)BetaPrefixEqual(x,x1,QB,QC,N)Original native command in the exact edition
  2. L92
    specialize beta_prefix_extend (N)
  3. L93
    specialize beta_prefix_extend (x)
  4. L94
    specialize beta_prefix_extend (x1)
  5. L95
    specialize beta_prefix_extend (x5)
  6. L96
    apply beta_prefix_extend
22Separate the logical casesL97–99

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

  1. L97
    cases hnew
  2. L98
    cases hnew_witness
  3. L99
    cases hnew_witness_witness
23Construct an explicit witnessL100–101

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

  1. L100
    exists x6
  2. L101
    exists x7
24Use earlier factsL102–111

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

  1. L102
    specialize prime_field_polynomial_quotient_prefix_append (p)
  2. L103
    specialize prime_field_polynomial_quotient_prefix_append (k)
  3. L104
    specialize prime_field_polynomial_quotient_prefix_append (ab)
  4. L105
    specialize prime_field_polynomial_quotient_prefix_append (ac)
  5. L106
    specialize prime_field_polynomial_quotient_prefix_append (bb)
  6. L107
    specialize prime_field_polynomial_quotient_prefix_append (bc)
  7. L108
    specialize prime_field_polynomial_quotient_prefix_append (M)
  8. L109
    specialize prime_field_polynomial_quotient_prefix_append (x)
  9. L110
    specialize prime_field_polynomial_quotient_prefix_append (x1)
  10. L111
    specialize prime_field_polynomial_quotient_prefix_append (x6)
25Use earlier factsL112–118

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

  1. L112
    specialize prime_field_polynomial_quotient_prefix_append (x7)
  2. L113
    specialize prime_field_polynomial_quotient_prefix_append (N)
  3. L114
    specialize prime_field_polynomial_quotient_prefix_append (x5)
  4. L115
    apply prime_field_polynomial_quotient_prefix_append
  5. L116
    exact hold_witness_witness
  6. L117
    exact hnew_witness_witness_right
  7. L118
    exact hnew_witness_witness_left
26Construct an explicit witnessL119–121

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

  1. L119
    exists x2
  2. L120
    exists x3
  3. L121
    exists x4
27Separate the logical casesL122–122

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

  1. L122
    split
28Use earlier factsL123–123

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

  1. L123
    exact hinput_witness_left
29Separate the logical casesL124–124

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

  1. L124
    split
30Use earlier factsL125–125

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

  1. L125
    exact hc_witness
31Separate the logical casesL126–126

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

  1. L126
    split
32Use earlier factsL127–128

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

  1. L127
    exact hs_witness
  2. L128
    exact hq_witness

Library-wide reading audit

Original defined command ledger · 128 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro N
  9. 0009intro hp
  10. 0010intro hk
  11. 0011induction N
  12. 0012intro ha
  13. 0013exists 0
  14. 0014exists 0
  15. 0015specialize prime_field_polynomial_quotient_prefix_empty (p)
  16. 0016specialize prime_field_polynomial_quotient_prefix_empty (k)
  17. 0017specialize prime_field_polynomial_quotient_prefix_empty (ab)
  18. 0018specialize prime_field_polynomial_quotient_prefix_empty (ac)
  19. 0019specialize prime_field_polynomial_quotient_prefix_empty (bb)
  20. 0020specialize prime_field_polynomial_quotient_prefix_empty (bc)
  21. 0021specialize prime_field_polynomial_quotient_prefix_empty (M)
  22. 0022specialize prime_field_polynomial_quotient_prefix_empty (0)
  23. 0023specialize prime_field_polynomial_quotient_prefix_empty (0)
  24. 0024apply prime_field_polynomial_quotient_prefix_empty
  25. 0025intro ha
  26. 0026have hold : ∃ qb. ∃ qc. FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N)
  27. 0027apply IH
  28. 0028intro i
  29. 0029intro hi
  30. 0030specialize ha (i)
  31. 0031apply ha
  32. 0032specialize le_succ (S i)
  33. 0033specialize le_succ (N)
  34. 0034apply le_succ
  35. 0035exact hi
  36. 0036cases hold
  37. 0037cases hold_witness
  38. 0038have hinput : ∃ a. BetaAt(ab,ac,N,a) ∧ Lt(a,p)
  39. 0039specialize ha (N)
  40. 0040apply ha
  41. 0041specialize le_refl (S N)
  42. 0042apply le_refl
  43. 0043cases hinput
  44. 0044cases hinput_witness
  45. 0045have hc : ∃ c. FpConvolutionCoefficient(p,x,x1,N,bb,bc,M,N,c)
  46. 0046specialize prime_field_convolution_coefficient_exists (p)
  47. 0047specialize prime_field_convolution_coefficient_exists (x)
  48. 0048specialize prime_field_convolution_coefficient_exists (x1)
  49. 0049specialize prime_field_convolution_coefficient_exists (N)
  50. 0050specialize prime_field_convolution_coefficient_exists (bb)
  51. 0051specialize prime_field_convolution_coefficient_exists (bc)
  52. 0052specialize prime_field_convolution_coefficient_exists (M)
  53. 0053specialize prime_field_convolution_coefficient_exists (N)
  54. 0054apply prime_field_convolution_coefficient_exists
  55. 0055intro hz
  56. 0056specialize prime_nonzero (p)
  57. 0057apply prime_nonzero
  58. 0058exact hp
  59. 0059exact hz
  60. 0060cases hc
  61. 0061have hs : ∃ s. FpAdd(p,x3,s,x2)
  62. 0062specialize prime_field_subtract_exists (p)
  63. 0063specialize prime_field_subtract_exists (x2)
  64. 0064specialize prime_field_subtract_exists (x3)
  65. 0065apply prime_field_subtract_exists
  66. 0066exact hp
  67. 0067exact hinput_witness_right
  68. 0068specialize prime_field_convolution_coefficient_bounded (p)
  69. 0069specialize prime_field_convolution_coefficient_bounded (x)
  70. 0070specialize prime_field_convolution_coefficient_bounded (x1)
  71. 0071specialize prime_field_convolution_coefficient_bounded (N)
  72. 0072specialize prime_field_convolution_coefficient_bounded (bb)
  73. 0073specialize prime_field_convolution_coefficient_bounded (bc)
  74. 0074specialize prime_field_convolution_coefficient_bounded (M)
  75. 0075specialize prime_field_convolution_coefficient_bounded (N)
  76. 0076specialize prime_field_convolution_coefficient_bounded (x3)
  77. 0077apply prime_field_convolution_coefficient_bounded
  78. 0078exact hc_witness
  79. 0079cases hs
  80. 0080have hq : ∃ q. FpMul(p,k,x4,q)
  81. 0081specialize prime_field_multiply_exists (p)
  82. 0082specialize prime_field_multiply_exists (k)
  83. 0083specialize prime_field_multiply_exists (x4)
  84. 0084apply prime_field_multiply_exists
  85. 0085exact hp
  86. 0086exact hk
  87. 0087cases hs_witness
  88. 0088cases hs_witness_right
  89. 0089exact hs_witness_right_left
  90. 0090cases hq
  91. 0091have hnew : ∃ QB. ∃ QC. BetaAt(QB,QC,N,x5) ∧ BetaPrefixEqual(x,x1,QB,QC,N)
  92. 0092specialize beta_prefix_extend (N)
  93. 0093specialize beta_prefix_extend (x)
  94. 0094specialize beta_prefix_extend (x1)
  95. 0095specialize beta_prefix_extend (x5)
  96. 0096apply beta_prefix_extend
  97. 0097cases hnew
  98. 0098cases hnew_witness
  99. 0099cases hnew_witness_witness
  100. 0100exists x6
  101. 0101exists x7
  102. 0102specialize prime_field_polynomial_quotient_prefix_append (p)
  103. 0103specialize prime_field_polynomial_quotient_prefix_append (k)
  104. 0104specialize prime_field_polynomial_quotient_prefix_append (ab)
  105. 0105specialize prime_field_polynomial_quotient_prefix_append (ac)
  106. 0106specialize prime_field_polynomial_quotient_prefix_append (bb)
  107. 0107specialize prime_field_polynomial_quotient_prefix_append (bc)
  108. 0108specialize prime_field_polynomial_quotient_prefix_append (M)
  109. 0109specialize prime_field_polynomial_quotient_prefix_append (x)
  110. 0110specialize prime_field_polynomial_quotient_prefix_append (x1)
  111. 0111specialize prime_field_polynomial_quotient_prefix_append (x6)
  112. 0112specialize prime_field_polynomial_quotient_prefix_append (x7)
  113. 0113specialize prime_field_polynomial_quotient_prefix_append (N)
  114. 0114specialize prime_field_polynomial_quotient_prefix_append (x5)
  115. 0115apply prime_field_polynomial_quotient_prefix_append
  116. 0116exact hold_witness_witness
  117. 0117exact hnew_witness_witness_right
  118. 0118exact hnew_witness_witness_left
  119. 0119exists x2
  120. 0120exists x3
  121. 0121exists x4
  122. 0122split
  123. 0123exact hinput_witness_left
  124. 0124split
  125. 0125exact hc_witness
  126. 0126split
  127. 0127exact hs_witness
  128. 0128exact hq_witness