PP002C

prime_field_polynomial_horner_successor_construct

Every actual canonical last multiply/add step extends an actual prefix to a full execution; the required coefficient bounds are derived, not assumed.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

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

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ t. ∀ l. ∀ a. ∀ h. ∀ k. ∀ r. Prime(p) → BetaAt(b,c,l,a) → FpHorner(p,b,c,t,l,h) → FpMul(p,h,t,k) → FpAdd(p,k,a,r) → FpHorner(p,b,c,t,S l,r)

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

Definition DAG

FpAdd(p,a,b,c) · 3FpMul(p,a,b,c) · 2BetaPrefixInto(b,c,l,B) · 2FpHorner(p,b,c,x,l,r) · 4Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_horner_input_boundsmatrix_rank_bounded_prefix_extend · checked external prerequisiteprime_field_polynomial_horner_existsprime_field_polynomial_horner_successor_decomposebeta_at_unique · checked external prerequisiteprime_field_polynomial_horner_functionalprime_field_multiply_functional · checked external prerequisiteprime_field_add_functional · checked external prerequisite
Original expanded first-order statement 
forall p b c t l a h k r. (~((p) = 1) /\ forall pfa_factor_left_successor_intro_prime pfa_factor_right_successor_intro_prime. (p) = pfa_factor_left_successor_intro_prime * pfa_factor_right_successor_intro_prime -> pfa_factor_left_successor_intro_prime = 1 \/ pfa_factor_right_successor_intro_prime = 1) -> (((exists ff_h_pfp_successor_intro_coefficient. ff_h_pfp_successor_intro_coefficient + S (a) = S ((S (l)) * c)) /\ exists ff_q_pfp_successor_intro_coefficient. b = ff_q_pfp_successor_intro_coefficient * S ((S (l)) * c) + (a))) -> (exists pfh_trace_code_successor_intro_prefix pfh_trace_scale_successor_intro_prefix. (((exists pfa_gap_successor_intro_prefixtracebase. pfa_gap_successor_intro_prefixtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_intro_prefixtraceinitial. ff_h_pfp_successor_intro_prefixtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_intro_prefix)) /\ exists ff_q_pfp_successor_intro_prefixtraceinitial. pfh_trace_code_successor_intro_prefix = ff_q_pfp_successor_intro_prefixtraceinitial * S ((S (0)) * pfh_trace_scale_successor_intro_prefix) + (0))) /\ (((((exists ff_h_pfp_successor_intro_prefixtraceterminal. ff_h_pfp_successor_intro_prefixtraceterminal + S (h) = S ((S (l)) * pfh_trace_scale_successor_intro_prefix)) /\ exists ff_q_pfp_successor_intro_prefixtraceterminal. pfh_trace_code_successor_intro_prefix = ff_q_pfp_successor_intro_prefixtraceterminal * S ((S (l)) * pfh_trace_scale_successor_intro_prefix) + (h))) /\ ((forall pfh_index_successor_intro_prefixtracesteps. (exists pfa_gap_successor_intro_prefixtracestepsindex. pfa_gap_successor_intro_prefixtracestepsindex + S (pfh_index_successor_intro_prefixtracesteps) = (l)) -> (exists pfh_coefficient_successor_intro_prefixtracestepsstep pfh_before_successor_intro_prefixtracestepsstep pfh_after_successor_intro_prefixtracestepsstep pfh_product_successor_intro_prefixtracestepsstep. ((((exists ff_h_pfp_successor_intro_prefixtracestepsstepcoefficient. ff_h_pfp_successor_intro_prefixtracestepsstepcoefficient + S (pfh_coefficient_successor_intro_prefixtracestepsstep) = S ((S (pfh_index_successor_intro_prefixtracesteps)) * c)) /\ exists ff_q_pfp_successor_intro_prefixtracestepsstepcoefficient. b = ff_q_pfp_successor_intro_prefixtracestepsstepcoefficient * S ((S (pfh_index_successor_intro_prefixtracesteps)) * c) + (pfh_coefficient_successor_intro_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_prefixtracestepsstepbefore. ff_h_pfp_successor_intro_prefixtracestepsstepbefore + S (pfh_before_successor_intro_prefixtracestepsstep) = S ((S (pfh_index_successor_intro_prefixtracesteps)) * pfh_trace_scale_successor_intro_prefix)) /\ exists ff_q_pfp_successor_intro_prefixtracestepsstepbefore. pfh_trace_code_successor_intro_prefix = ff_q_pfp_successor_intro_prefixtracestepsstepbefore * S ((S (pfh_index_successor_intro_prefixtracesteps)) * pfh_trace_scale_successor_intro_prefix) + (pfh_before_successor_intro_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_prefixtracestepsstepafter. ff_h_pfp_successor_intro_prefixtracestepsstepafter + S (pfh_after_successor_intro_prefixtracestepsstep) = S ((S (S (pfh_index_successor_intro_prefixtracesteps))) * pfh_trace_scale_successor_intro_prefix)) /\ exists ff_q_pfp_successor_intro_prefixtracestepsstepafter. pfh_trace_code_successor_intro_prefix = ff_q_pfp_successor_intro_prefixtracestepsstepafter * S ((S (S (pfh_index_successor_intro_prefixtracesteps))) * pfh_trace_scale_successor_intro_prefix) + (pfh_after_successor_intro_prefixtracestepsstep))) /\ (((((exists pfa_gap_successor_intro_prefixtracestepsstepmultiplyleft. pfa_gap_successor_intro_prefixtracestepsstepmultiplyleft + S (pfh_before_successor_intro_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_prefixtracestepsstepmultiplyright. pfa_gap_successor_intro_prefixtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_intro_prefixtracestepsstepmultiplyresultbound. pfa_gap_successor_intro_prefixtracestepsstepmultiplyresultbound + S (pfh_product_successor_intro_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_prefixtracestepsstepmultiplyresultcongruence pfa_offset_right_successor_intro_prefixtracestepsstepmultiplyresultcongruence. ((pfh_before_successor_intro_prefixtracestepsstep) * (t)) + (p) * pfa_offset_left_successor_intro_prefixtracestepsstepmultiplyresultcongruence = (pfh_product_successor_intro_prefixtracestepsstep) + (p) * pfa_offset_right_successor_intro_prefixtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_intro_prefixtracestepsstepaddleft. pfa_gap_successor_intro_prefixtracestepsstepaddleft + S (pfh_product_successor_intro_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_prefixtracestepsstepaddright. pfa_gap_successor_intro_prefixtracestepsstepaddright + S (pfh_coefficient_successor_intro_prefixtracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_intro_prefixtracestepsstepaddresultbound. pfa_gap_successor_intro_prefixtracestepsstepaddresultbound + S (pfh_after_successor_intro_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_prefixtracestepsstepaddresultcongruence pfa_offset_right_successor_intro_prefixtracestepsstepaddresultcongruence. ((pfh_product_successor_intro_prefixtracestepsstep) + (pfh_coefficient_successor_intro_prefixtracestepsstep)) + (p) * pfa_offset_left_successor_intro_prefixtracestepsstepaddresultcongruence = (pfh_after_successor_intro_prefixtracestepsstep) + (p) * pfa_offset_right_successor_intro_prefixtracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> (((exists pfa_gap_successor_intro_multiplyleft. pfa_gap_successor_intro_multiplyleft + S (h) = (p)) /\ (((exists pfa_gap_successor_intro_multiplyright. pfa_gap_successor_intro_multiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_intro_multiplyresultbound. pfa_gap_successor_intro_multiplyresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_successor_intro_multiplyresultcongruence pfa_offset_right_successor_intro_multiplyresultcongruence. ((h) * (t)) + (p) * pfa_offset_left_successor_intro_multiplyresultcongruence = (k) + (p) * pfa_offset_right_successor_intro_multiplyresultcongruence))))))))) -> (((exists pfa_gap_successor_intro_addleft. pfa_gap_successor_intro_addleft + S (k) = (p)) /\ (((exists pfa_gap_successor_intro_addright. pfa_gap_successor_intro_addright + S (a) = (p)) /\ ((((exists pfa_gap_successor_intro_addresultbound. pfa_gap_successor_intro_addresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_successor_intro_addresultcongruence pfa_offset_right_successor_intro_addresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_successor_intro_addresultcongruence = (r) + (p) * pfa_offset_right_successor_intro_addresultcongruence))))))))) -> (exists pfh_trace_code_successor_intro_execution pfh_trace_scale_successor_intro_execution. (((exists pfa_gap_successor_intro_executiontracebase. pfa_gap_successor_intro_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_intro_executiontraceinitial. ff_h_pfp_successor_intro_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_intro_execution)) /\ exists ff_q_pfp_successor_intro_executiontraceinitial. pfh_trace_code_successor_intro_execution = ff_q_pfp_successor_intro_executiontraceinitial * S ((S (0)) * pfh_trace_scale_successor_intro_execution) + (0))) /\ (((((exists ff_h_pfp_successor_intro_executiontraceterminal. ff_h_pfp_successor_intro_executiontraceterminal + S (r) = S ((S (S l)) * pfh_trace_scale_successor_intro_execution)) /\ exists ff_q_pfp_successor_intro_executiontraceterminal. pfh_trace_code_successor_intro_execution = ff_q_pfp_successor_intro_executiontraceterminal * S ((S (S l)) * pfh_trace_scale_successor_intro_execution) + (r))) /\ ((forall pfh_index_successor_intro_executiontracesteps. (exists pfa_gap_successor_intro_executiontracestepsindex. pfa_gap_successor_intro_executiontracestepsindex + S (pfh_index_successor_intro_executiontracesteps) = (S l)) -> (exists pfh_coefficient_successor_intro_executiontracestepsstep pfh_before_successor_intro_executiontracestepsstep pfh_after_successor_intro_executiontracestepsstep pfh_product_successor_intro_executiontracestepsstep. ((((exists ff_h_pfp_successor_intro_executiontracestepsstepcoefficient. ff_h_pfp_successor_intro_executiontracestepsstepcoefficient + S (pfh_coefficient_successor_intro_executiontracestepsstep) = S ((S (pfh_index_successor_intro_executiontracesteps)) * c)) /\ exists ff_q_pfp_successor_intro_executiontracestepsstepcoefficient. b = ff_q_pfp_successor_intro_executiontracestepsstepcoefficient * S ((S (pfh_index_successor_intro_executiontracesteps)) * c) + (pfh_coefficient_successor_intro_executiontracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_executiontracestepsstepbefore. ff_h_pfp_successor_intro_executiontracestepsstepbefore + S (pfh_before_successor_intro_executiontracestepsstep) = S ((S (pfh_index_successor_intro_executiontracesteps)) * pfh_trace_scale_successor_intro_execution)) /\ exists ff_q_pfp_successor_intro_executiontracestepsstepbefore. pfh_trace_code_successor_intro_execution = ff_q_pfp_successor_intro_executiontracestepsstepbefore * S ((S (pfh_index_successor_intro_executiontracesteps)) * pfh_trace_scale_successor_intro_execution) + (pfh_before_successor_intro_executiontracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_executiontracestepsstepafter. ff_h_pfp_successor_intro_executiontracestepsstepafter + S (pfh_after_successor_intro_executiontracestepsstep) = S ((S (S (pfh_index_successor_intro_executiontracesteps))) * pfh_trace_scale_successor_intro_execution)) /\ exists ff_q_pfp_successor_intro_executiontracestepsstepafter. pfh_trace_code_successor_intro_execution = ff_q_pfp_successor_intro_executiontracestepsstepafter * S ((S (S (pfh_index_successor_intro_executiontracesteps))) * pfh_trace_scale_successor_intro_execution) + (pfh_after_successor_intro_executiontracestepsstep))) /\ (((((exists pfa_gap_successor_intro_executiontracestepsstepmultiplyleft. pfa_gap_successor_intro_executiontracestepsstepmultiplyleft + S (pfh_before_successor_intro_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_executiontracestepsstepmultiplyright. pfa_gap_successor_intro_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_intro_executiontracestepsstepmultiplyresultbound. pfa_gap_successor_intro_executiontracestepsstepmultiplyresultbound + S (pfh_product_successor_intro_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_successor_intro_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_successor_intro_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_successor_intro_executiontracestepsstepmultiplyresultcongruence = (pfh_product_successor_intro_executiontracestepsstep) + (p) * pfa_offset_right_successor_intro_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_intro_executiontracestepsstepaddleft. pfa_gap_successor_intro_executiontracestepsstepaddleft + S (pfh_product_successor_intro_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_executiontracestepsstepaddright. pfa_gap_successor_intro_executiontracestepsstepaddright + S (pfh_coefficient_successor_intro_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_intro_executiontracestepsstepaddresultbound. pfa_gap_successor_intro_executiontracestepsstepaddresultbound + S (pfh_after_successor_intro_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_executiontracestepsstepaddresultcongruence pfa_offset_right_successor_intro_executiontracestepsstepaddresultcongruence. ((pfh_product_successor_intro_executiontracestepsstep) + (pfh_coefficient_successor_intro_executiontracestepsstep)) + (p) * pfa_offset_left_successor_intro_executiontracestepsstepaddresultcongruence = (pfh_after_successor_intro_executiontracestepsstep) + (p) * pfa_offset_right_successor_intro_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

112 script commands · 20 reading checkpoints · 9 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 (4)
prime field polynomial horner input boundsprime field polynomial horner existsprime field polynomial horner successor decomposeprime field polynomial horner functional
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro t
  5. L5
    intro l
  6. L6
    intro a
  7. L7
    intro h
  8. L8
    intro k
  9. L9
    intro r
  10. L10
    intro hp
02Fix variables and assumptionsL11–14

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

  1. L11
    intro ha
  2. L12
    intro hh
  3. L13
    intro hm
  4. L14
    intro hr
03Establish hboundsL15–23

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

  1. L15
    have hbounds : Lt(t,p) ∧ BetaPrefixInto(b,c,l,p)Definitions: Lt(t,p)BetaPrefixInto(b,c,l,p)Original native command in the exact edition
  2. L16
    specialize prime_field_polynomial_horner_input_bounds (p)
  3. L17
    specialize prime_field_polynomial_horner_input_bounds (b)
  4. L18
    specialize prime_field_polynomial_horner_input_bounds (c)
  5. L19
    specialize prime_field_polynomial_horner_input_bounds (t)
  6. L20
    specialize prime_field_polynomial_horner_input_bounds (l)
  7. L21
    specialize prime_field_polynomial_horner_input_bounds (h)
  8. L22
    apply prime_field_polynomial_horner_input_bounds
  9. L23
    exact hh
04Separate the logical casesL24–24

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

  1. L24
    cases hbounds
05Establish hrcopyL25–26

Establish this local claim before using it. It is not an additional assumption.

  1. L25
    have hrcopy : FpAdd(p,k,a,r)Definitions: FpAdd(p,k,a,r)Original native command in the exact edition
  2. L26
    exact hr
06Separate the logical casesL27–28

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

  1. L27
    cases hrcopy
  2. L28
    cases hrcopy_right
07Establish hcoeffL29–38

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

  1. L29
    have hcoeff : BetaPrefixInto(b,c,S l,p)Definitions: BetaPrefixInto(b,c,S l,p)Original native command in the exact edition
  2. L30
    specialize matrix_rank_bounded_prefix_extend (b)
  3. L31
    specialize matrix_rank_bounded_prefix_extend (c)
  4. L32
    specialize matrix_rank_bounded_prefix_extend (l)
  5. L33
    specialize matrix_rank_bounded_prefix_extend (p)
  6. L34
    specialize matrix_rank_bounded_prefix_extend (a)
  7. L35
    apply matrix_rank_bounded_prefix_extend
  8. L36
    exact hbounds_right
  9. L37
    exact ha
  10. L38
    exact hrcopy_right_left
08Establish heL39–48

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

  1. L39
    have he : ∃ s. FpHorner(p,b,c,t,S l,s)Definitions: FpHorner(p,b,c,t,S l,s)Original native command in the exact edition
  2. L40
    specialize prime_field_polynomial_horner_exists (p)
  3. L41
    specialize prime_field_polynomial_horner_exists (b)
  4. L42
    specialize prime_field_polynomial_horner_exists (c)
  5. L43
    specialize prime_field_polynomial_horner_exists (t)
  6. L44
    specialize prime_field_polynomial_horner_exists (S l)
  7. L45
    apply prime_field_polynomial_horner_exists
  8. L46
    exact hp
  9. L47
    exact hcoeff
  10. L48
    exact hbounds_left
09Separate the logical casesL49–49

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

  1. L49
    cases he
10Establish hsL50–58

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

  1. L50
    have hs : ∃ a. ∃ h. ∃ k. BetaAt(b,c,l,a) ∧ (FpHorner(p,b,c,t,l,h) ∧ (FpMul(p,h,t,k) ∧ FpAdd(p,k,a,x)))Definitions: BetaAt(b,c,l,a)FpHorner(p,b,c,t,l,h)FpMul(p,h,t,k)FpAdd(p,k,a,x)Original native command in the exact edition
  2. L51
    specialize prime_field_polynomial_horner_successor_decompose (p)
  3. L52
    specialize prime_field_polynomial_horner_successor_decompose (b)
  4. L53
    specialize prime_field_polynomial_horner_successor_decompose (c)
  5. L54
    specialize prime_field_polynomial_horner_successor_decompose (t)
  6. L55
    specialize prime_field_polynomial_horner_successor_decompose (l)
  7. L56
    specialize prime_field_polynomial_horner_successor_decompose (x)
  8. L57
    apply prime_field_polynomial_horner_successor_decompose
  9. L58
    exact he_witness
11Separate the logical casesL59–64

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

  1. L59
    cases hs
  2. L60
    cases hs_witness
  3. L61
    cases hs_witness_witness
  4. L62
    cases hs_witness_witness_witness
  5. L63
    cases hs_witness_witness_witness_right
  6. L64
    cases hs_witness_witness_witness_right_right
12Establish haeL65–73

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

  1. L65
    have hae : x1=a
  2. L66
    specialize beta_at_unique (b)
  3. L67
    specialize beta_at_unique (c)
  4. L68
    specialize beta_at_unique (l)
  5. L69
    specialize beta_at_unique (x1)
  6. L70
    specialize beta_at_unique (a)
  7. L71
    apply beta_at_unique
  8. L72
    exact hs_witness_witness_witness_left
  9. L73
    exact ha
13Establish hheL74–83

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

  1. L74
    have hhe : x2=h
  2. L75
    specialize prime_field_polynomial_horner_functional (p)
  3. L76
    specialize prime_field_polynomial_horner_functional (b)
  4. L77
    specialize prime_field_polynomial_horner_functional (c)
  5. L78
    specialize prime_field_polynomial_horner_functional (t)
  6. L79
    specialize prime_field_polynomial_horner_functional (l)
  7. L80
    specialize prime_field_polynomial_horner_functional (x2)
  8. L81
    specialize prime_field_polynomial_horner_functional (h)
  9. L82
    apply prime_field_polynomial_horner_functional
  10. L83
    exact hp
14Use earlier factsL84–85

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

  1. L84
    exact hs_witness_witness_witness_right_left
  2. L85
    exact hh
15Calculate and transport equalitiesL86–87

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L86
    rewrite hhe at hs_witness_witness_witness_right_right_left
  2. L87
    rewrite hhe at hs_witness_witness_witness_right_right_left
16Establish hkeL88–97

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

  1. L88
    have hke : x3=k
  2. L89
    specialize prime_field_multiply_functional (p)
  3. L90
    specialize prime_field_multiply_functional (h)
  4. L91
    specialize prime_field_multiply_functional (t)
  5. L92
    specialize prime_field_multiply_functional (x3)
  6. L93
    specialize prime_field_multiply_functional (k)
  7. L94
    apply prime_field_multiply_functional
  8. L95
    exact hs_witness_witness_witness_right_right_left
  9. L96
    exact hm
  10. L97
    rewrite hae at hs_witness_witness_witness_right_right_right
17Calculate and transport equalitiesL98–100

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L98
    rewrite hae at hs_witness_witness_witness_right_right_right
  2. L99
    rewrite hke at hs_witness_witness_witness_right_right_right
  3. L100
    rewrite hke at hs_witness_witness_witness_right_right_right
18Establish hreL101–110

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

  1. L101
    have hre : x=r
  2. L102
    specialize prime_field_add_functional (p)
  3. L103
    specialize prime_field_add_functional (k)
  4. L104
    specialize prime_field_add_functional (a)
  5. L105
    specialize prime_field_add_functional (x)
  6. L106
    specialize prime_field_add_functional (r)
  7. L107
    apply prime_field_add_functional
  8. L108
    exact hs_witness_witness_witness_right_right_right
  9. L109
    exact hr
  10. L110
    rewrite hre at he_witness
19Calculate and transport equalitiesL111–111

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L111
    rewrite hre at he_witness
20Use earlier factsL112–112

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

  1. L112
    exact he_witness

Library-wide reading audit

Original defined command ledger · 112 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro a
  7. 0007intro h
  8. 0008intro k
  9. 0009intro r
  10. 0010intro hp
  11. 0011intro ha
  12. 0012intro hh
  13. 0013intro hm
  14. 0014intro hr
  15. 0015have hbounds : Lt(t,p) ∧ BetaPrefixInto(b,c,l,p)
  16. 0016specialize prime_field_polynomial_horner_input_bounds (p)
  17. 0017specialize prime_field_polynomial_horner_input_bounds (b)
  18. 0018specialize prime_field_polynomial_horner_input_bounds (c)
  19. 0019specialize prime_field_polynomial_horner_input_bounds (t)
  20. 0020specialize prime_field_polynomial_horner_input_bounds (l)
  21. 0021specialize prime_field_polynomial_horner_input_bounds (h)
  22. 0022apply prime_field_polynomial_horner_input_bounds
  23. 0023exact hh
  24. 0024cases hbounds
  25. 0025have hrcopy : FpAdd(p,k,a,r)
  26. 0026exact hr
  27. 0027cases hrcopy
  28. 0028cases hrcopy_right
  29. 0029have hcoeff : BetaPrefixInto(b,c,S l,p)
  30. 0030specialize matrix_rank_bounded_prefix_extend (b)
  31. 0031specialize matrix_rank_bounded_prefix_extend (c)
  32. 0032specialize matrix_rank_bounded_prefix_extend (l)
  33. 0033specialize matrix_rank_bounded_prefix_extend (p)
  34. 0034specialize matrix_rank_bounded_prefix_extend (a)
  35. 0035apply matrix_rank_bounded_prefix_extend
  36. 0036exact hbounds_right
  37. 0037exact ha
  38. 0038exact hrcopy_right_left
  39. 0039have he : ∃ s. FpHorner(p,b,c,t,S l,s)
  40. 0040specialize prime_field_polynomial_horner_exists (p)
  41. 0041specialize prime_field_polynomial_horner_exists (b)
  42. 0042specialize prime_field_polynomial_horner_exists (c)
  43. 0043specialize prime_field_polynomial_horner_exists (t)
  44. 0044specialize prime_field_polynomial_horner_exists (S l)
  45. 0045apply prime_field_polynomial_horner_exists
  46. 0046exact hp
  47. 0047exact hcoeff
  48. 0048exact hbounds_left
  49. 0049cases he
  50. 0050have hs : ∃ a. ∃ h. ∃ k. BetaAt(b,c,l,a) ∧ (FpHorner(p,b,c,t,l,h) ∧ (FpMul(p,h,t,k) ∧ FpAdd(p,k,a,x)))
  51. 0051specialize prime_field_polynomial_horner_successor_decompose (p)
  52. 0052specialize prime_field_polynomial_horner_successor_decompose (b)
  53. 0053specialize prime_field_polynomial_horner_successor_decompose (c)
  54. 0054specialize prime_field_polynomial_horner_successor_decompose (t)
  55. 0055specialize prime_field_polynomial_horner_successor_decompose (l)
  56. 0056specialize prime_field_polynomial_horner_successor_decompose (x)
  57. 0057apply prime_field_polynomial_horner_successor_decompose
  58. 0058exact he_witness
  59. 0059cases hs
  60. 0060cases hs_witness
  61. 0061cases hs_witness_witness
  62. 0062cases hs_witness_witness_witness
  63. 0063cases hs_witness_witness_witness_right
  64. 0064cases hs_witness_witness_witness_right_right
  65. 0065have hae : x1=a
  66. 0066specialize beta_at_unique (b)
  67. 0067specialize beta_at_unique (c)
  68. 0068specialize beta_at_unique (l)
  69. 0069specialize beta_at_unique (x1)
  70. 0070specialize beta_at_unique (a)
  71. 0071apply beta_at_unique
  72. 0072exact hs_witness_witness_witness_left
  73. 0073exact ha
  74. 0074have hhe : x2=h
  75. 0075specialize prime_field_polynomial_horner_functional (p)
  76. 0076specialize prime_field_polynomial_horner_functional (b)
  77. 0077specialize prime_field_polynomial_horner_functional (c)
  78. 0078specialize prime_field_polynomial_horner_functional (t)
  79. 0079specialize prime_field_polynomial_horner_functional (l)
  80. 0080specialize prime_field_polynomial_horner_functional (x2)
  81. 0081specialize prime_field_polynomial_horner_functional (h)
  82. 0082apply prime_field_polynomial_horner_functional
  83. 0083exact hp
  84. 0084exact hs_witness_witness_witness_right_left
  85. 0085exact hh
  86. 0086rewrite hhe at hs_witness_witness_witness_right_right_left
  87. 0087rewrite hhe at hs_witness_witness_witness_right_right_left
  88. 0088have hke : x3=k
  89. 0089specialize prime_field_multiply_functional (p)
  90. 0090specialize prime_field_multiply_functional (h)
  91. 0091specialize prime_field_multiply_functional (t)
  92. 0092specialize prime_field_multiply_functional (x3)
  93. 0093specialize prime_field_multiply_functional (k)
  94. 0094apply prime_field_multiply_functional
  95. 0095exact hs_witness_witness_witness_right_right_left
  96. 0096exact hm
  97. 0097rewrite hae at hs_witness_witness_witness_right_right_right
  98. 0098rewrite hae at hs_witness_witness_witness_right_right_right
  99. 0099rewrite hke at hs_witness_witness_witness_right_right_right
  100. 0100rewrite hke at hs_witness_witness_witness_right_right_right
  101. 0101have hre : x=r
  102. 0102specialize prime_field_add_functional (p)
  103. 0103specialize prime_field_add_functional (k)
  104. 0104specialize prime_field_add_functional (a)
  105. 0105specialize prime_field_add_functional (x)
  106. 0106specialize prime_field_add_functional (r)
  107. 0107apply prime_field_add_functional
  108. 0108exact hs_witness_witness_witness_right_right_right
  109. 0109exact hr
  110. 0110rewrite hre at he_witness
  111. 0111rewrite hre at he_witness
  112. 0112exact he_witness