PP002C

prime_field_polynomial_horner_successor_construct

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

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

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

Exact expanded first-order arithmetic statement

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 8 declared prerequisites and contains 112 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PP0023 prime_field_polynomial_horner_input_bounds matrix_rank_bounded_prefix_extend Alpha theorem; checked-use authorized PP0022 prime_field_polynomial_horner_exists PP0025 prime_field_polynomial_horner_successor_decompose beta_at_unique Stable theorem; checked-use authorized PP0029 prime_field_polynomial_horner_functional prime_field_multiply_functional Alpha theorem; checked-use authorized prime_field_add_functional Alpha theorem; checked-use authorized

Direct dependents

PP002D prime_field_polynomial_horner_constant PP002E prime_field_polynomial_horner_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

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.

Named ingredients (4)
prime field polynomial horner input boundsprime field polynomial horner existsprime field polynomial horner successor decomposeprime field polynomial horner functional

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro 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: BetaPrefixIntoLt
  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
  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
  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
  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: FpAddFpMulFpHornerBetaAt
  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 exact 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 : ((exists pfa_gap_successor_intro_base. pfa_gap_successor_intro_base + S (t) = (p)) /\ ((forall fom_index_pfp_successor_intro_prefix_bounds. (exists fom_gap_pfp_successor_intro_prefix_bounds_index_bound. fom_gap_pfp_successor_intro_prefix_bounds_index_bound + S (fom_index_pfp_successor_intro_prefix_bounds) = l) -> exists fom_value_pfp_successor_intro_prefix_bounds. ((((exists fom_beta_height_pfp_successor_intro_prefix_bounds_entry. fom_beta_height_pfp_successor_intro_prefix_bounds_entry + S (fom_value_pfp_successor_intro_prefix_bounds) = S ((S (fom_index_pfp_successor_intro_prefix_bounds)) * c)) /\ exists fom_beta_quotient_pfp_successor_intro_prefix_bounds_entry. b = fom_beta_quotient_pfp_successor_intro_prefix_bounds_entry * S ((S (fom_index_pfp_successor_intro_prefix_bounds)) * c) + (fom_value_pfp_successor_intro_prefix_bounds))) /\ (exists fom_gap_pfp_successor_intro_prefix_bounds_value_bound. fom_gap_pfp_successor_intro_prefix_bounds_value_bound + S (fom_value_pfp_successor_intro_prefix_bounds) = 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 : ((exists pfa_gap_successor_intro_operation_copyleft. pfa_gap_successor_intro_operation_copyleft + S (k) = (p)) /\ (((exists pfa_gap_successor_intro_operation_copyright. pfa_gap_successor_intro_operation_copyright + S (a) = (p)) /\ ((((exists pfa_gap_successor_intro_operation_copyresultbound. pfa_gap_successor_intro_operation_copyresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_successor_intro_operation_copyresultcongruence pfa_offset_right_successor_intro_operation_copyresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_successor_intro_operation_copyresultcongruence = (r) + (p) * pfa_offset_right_successor_intro_operation_copyresultcongruence))))))))
  26. 0026exact hr
  27. 0027cases hrcopy
  28. 0028cases hrcopy_right
  29. 0029have hcoeff : forall fom_index_pfp_successor_intro_coefficients. (exists fom_gap_pfp_successor_intro_coefficients_index_bound. fom_gap_pfp_successor_intro_coefficients_index_bound + S (fom_index_pfp_successor_intro_coefficients) = S l) -> exists fom_value_pfp_successor_intro_coefficients. ((((exists fom_beta_height_pfp_successor_intro_coefficients_entry. fom_beta_height_pfp_successor_intro_coefficients_entry + S (fom_value_pfp_successor_intro_coefficients) = S ((S (fom_index_pfp_successor_intro_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_successor_intro_coefficients_entry. b = fom_beta_quotient_pfp_successor_intro_coefficients_entry * S ((S (fom_index_pfp_successor_intro_coefficients)) * c) + (fom_value_pfp_successor_intro_coefficients))) /\ (exists fom_gap_pfp_successor_intro_coefficients_value_bound. fom_gap_pfp_successor_intro_coefficients_value_bound + S (fom_value_pfp_successor_intro_coefficients) = 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 : exists s. (exists pfh_trace_code_successor_intro_candidate pfh_trace_scale_successor_intro_candidate. (((exists pfa_gap_successor_intro_candidatetracebase. pfa_gap_successor_intro_candidatetracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_intro_candidatetraceinitial. ff_h_pfp_successor_intro_candidatetraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_intro_candidate)) /\ exists ff_q_pfp_successor_intro_candidatetraceinitial. pfh_trace_code_successor_intro_candidate = ff_q_pfp_successor_intro_candidatetraceinitial * S ((S (0)) * pfh_trace_scale_successor_intro_candidate) + (0))) /\ (((((exists ff_h_pfp_successor_intro_candidatetraceterminal. ff_h_pfp_successor_intro_candidatetraceterminal + S (s) = S ((S (S l)) * pfh_trace_scale_successor_intro_candidate)) /\ exists ff_q_pfp_successor_intro_candidatetraceterminal. pfh_trace_code_successor_intro_candidate = ff_q_pfp_successor_intro_candidatetraceterminal * S ((S (S l)) * pfh_trace_scale_successor_intro_candidate) + (s))) /\ ((forall pfh_index_successor_intro_candidatetracesteps. (exists pfa_gap_successor_intro_candidatetracestepsindex. pfa_gap_successor_intro_candidatetracestepsindex + S (pfh_index_successor_intro_candidatetracesteps) = (S l)) -> (exists pfh_coefficient_successor_intro_candidatetracestepsstep pfh_before_successor_intro_candidatetracestepsstep pfh_after_successor_intro_candidatetracestepsstep pfh_product_successor_intro_candidatetracestepsstep. ((((exists ff_h_pfp_successor_intro_candidatetracestepsstepcoefficient. ff_h_pfp_successor_intro_candidatetracestepsstepcoefficient + S (pfh_coefficient_successor_intro_candidatetracestepsstep) = S ((S (pfh_index_successor_intro_candidatetracesteps)) * c)) /\ exists ff_q_pfp_successor_intro_candidatetracestepsstepcoefficient. b = ff_q_pfp_successor_intro_candidatetracestepsstepcoefficient * S ((S (pfh_index_successor_intro_candidatetracesteps)) * c) + (pfh_coefficient_successor_intro_candidatetracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_candidatetracestepsstepbefore. ff_h_pfp_successor_intro_candidatetracestepsstepbefore + S (pfh_before_successor_intro_candidatetracestepsstep) = S ((S (pfh_index_successor_intro_candidatetracesteps)) * pfh_trace_scale_successor_intro_candidate)) /\ exists ff_q_pfp_successor_intro_candidatetracestepsstepbefore. pfh_trace_code_successor_intro_candidate = ff_q_pfp_successor_intro_candidatetracestepsstepbefore * S ((S (pfh_index_successor_intro_candidatetracesteps)) * pfh_trace_scale_successor_intro_candidate) + (pfh_before_successor_intro_candidatetracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_candidatetracestepsstepafter. ff_h_pfp_successor_intro_candidatetracestepsstepafter + S (pfh_after_successor_intro_candidatetracestepsstep) = S ((S (S (pfh_index_successor_intro_candidatetracesteps))) * pfh_trace_scale_successor_intro_candidate)) /\ exists ff_q_pfp_successor_intro_candidatetracestepsstepafter. pfh_trace_code_successor_intro_candidate = ff_q_pfp_successor_intro_candidatetracestepsstepafter * S ((S (S (pfh_index_successor_intro_candidatetracesteps))) * pfh_trace_scale_successor_intro_candidate) + (pfh_after_successor_intro_candidatetracestepsstep))) /\ (((((exists pfa_gap_successor_intro_candidatetracestepsstepmultiplyleft. pfa_gap_successor_intro_candidatetracestepsstepmultiplyleft + S (pfh_before_successor_intro_candidatetracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_candidatetracestepsstepmultiplyright. pfa_gap_successor_intro_candidatetracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_intro_candidatetracestepsstepmultiplyresultbound. pfa_gap_successor_intro_candidatetracestepsstepmultiplyresultbound + S (pfh_product_successor_intro_candidatetracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_candidatetracestepsstepmultiplyresultcongruence pfa_offset_right_successor_intro_candidatetracestepsstepmultiplyresultcongruence. ((pfh_before_successor_intro_candidatetracestepsstep) * (t)) + (p) * pfa_offset_left_successor_intro_candidatetracestepsstepmultiplyresultcongruence = (pfh_product_successor_intro_candidatetracestepsstep) + (p) * pfa_offset_right_successor_intro_candidatetracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_intro_candidatetracestepsstepaddleft. pfa_gap_successor_intro_candidatetracestepsstepaddleft + S (pfh_product_successor_intro_candidatetracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_candidatetracestepsstepaddright. pfa_gap_successor_intro_candidatetracestepsstepaddright + S (pfh_coefficient_successor_intro_candidatetracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_intro_candidatetracestepsstepaddresultbound. pfa_gap_successor_intro_candidatetracestepsstepaddresultbound + S (pfh_after_successor_intro_candidatetracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_candidatetracestepsstepaddresultcongruence pfa_offset_right_successor_intro_candidatetracestepsstepaddresultcongruence. ((pfh_product_successor_intro_candidatetracestepsstep) + (pfh_coefficient_successor_intro_candidatetracestepsstep)) + (p) * pfa_offset_left_successor_intro_candidatetracestepsstepaddresultcongruence = (pfh_after_successor_intro_candidatetracestepsstep) + (p) * pfa_offset_right_successor_intro_candidatetracestepsstepaddresultcongruence)))))))))))))))))))))))))))
  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 : exists a h k. ((((exists ff_h_pfp_successor_intro_candidate_coefficient. ff_h_pfp_successor_intro_candidate_coefficient + S (a) = S ((S (l)) * c)) /\ exists ff_q_pfp_successor_intro_candidate_coefficient. b = ff_q_pfp_successor_intro_candidate_coefficient * S ((S (l)) * c) + (a))) /\ (((exists pfh_trace_code_successor_intro_candidate_prefix pfh_trace_scale_successor_intro_candidate_prefix. (((exists pfa_gap_successor_intro_candidate_prefixtracebase. pfa_gap_successor_intro_candidate_prefixtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_intro_candidate_prefixtraceinitial. ff_h_pfp_successor_intro_candidate_prefixtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_intro_candidate_prefix)) /\ exists ff_q_pfp_successor_intro_candidate_prefixtraceinitial. pfh_trace_code_successor_intro_candidate_prefix = ff_q_pfp_successor_intro_candidate_prefixtraceinitial * S ((S (0)) * pfh_trace_scale_successor_intro_candidate_prefix) + (0))) /\ (((((exists ff_h_pfp_successor_intro_candidate_prefixtraceterminal. ff_h_pfp_successor_intro_candidate_prefixtraceterminal + S (h) = S ((S (l)) * pfh_trace_scale_successor_intro_candidate_prefix)) /\ exists ff_q_pfp_successor_intro_candidate_prefixtraceterminal. pfh_trace_code_successor_intro_candidate_prefix = ff_q_pfp_successor_intro_candidate_prefixtraceterminal * S ((S (l)) * pfh_trace_scale_successor_intro_candidate_prefix) + (h))) /\ ((forall pfh_index_successor_intro_candidate_prefixtracesteps. (exists pfa_gap_successor_intro_candidate_prefixtracestepsindex. pfa_gap_successor_intro_candidate_prefixtracestepsindex + S (pfh_index_successor_intro_candidate_prefixtracesteps) = (l)) -> (exists pfh_coefficient_successor_intro_candidate_prefixtracestepsstep pfh_before_successor_intro_candidate_prefixtracestepsstep pfh_after_successor_intro_candidate_prefixtracestepsstep pfh_product_successor_intro_candidate_prefixtracestepsstep. ((((exists ff_h_pfp_successor_intro_candidate_prefixtracestepsstepcoefficient. ff_h_pfp_successor_intro_candidate_prefixtracestepsstepcoefficient + S (pfh_coefficient_successor_intro_candidate_prefixtracestepsstep) = S ((S (pfh_index_successor_intro_candidate_prefixtracesteps)) * c)) /\ exists ff_q_pfp_successor_intro_candidate_prefixtracestepsstepcoefficient. b = ff_q_pfp_successor_intro_candidate_prefixtracestepsstepcoefficient * S ((S (pfh_index_successor_intro_candidate_prefixtracesteps)) * c) + (pfh_coefficient_successor_intro_candidate_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_candidate_prefixtracestepsstepbefore. ff_h_pfp_successor_intro_candidate_prefixtracestepsstepbefore + S (pfh_before_successor_intro_candidate_prefixtracestepsstep) = S ((S (pfh_index_successor_intro_candidate_prefixtracesteps)) * pfh_trace_scale_successor_intro_candidate_prefix)) /\ exists ff_q_pfp_successor_intro_candidate_prefixtracestepsstepbefore. pfh_trace_code_successor_intro_candidate_prefix = ff_q_pfp_successor_intro_candidate_prefixtracestepsstepbefore * S ((S (pfh_index_successor_intro_candidate_prefixtracesteps)) * pfh_trace_scale_successor_intro_candidate_prefix) + (pfh_before_successor_intro_candidate_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_intro_candidate_prefixtracestepsstepafter. ff_h_pfp_successor_intro_candidate_prefixtracestepsstepafter + S (pfh_after_successor_intro_candidate_prefixtracestepsstep) = S ((S (S (pfh_index_successor_intro_candidate_prefixtracesteps))) * pfh_trace_scale_successor_intro_candidate_prefix)) /\ exists ff_q_pfp_successor_intro_candidate_prefixtracestepsstepafter. pfh_trace_code_successor_intro_candidate_prefix = ff_q_pfp_successor_intro_candidate_prefixtracestepsstepafter * S ((S (S (pfh_index_successor_intro_candidate_prefixtracesteps))) * pfh_trace_scale_successor_intro_candidate_prefix) + (pfh_after_successor_intro_candidate_prefixtracestepsstep))) /\ (((((exists pfa_gap_successor_intro_candidate_prefixtracestepsstepmultiplyleft. pfa_gap_successor_intro_candidate_prefixtracestepsstepmultiplyleft + S (pfh_before_successor_intro_candidate_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_candidate_prefixtracestepsstepmultiplyright. pfa_gap_successor_intro_candidate_prefixtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_intro_candidate_prefixtracestepsstepmultiplyresultbound. pfa_gap_successor_intro_candidate_prefixtracestepsstepmultiplyresultbound + S (pfh_product_successor_intro_candidate_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_candidate_prefixtracestepsstepmultiplyresultcongruence pfa_offset_right_successor_intro_candidate_prefixtracestepsstepmultiplyresultcongruence. ((pfh_before_successor_intro_candidate_prefixtracestepsstep) * (t)) + (p) * pfa_offset_left_successor_intro_candidate_prefixtracestepsstepmultiplyresultcongruence = (pfh_product_successor_intro_candidate_prefixtracestepsstep) + (p) * pfa_offset_right_successor_intro_candidate_prefixtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_intro_candidate_prefixtracestepsstepaddleft. pfa_gap_successor_intro_candidate_prefixtracestepsstepaddleft + S (pfh_product_successor_intro_candidate_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_intro_candidate_prefixtracestepsstepaddright. pfa_gap_successor_intro_candidate_prefixtracestepsstepaddright + S (pfh_coefficient_successor_intro_candidate_prefixtracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_intro_candidate_prefixtracestepsstepaddresultbound. pfa_gap_successor_intro_candidate_prefixtracestepsstepaddresultbound + S (pfh_after_successor_intro_candidate_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_intro_candidate_prefixtracestepsstepaddresultcongruence pfa_offset_right_successor_intro_candidate_prefixtracestepsstepaddresultcongruence. ((pfh_product_successor_intro_candidate_prefixtracestepsstep) + (pfh_coefficient_successor_intro_candidate_prefixtracestepsstep)) + (p) * pfa_offset_left_successor_intro_candidate_prefixtracestepsstepaddresultcongruence = (pfh_after_successor_intro_candidate_prefixtracestepsstep) + (p) * pfa_offset_right_successor_intro_candidate_prefixtracestepsstepaddresultcongruence))))))))))))))))))))))))))) /\ (((((exists pfa_gap_successor_intro_candidate_multiplyleft. pfa_gap_successor_intro_candidate_multiplyleft + S (h) = (p)) /\ (((exists pfa_gap_successor_intro_candidate_multiplyright. pfa_gap_successor_intro_candidate_multiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_intro_candidate_multiplyresultbound. pfa_gap_successor_intro_candidate_multiplyresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_successor_intro_candidate_multiplyresultcongruence pfa_offset_right_successor_intro_candidate_multiplyresultcongruence. ((h) * (t)) + (p) * pfa_offset_left_successor_intro_candidate_multiplyresultcongruence = (k) + (p) * pfa_offset_right_successor_intro_candidate_multiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_intro_candidate_addleft. pfa_gap_successor_intro_candidate_addleft + S (k) = (p)) /\ (((exists pfa_gap_successor_intro_candidate_addright. pfa_gap_successor_intro_candidate_addright + S (a) = (p)) /\ ((((exists pfa_gap_successor_intro_candidate_addresultbound. pfa_gap_successor_intro_candidate_addresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_successor_intro_candidate_addresultcongruence pfa_offset_right_successor_intro_candidate_addresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_successor_intro_candidate_addresultcongruence = (x) + (p) * pfa_offset_right_successor_intro_candidate_addresultcongruence)))))))))))))))
  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