PP0021

prime_field_polynomial_horner_trace_from_normalization

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

Reducing all l+1 states of a genuine natural Horner trace constructs a genuine canonical execution, including its zero initial state.

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 n u v U V. (~((p) = 1) /\ forall pfa_factor_left_trace_construct_prime pfa_factor_right_trace_construct_prime. (p) = pfa_factor_left_trace_construct_prime * pfa_factor_right_trace_construct_prime -> pfa_factor_left_trace_construct_prime = 1 \/ pfa_factor_right_trace_construct_prime = 1) -> (forall fom_index_pfp_trace_construct_coefficients. (exists fom_gap_pfp_trace_construct_coefficients_index_bound. fom_gap_pfp_trace_construct_coefficients_index_bound + S (fom_index_pfp_trace_construct_coefficients) = l) -> exists fom_value_pfp_trace_construct_coefficients. ((((exists fom_beta_height_pfp_trace_construct_coefficients_entry. fom_beta_height_pfp_trace_construct_coefficients_entry + S (fom_value_pfp_trace_construct_coefficients) = S ((S (fom_index_pfp_trace_construct_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_trace_construct_coefficients_entry. b = fom_beta_quotient_pfp_trace_construct_coefficients_entry * S ((S (fom_index_pfp_trace_construct_coefficients)) * c) + (fom_value_pfp_trace_construct_coefficients))) /\ (exists fom_gap_pfp_trace_construct_coefficients_value_bound. fom_gap_pfp_trace_construct_coefficients_value_bound + S (fom_value_pfp_trace_construct_coefficients) = p))) -> (exists pfa_gap_trace_construct_base. pfa_gap_trace_construct_base + S (t) = (p)) -> (((((exists fs_h_ph_pfh_trace_construct_natural_start. fs_h_ph_pfh_trace_construct_natural_start + S (0) = S ((S (0)) * v)) /\ exists fs_q_ph_pfh_trace_construct_natural_start. u = fs_q_ph_pfh_trace_construct_natural_start * S ((S (0)) * v) + (0))) /\ ((((exists fs_h_ph_pfh_trace_construct_natural_terminal. fs_h_ph_pfh_trace_construct_natural_terminal + S (n) = S ((S (l)) * v)) /\ exists fs_q_ph_pfh_trace_construct_natural_terminal. u = fs_q_ph_pfh_trace_construct_natural_terminal * S ((S (l)) * v) + (n))) /\ forall ff_i_ph_pfh_trace_construct_natural_steps. (exists ph_bound_pfh_trace_construct_natural_steps. ph_bound_pfh_trace_construct_natural_steps + S ff_i_ph_pfh_trace_construct_natural_steps = l) -> exists ff_coefficient_ph_pfh_trace_construct_natural_steps ff_previous_ph_pfh_trace_construct_natural_steps ff_current_ph_pfh_trace_construct_natural_steps. ((((exists fs_h_ph_pfh_trace_construct_natural_steps_coefficient. fs_h_ph_pfh_trace_construct_natural_steps_coefficient + S (ff_coefficient_ph_pfh_trace_construct_natural_steps) = S ((S (ff_i_ph_pfh_trace_construct_natural_steps)) * c)) /\ exists fs_q_ph_pfh_trace_construct_natural_steps_coefficient. b = fs_q_ph_pfh_trace_construct_natural_steps_coefficient * S ((S (ff_i_ph_pfh_trace_construct_natural_steps)) * c) + (ff_coefficient_ph_pfh_trace_construct_natural_steps))) /\ ((((exists fs_h_ph_pfh_trace_construct_natural_steps_before. fs_h_ph_pfh_trace_construct_natural_steps_before + S (ff_previous_ph_pfh_trace_construct_natural_steps) = S ((S (ff_i_ph_pfh_trace_construct_natural_steps)) * v)) /\ exists fs_q_ph_pfh_trace_construct_natural_steps_before. u = fs_q_ph_pfh_trace_construct_natural_steps_before * S ((S (ff_i_ph_pfh_trace_construct_natural_steps)) * v) + (ff_previous_ph_pfh_trace_construct_natural_steps))) /\ ((((exists fs_h_ph_pfh_trace_construct_natural_steps_after. fs_h_ph_pfh_trace_construct_natural_steps_after + S (ff_current_ph_pfh_trace_construct_natural_steps) = S ((S (S ff_i_ph_pfh_trace_construct_natural_steps)) * v)) /\ exists fs_q_ph_pfh_trace_construct_natural_steps_after. u = fs_q_ph_pfh_trace_construct_natural_steps_after * S ((S (S ff_i_ph_pfh_trace_construct_natural_steps)) * v) + (ff_current_ph_pfh_trace_construct_natural_steps))) /\ ff_current_ph_pfh_trace_construct_natural_steps = ff_previous_ph_pfh_trace_construct_natural_steps * t + ff_coefficient_ph_pfh_trace_construct_natural_steps)))))) -> (forall pfp_index_trace_construct_normalization. (exists pfa_gap_trace_construct_normalizationindex. pfa_gap_trace_construct_normalizationindex + S (pfp_index_trace_construct_normalization) = (S l)) -> exists pfp_source_trace_construct_normalization pfp_residue_trace_construct_normalization. ((((exists ff_h_pfp_trace_construct_normalizationsource. ff_h_pfp_trace_construct_normalizationsource + S (pfp_source_trace_construct_normalization) = S ((S (pfp_index_trace_construct_normalization)) * v)) /\ exists ff_q_pfp_trace_construct_normalizationsource. u = ff_q_pfp_trace_construct_normalizationsource * S ((S (pfp_index_trace_construct_normalization)) * v) + (pfp_source_trace_construct_normalization))) /\ (((((exists ff_h_pfp_trace_construct_normalizationtarget. ff_h_pfp_trace_construct_normalizationtarget + S (pfp_residue_trace_construct_normalization) = S ((S (pfp_index_trace_construct_normalization)) * V)) /\ exists ff_q_pfp_trace_construct_normalizationtarget. U = ff_q_pfp_trace_construct_normalizationtarget * S ((S (pfp_index_trace_construct_normalization)) * V) + (pfp_residue_trace_construct_normalization))) /\ ((((exists pfa_gap_trace_construct_normalizationresiduebound. pfa_gap_trace_construct_normalizationresiduebound + S (pfp_residue_trace_construct_normalization) = (p)) /\ ((exists pfa_offset_left_trace_construct_normalizationresiduecongruence pfa_offset_right_trace_construct_normalizationresiduecongruence. (pfp_source_trace_construct_normalization) + (p) * pfa_offset_left_trace_construct_normalizationresiduecongruence = (pfp_residue_trace_construct_normalization) + (p) * pfa_offset_right_trace_construct_normalizationresiduecongruence))))))))) -> exists r. ((((exists pfa_gap_trace_construct_executionbase. pfa_gap_trace_construct_executionbase + S (t) = (p)) /\ (((((exists ff_h_pfp_trace_construct_executioninitial. ff_h_pfp_trace_construct_executioninitial + S (0) = S ((S (0)) * V)) /\ exists ff_q_pfp_trace_construct_executioninitial. U = ff_q_pfp_trace_construct_executioninitial * S ((S (0)) * V) + (0))) /\ (((((exists ff_h_pfp_trace_construct_executionterminal. ff_h_pfp_trace_construct_executionterminal + S (r) = S ((S (l)) * V)) /\ exists ff_q_pfp_trace_construct_executionterminal. U = ff_q_pfp_trace_construct_executionterminal * S ((S (l)) * V) + (r))) /\ ((forall pfh_index_trace_construct_executionsteps. (exists pfa_gap_trace_construct_executionstepsindex. pfa_gap_trace_construct_executionstepsindex + S (pfh_index_trace_construct_executionsteps) = (l)) -> (exists pfh_coefficient_trace_construct_executionstepsstep pfh_before_trace_construct_executionstepsstep pfh_after_trace_construct_executionstepsstep pfh_product_trace_construct_executionstepsstep. ((((exists ff_h_pfp_trace_construct_executionstepsstepcoefficient. ff_h_pfp_trace_construct_executionstepsstepcoefficient + S (pfh_coefficient_trace_construct_executionstepsstep) = S ((S (pfh_index_trace_construct_executionsteps)) * c)) /\ exists ff_q_pfp_trace_construct_executionstepsstepcoefficient. b = ff_q_pfp_trace_construct_executionstepsstepcoefficient * S ((S (pfh_index_trace_construct_executionsteps)) * c) + (pfh_coefficient_trace_construct_executionstepsstep))) /\ (((((exists ff_h_pfp_trace_construct_executionstepsstepbefore. ff_h_pfp_trace_construct_executionstepsstepbefore + S (pfh_before_trace_construct_executionstepsstep) = S ((S (pfh_index_trace_construct_executionsteps)) * V)) /\ exists ff_q_pfp_trace_construct_executionstepsstepbefore. U = ff_q_pfp_trace_construct_executionstepsstepbefore * S ((S (pfh_index_trace_construct_executionsteps)) * V) + (pfh_before_trace_construct_executionstepsstep))) /\ (((((exists ff_h_pfp_trace_construct_executionstepsstepafter. ff_h_pfp_trace_construct_executionstepsstepafter + S (pfh_after_trace_construct_executionstepsstep) = S ((S (S (pfh_index_trace_construct_executionsteps))) * V)) /\ exists ff_q_pfp_trace_construct_executionstepsstepafter. U = ff_q_pfp_trace_construct_executionstepsstepafter * S ((S (S (pfh_index_trace_construct_executionsteps))) * V) + (pfh_after_trace_construct_executionstepsstep))) /\ (((((exists pfa_gap_trace_construct_executionstepsstepmultiplyleft. pfa_gap_trace_construct_executionstepsstepmultiplyleft + S (pfh_before_trace_construct_executionstepsstep) = (p)) /\ (((exists pfa_gap_trace_construct_executionstepsstepmultiplyright. pfa_gap_trace_construct_executionstepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_trace_construct_executionstepsstepmultiplyresultbound. pfa_gap_trace_construct_executionstepsstepmultiplyresultbound + S (pfh_product_trace_construct_executionstepsstep) = (p)) /\ ((exists pfa_offset_left_trace_construct_executionstepsstepmultiplyresultcongruence pfa_offset_right_trace_construct_executionstepsstepmultiplyresultcongruence. ((pfh_before_trace_construct_executionstepsstep) * (t)) + (p) * pfa_offset_left_trace_construct_executionstepsstepmultiplyresultcongruence = (pfh_product_trace_construct_executionstepsstep) + (p) * pfa_offset_right_trace_construct_executionstepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_trace_construct_executionstepsstepaddleft. pfa_gap_trace_construct_executionstepsstepaddleft + S (pfh_product_trace_construct_executionstepsstep) = (p)) /\ (((exists pfa_gap_trace_construct_executionstepsstepaddright. pfa_gap_trace_construct_executionstepsstepaddright + S (pfh_coefficient_trace_construct_executionstepsstep) = (p)) /\ ((((exists pfa_gap_trace_construct_executionstepsstepaddresultbound. pfa_gap_trace_construct_executionstepsstepaddresultbound + S (pfh_after_trace_construct_executionstepsstep) = (p)) /\ ((exists pfa_offset_left_trace_construct_executionstepsstepaddresultcongruence pfa_offset_right_trace_construct_executionstepsstepaddresultcongruence. ((pfh_product_trace_construct_executionstepsstep) + (pfh_coefficient_trace_construct_executionstepsstep)) + (p) * pfa_offset_left_trace_construct_executionstepsstepaddresultcongruence = (pfh_after_trace_construct_executionstepsstep) + (p) * pfa_offset_right_trace_construct_executionstepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((((exists pfa_gap_trace_construct_final_residuebound. pfa_gap_trace_construct_final_residuebound + S (r) = (p)) /\ ((exists pfa_offset_left_trace_construct_final_residuecongruence pfa_offset_right_trace_construct_final_residuecongruence. (n) + (p) * pfa_offset_left_trace_construct_final_residuecongruence = (r) + (p) * pfa_offset_right_trace_construct_final_residuecongruence))))))

Constructive proof overview

Generated structural guide

Reducing all l+1 states of a genuine natural Horner trace constructs a genuine canonical execution, including its zero initial state.

The unchanged tactic script uses 10 declared prerequisites and contains 187 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized PP0003 prime_field_polynomial_normalization_entry zero_add Stable theorem; checked-use authorized prime_field_residue_bounded_value Alpha theorem; checked-use authorized prime_field_zero_below_prime Alpha theorem; checked-use authorized le_succ Stable theorem; checked-use authorized succ_le_succ Stable theorem; checked-use authorized prime_field_residue_input_equal Alpha theorem; checked-use authorized PP0020 prime_field_polynomial_horner_canonical_step matrix_rank_bounded_prefix_value Alpha theorem; checked-use authorized

Direct dependents

PP0022 prime_field_polynomial_horner_exists

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

187 script commands · 52 reading checkpoints · 12 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
prime field polynomial normalization entryprime field polynomial horner canonical step

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 n
  7. L7
    intro u
  8. L8
    intro v
  9. L9
    intro U
  10. L10
    intro V
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hp
  2. L12
    intro hc
  3. L13
    intro ht
  4. L14
    intro hn
  5. L15
    intro hred
03Separate the logical casesL16–17

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

  1. L16
    cases hn
  2. L17
    cases hn_right
04Establish heL18–22

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

  1. L18
    have he : exists r. (((exists ff_h_pfp_trace_construct_terminal. ff_h_pfp_trace_construct_terminal + S (r) = S ((S (l)) * V)) /\ exists ff_q_pfp_trace_construct_terminal. U = ff_q_pfp_trace_construct_terminal * S ((S (l)) * V) + (r)))
  2. L19
    specialize beta_at_exists (U)
  3. L20
    specialize beta_at_exists (V)
  4. L21
    specialize beta_at_exists (l)
  5. L22
    apply beta_at_exists
05Separate the logical casesL23–23

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

  1. L23
    cases he
06Establish hrL24–33

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

  1. L24
    have hr : ((exists pfa_gap_trace_construct_resultbound. pfa_gap_trace_construct_resultbound + S (x) = (p)) /\ ((exists pfa_offset_left_trace_construct_resultcongruence pfa_offset_right_trace_construct_resultcongruence. (n) + (p) * pfa_offset_left_trace_construct_resultcongruence = (x) + (p) * pfa_offset_right_trace_construct_resultcongruence)))
  2. L25
    specialize prime_field_polynomial_normalization_entry (p)
  3. L26
    specialize prime_field_polynomial_normalization_entry (u)
  4. L27
    specialize prime_field_polynomial_normalization_entry (v)
  5. L28
    specialize prime_field_polynomial_normalization_entry (U)
  6. L29
    specialize prime_field_polynomial_normalization_entry (V)
  7. L30
    specialize prime_field_polynomial_normalization_entry (S l)
  8. L31
    specialize prime_field_polynomial_normalization_entry (l)
  9. L32
    specialize prime_field_polynomial_normalization_entry (n)
  10. L33
    specialize prime_field_polynomial_normalization_entry (x)
07Use earlier factsL34–35

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

  1. L34
    apply prime_field_polynomial_normalization_entry
  2. L35
    exact hred
08Construct an explicit witnessL36–36

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

  1. L36
    exists 0
09Use earlier factsL37–39

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

  1. L37
    apply zero_add
  2. L38
    exact hn_right_left
  3. L39
    exact he_witness
10Establish hzeroL40–40

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

  1. L40
    have hzero : ((exists ff_h_pfp_trace_construct_zero. ff_h_pfp_trace_construct_zero + S (0) = S ((S (0)) * V)) /\ exists ff_q_pfp_trace_construct_zero. U = ff_q_pfp_trace_construct_zero * S ((S (0)) * V) + (0))
11Establish hzL41–45

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

  1. L41
    have hz : exists z. (((exists ff_h_pfp_trace_construct_first. ff_h_pfp_trace_construct_first + S (z) = S ((S (0)) * V)) /\ exists ff_q_pfp_trace_construct_first. U = ff_q_pfp_trace_construct_first * S ((S (0)) * V) + (z)))
  2. L42
    specialize beta_at_exists (U)
  3. L43
    specialize beta_at_exists (V)
  4. L44
    specialize beta_at_exists (0)
  5. L45
    apply beta_at_exists
12Separate the logical casesL46–46

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

  1. L46
    cases hz
13Establish hzresL47–56

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

  1. L47
    have hzres : ((exists pfa_gap_trace_construct_first_residuebound. pfa_gap_trace_construct_first_residuebound + S (x1) = (p)) /\ ((exists pfa_offset_left_trace_construct_first_residuecongruence pfa_offset_right_trace_construct_first_residuecongruence. (0) + (p) * pfa_offset_left_trace_construct_first_residuecongruence = (x1) + (p) * pfa_offset_right_trace_construct_first_residuecongruence)))
  2. L48
    specialize prime_field_polynomial_normalization_entry (p)
  3. L49
    specialize prime_field_polynomial_normalization_entry (u)
  4. L50
    specialize prime_field_polynomial_normalization_entry (v)
  5. L51
    specialize prime_field_polynomial_normalization_entry (U)
  6. L52
    specialize prime_field_polynomial_normalization_entry (V)
  7. L53
    specialize prime_field_polynomial_normalization_entry (S l)
  8. L54
    specialize prime_field_polynomial_normalization_entry (0)
  9. L55
    specialize prime_field_polynomial_normalization_entry (0)
  10. L56
    specialize prime_field_polynomial_normalization_entry (x1)
14Use earlier factsL57–58

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

  1. L57
    apply prime_field_polynomial_normalization_entry
  2. L58
    exact hred
15Construct an explicit witnessL59–59

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

  1. L59
    exists l
16Calculate and transport equalitiesL60–60

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

  1. L60
    simp
17Use earlier factsL61–62

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

  1. L61
    exact hn_left
  2. L62
    exact hz_witness
18Establish hzeqL63–72

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

  1. L63
    have hzeq : x1=0
  2. L64
    specialize prime_field_residue_bounded_value (p)
  3. L65
    specialize prime_field_residue_bounded_value (0)
  4. L66
    specialize prime_field_residue_bounded_value (x1)
  5. L67
    apply prime_field_residue_bounded_value
  6. L68
    specialize prime_field_zero_below_prime (p)
  7. L69
    apply prime_field_zero_below_prime
  8. L70
    exact hp
  9. L71
    exact hzres
  10. L72
    rewrite hzeq at hz_witness
19Calculate and transport equalitiesL73–73

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

  1. L73
    rewrite hzeq at hz_witness
20Use earlier factsL74–74

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

  1. L74
    exact hz_witness
21Construct an explicit witnessL75–75

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

  1. L75
    exists x
22Separate the logical casesL76–77

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

  1. L76
    split
  2. L77
    split
23Use earlier factsL78–78

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

  1. L78
    exact ht
24Separate the logical casesL79–79

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

  1. L79
    split
25Use earlier factsL80–80

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

  1. L80
    exact hzero
26Separate the logical casesL81–81

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

  1. L81
    split
27Use earlier factsL82–82

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

  1. L82
    exact he_witness
28Fix variables and assumptionsL83–84

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

  1. L83
    intro i
  2. L84
    intro hi
29Establish hsL85–88

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

  1. L85
    have hs : ∃ a. ∃ h. ∃ j. BetaAt(b,c,i,a) ∧ (BetaAt(u,v,i,h) ∧ (BetaAt(u,v,S i,j) ∧ j = h · t + a))Definitions: BetaAt
  2. L86
    specialize hn_right_right (i)
  3. L87
    apply hn_right_right
  4. L88
    exact hi
30Separate the logical casesL89–94

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

  1. L89
    cases hs
  2. L90
    cases hs_witness
  3. L91
    cases hs_witness_witness
  4. L92
    cases hs_witness_witness_witness
  5. L93
    cases hs_witness_witness_witness_right
  6. L94
    cases hs_witness_witness_witness_right_right
31Establish hbL95–99

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

  1. L95
    have hb : exists r. (((exists ff_h_pfp_trace_construct_canonical_before. ff_h_pfp_trace_construct_canonical_before + S (r) = S ((S (i)) * V)) /\ exists ff_q_pfp_trace_construct_canonical_before. U = ff_q_pfp_trace_construct_canonical_before * S ((S (i)) * V) + (r)))
  2. L96
    specialize beta_at_exists (U)
  3. L97
    specialize beta_at_exists (V)
  4. L98
    specialize beta_at_exists (i)
  5. L99
    apply beta_at_exists
32Separate the logical casesL100–100

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

  1. L100
    cases hb
33Establish haL101–105

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

  1. L101
    have ha : exists r. (((exists ff_h_pfp_trace_construct_canonical_after. ff_h_pfp_trace_construct_canonical_after + S (r) = S ((S (S i)) * V)) /\ exists ff_q_pfp_trace_construct_canonical_after. U = ff_q_pfp_trace_construct_canonical_after * S ((S (S i)) * V) + (r)))
  2. L102
    specialize beta_at_exists (U)
  3. L103
    specialize beta_at_exists (V)
  4. L104
    specialize beta_at_exists (S i)
  5. L105
    apply beta_at_exists
34Separate the logical casesL106–106

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

  1. L106
    cases ha
35Establish hbeforeL107–116

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

  1. L107
    have hbefore : ((exists pfa_gap_trace_construct_before_residuebound. pfa_gap_trace_construct_before_residuebound + S (x4) = (p)) /\ ((exists pfa_offset_left_trace_construct_before_residuecongruence pfa_offset_right_trace_construct_before_residuecongruence. (x2) + (p) * pfa_offset_left_trace_construct_before_residuecongruence = (x4) + (p) * pfa_offset_right_trace_construct_before_residuecongruence)))
  2. L108
    specialize prime_field_polynomial_normalization_entry (p)
  3. L109
    specialize prime_field_polynomial_normalization_entry (u)
  4. L110
    specialize prime_field_polynomial_normalization_entry (v)
  5. L111
    specialize prime_field_polynomial_normalization_entry (U)
  6. L112
    specialize prime_field_polynomial_normalization_entry (V)
  7. L113
    specialize prime_field_polynomial_normalization_entry (S l)
  8. L114
    specialize prime_field_polynomial_normalization_entry (i)
  9. L115
    specialize prime_field_polynomial_normalization_entry (x2)
  10. L116
    specialize prime_field_polynomial_normalization_entry (x4)
36Use earlier factsL117–124

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

  1. L117
    apply prime_field_polynomial_normalization_entry
  2. L118
    exact hred
  3. L119
    specialize le_succ (S i)
  4. L120
    specialize le_succ (l)
  5. L121
    apply le_succ
  6. L122
    exact hi
  7. L123
    exact hs_witness_witness_witness_right_left
  8. L124
    exact hb_witness
37Establish hafterL125–134

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

  1. L125
    have hafter : ((exists pfa_gap_trace_construct_after_residuebound. pfa_gap_trace_construct_after_residuebound + S (x5) = (p)) /\ ((exists pfa_offset_left_trace_construct_after_residuecongruence pfa_offset_right_trace_construct_after_residuecongruence. (x2*t+x1) + (p) * pfa_offset_left_trace_construct_after_residuecongruence = (x5) + (p) * pfa_offset_right_trace_construct_after_residuecongruence)))
  2. L126
    specialize prime_field_residue_input_equal (p)
  3. L127
    specialize prime_field_residue_input_equal (x2*t+x1)
  4. L128
    specialize prime_field_residue_input_equal (x3)
  5. L129
    specialize prime_field_residue_input_equal (x5)
  6. L130
    apply prime_field_residue_input_equal
  7. L131
    symm
  8. L132
    exact hs_witness_witness_witness_right_right_right
  9. L133
    specialize prime_field_polynomial_normalization_entry (p)
  10. L134
    specialize prime_field_polynomial_normalization_entry (u)
38Use earlier factsL135–144

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

  1. L135
    specialize prime_field_polynomial_normalization_entry (v)
  2. L136
    specialize prime_field_polynomial_normalization_entry (U)
  3. L137
    specialize prime_field_polynomial_normalization_entry (V)
  4. L138
    specialize prime_field_polynomial_normalization_entry (S l)
  5. L139
    specialize prime_field_polynomial_normalization_entry (S i)
  6. L140
    specialize prime_field_polynomial_normalization_entry (x3)
  7. L141
    specialize prime_field_polynomial_normalization_entry (x5)
  8. L142
    apply prime_field_polynomial_normalization_entry
  9. L143
    exact hred
  10. L144
    specialize succ_le_succ (S i)
39Use earlier factsL145–149

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

  1. L145
    specialize succ_le_succ (l)
  2. L146
    apply succ_le_succ
  3. L147
    exact hi
  4. L148
    exact hs_witness_witness_witness_right_right_left
  5. L149
    exact ha_witness
40Establish hopL150–159

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

  1. L150
    have hop : ∃ k. FpMul(p,x4,t,k) ∧ FpAdd(p,k,x1,x5)Definitions: FpAddFpMul
  2. L151
    specialize prime_field_polynomial_horner_canonical_step (p)
  3. L152
    specialize prime_field_polynomial_horner_canonical_step (x2)
  4. L153
    specialize prime_field_polynomial_horner_canonical_step (t)
  5. L154
    specialize prime_field_polynomial_horner_canonical_step (x1)
  6. L155
    specialize prime_field_polynomial_horner_canonical_step (x4)
  7. L156
    specialize prime_field_polynomial_horner_canonical_step (x5)
  8. L157
    apply prime_field_polynomial_horner_canonical_step
  9. L158
    exact hp
  10. L159
    exact ht
41Use earlier factsL160–169

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

  1. L160
    specialize matrix_rank_bounded_prefix_value (b)
  2. L161
    specialize matrix_rank_bounded_prefix_value (c)
  3. L162
    specialize matrix_rank_bounded_prefix_value (l)
  4. L163
    specialize matrix_rank_bounded_prefix_value (p)
  5. L164
    specialize matrix_rank_bounded_prefix_value (i)
  6. L165
    specialize matrix_rank_bounded_prefix_value (x1)
  7. L166
    apply matrix_rank_bounded_prefix_value
  8. L167
    exact hc
  9. L168
    exact hi
  10. L169
    exact hs_witness_witness_witness_left
42Use earlier factsL170–171

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

  1. L170
    exact hbefore
  2. L171
    exact hafter
43Separate the logical casesL172–173

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

  1. L172
    cases hop
  2. L173
    cases hop_witness
44Construct an explicit witnessL174–177

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

  1. L174
    exists x1
  2. L175
    exists x4
  3. L176
    exists x5
  4. L177
    exists x6
45Separate the logical casesL178–178

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

  1. L178
    split
46Use earlier factsL179–179

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

  1. L179
    exact hs_witness_witness_witness_left
47Separate the logical casesL180–180

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

  1. L180
    split
48Use earlier factsL181–181

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

  1. L181
    exact hb_witness
49Separate the logical casesL182–182

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

  1. L182
    split
50Use earlier factsL183–183

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

  1. L183
    exact ha_witness
51Separate the logical casesL184–184

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

  1. L184
    split
52Use earlier factsL185–187

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

  1. L185
    exact hop_witness_left
  2. L186
    exact hop_witness_right
  3. L187
    exact hr

Library-wide reading audit

Original exact command ledger · 187 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro n
  7. 0007intro u
  8. 0008intro v
  9. 0009intro U
  10. 0010intro V
  11. 0011intro hp
  12. 0012intro hc
  13. 0013intro ht
  14. 0014intro hn
  15. 0015intro hred
  16. 0016cases hn
  17. 0017cases hn_right
  18. 0018have he : exists r. (((exists ff_h_pfp_trace_construct_terminal. ff_h_pfp_trace_construct_terminal + S (r) = S ((S (l)) * V)) /\ exists ff_q_pfp_trace_construct_terminal. U = ff_q_pfp_trace_construct_terminal * S ((S (l)) * V) + (r)))
  19. 0019specialize beta_at_exists (U)
  20. 0020specialize beta_at_exists (V)
  21. 0021specialize beta_at_exists (l)
  22. 0022apply beta_at_exists
  23. 0023cases he
  24. 0024have hr : ((exists pfa_gap_trace_construct_resultbound. pfa_gap_trace_construct_resultbound + S (x) = (p)) /\ ((exists pfa_offset_left_trace_construct_resultcongruence pfa_offset_right_trace_construct_resultcongruence. (n) + (p) * pfa_offset_left_trace_construct_resultcongruence = (x) + (p) * pfa_offset_right_trace_construct_resultcongruence)))
  25. 0025specialize prime_field_polynomial_normalization_entry (p)
  26. 0026specialize prime_field_polynomial_normalization_entry (u)
  27. 0027specialize prime_field_polynomial_normalization_entry (v)
  28. 0028specialize prime_field_polynomial_normalization_entry (U)
  29. 0029specialize prime_field_polynomial_normalization_entry (V)
  30. 0030specialize prime_field_polynomial_normalization_entry (S l)
  31. 0031specialize prime_field_polynomial_normalization_entry (l)
  32. 0032specialize prime_field_polynomial_normalization_entry (n)
  33. 0033specialize prime_field_polynomial_normalization_entry (x)
  34. 0034apply prime_field_polynomial_normalization_entry
  35. 0035exact hred
  36. 0036exists 0
  37. 0037apply zero_add
  38. 0038exact hn_right_left
  39. 0039exact he_witness
  40. 0040have hzero : ((exists ff_h_pfp_trace_construct_zero. ff_h_pfp_trace_construct_zero + S (0) = S ((S (0)) * V)) /\ exists ff_q_pfp_trace_construct_zero. U = ff_q_pfp_trace_construct_zero * S ((S (0)) * V) + (0))
  41. 0041have hz : exists z. (((exists ff_h_pfp_trace_construct_first. ff_h_pfp_trace_construct_first + S (z) = S ((S (0)) * V)) /\ exists ff_q_pfp_trace_construct_first. U = ff_q_pfp_trace_construct_first * S ((S (0)) * V) + (z)))
  42. 0042specialize beta_at_exists (U)
  43. 0043specialize beta_at_exists (V)
  44. 0044specialize beta_at_exists (0)
  45. 0045apply beta_at_exists
  46. 0046cases hz
  47. 0047have hzres : ((exists pfa_gap_trace_construct_first_residuebound. pfa_gap_trace_construct_first_residuebound + S (x1) = (p)) /\ ((exists pfa_offset_left_trace_construct_first_residuecongruence pfa_offset_right_trace_construct_first_residuecongruence. (0) + (p) * pfa_offset_left_trace_construct_first_residuecongruence = (x1) + (p) * pfa_offset_right_trace_construct_first_residuecongruence)))
  48. 0048specialize prime_field_polynomial_normalization_entry (p)
  49. 0049specialize prime_field_polynomial_normalization_entry (u)
  50. 0050specialize prime_field_polynomial_normalization_entry (v)
  51. 0051specialize prime_field_polynomial_normalization_entry (U)
  52. 0052specialize prime_field_polynomial_normalization_entry (V)
  53. 0053specialize prime_field_polynomial_normalization_entry (S l)
  54. 0054specialize prime_field_polynomial_normalization_entry (0)
  55. 0055specialize prime_field_polynomial_normalization_entry (0)
  56. 0056specialize prime_field_polynomial_normalization_entry (x1)
  57. 0057apply prime_field_polynomial_normalization_entry
  58. 0058exact hred
  59. 0059exists l
  60. 0060simp
  61. 0061exact hn_left
  62. 0062exact hz_witness
  63. 0063have hzeq : x1=0
  64. 0064specialize prime_field_residue_bounded_value (p)
  65. 0065specialize prime_field_residue_bounded_value (0)
  66. 0066specialize prime_field_residue_bounded_value (x1)
  67. 0067apply prime_field_residue_bounded_value
  68. 0068specialize prime_field_zero_below_prime (p)
  69. 0069apply prime_field_zero_below_prime
  70. 0070exact hp
  71. 0071exact hzres
  72. 0072rewrite hzeq at hz_witness
  73. 0073rewrite hzeq at hz_witness
  74. 0074exact hz_witness
  75. 0075exists x
  76. 0076split
  77. 0077split
  78. 0078exact ht
  79. 0079split
  80. 0080exact hzero
  81. 0081split
  82. 0082exact he_witness
  83. 0083intro i
  84. 0084intro hi
  85. 0085have hs : exists a h j. ((((exists ff_h_pfp_trace_construct_coefficient. ff_h_pfp_trace_construct_coefficient + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_trace_construct_coefficient. b = ff_q_pfp_trace_construct_coefficient * S ((S (i)) * c) + (a))) /\ (((((exists ff_h_pfp_trace_construct_before. ff_h_pfp_trace_construct_before + S (h) = S ((S (i)) * v)) /\ exists ff_q_pfp_trace_construct_before. u = ff_q_pfp_trace_construct_before * S ((S (i)) * v) + (h))) /\ (((((exists ff_h_pfp_trace_construct_after. ff_h_pfp_trace_construct_after + S (j) = S ((S (S i)) * v)) /\ exists ff_q_pfp_trace_construct_after. u = ff_q_pfp_trace_construct_after * S ((S (S i)) * v) + (j))) /\ ((j=h*t+a)))))))
  86. 0086specialize hn_right_right (i)
  87. 0087apply hn_right_right
  88. 0088exact hi
  89. 0089cases hs
  90. 0090cases hs_witness
  91. 0091cases hs_witness_witness
  92. 0092cases hs_witness_witness_witness
  93. 0093cases hs_witness_witness_witness_right
  94. 0094cases hs_witness_witness_witness_right_right
  95. 0095have hb : exists r. (((exists ff_h_pfp_trace_construct_canonical_before. ff_h_pfp_trace_construct_canonical_before + S (r) = S ((S (i)) * V)) /\ exists ff_q_pfp_trace_construct_canonical_before. U = ff_q_pfp_trace_construct_canonical_before * S ((S (i)) * V) + (r)))
  96. 0096specialize beta_at_exists (U)
  97. 0097specialize beta_at_exists (V)
  98. 0098specialize beta_at_exists (i)
  99. 0099apply beta_at_exists
  100. 0100cases hb
  101. 0101have ha : exists r. (((exists ff_h_pfp_trace_construct_canonical_after. ff_h_pfp_trace_construct_canonical_after + S (r) = S ((S (S i)) * V)) /\ exists ff_q_pfp_trace_construct_canonical_after. U = ff_q_pfp_trace_construct_canonical_after * S ((S (S i)) * V) + (r)))
  102. 0102specialize beta_at_exists (U)
  103. 0103specialize beta_at_exists (V)
  104. 0104specialize beta_at_exists (S i)
  105. 0105apply beta_at_exists
  106. 0106cases ha
  107. 0107have hbefore : ((exists pfa_gap_trace_construct_before_residuebound. pfa_gap_trace_construct_before_residuebound + S (x4) = (p)) /\ ((exists pfa_offset_left_trace_construct_before_residuecongruence pfa_offset_right_trace_construct_before_residuecongruence. (x2) + (p) * pfa_offset_left_trace_construct_before_residuecongruence = (x4) + (p) * pfa_offset_right_trace_construct_before_residuecongruence)))
  108. 0108specialize prime_field_polynomial_normalization_entry (p)
  109. 0109specialize prime_field_polynomial_normalization_entry (u)
  110. 0110specialize prime_field_polynomial_normalization_entry (v)
  111. 0111specialize prime_field_polynomial_normalization_entry (U)
  112. 0112specialize prime_field_polynomial_normalization_entry (V)
  113. 0113specialize prime_field_polynomial_normalization_entry (S l)
  114. 0114specialize prime_field_polynomial_normalization_entry (i)
  115. 0115specialize prime_field_polynomial_normalization_entry (x2)
  116. 0116specialize prime_field_polynomial_normalization_entry (x4)
  117. 0117apply prime_field_polynomial_normalization_entry
  118. 0118exact hred
  119. 0119specialize le_succ (S i)
  120. 0120specialize le_succ (l)
  121. 0121apply le_succ
  122. 0122exact hi
  123. 0123exact hs_witness_witness_witness_right_left
  124. 0124exact hb_witness
  125. 0125have hafter : ((exists pfa_gap_trace_construct_after_residuebound. pfa_gap_trace_construct_after_residuebound + S (x5) = (p)) /\ ((exists pfa_offset_left_trace_construct_after_residuecongruence pfa_offset_right_trace_construct_after_residuecongruence. (x2*t+x1) + (p) * pfa_offset_left_trace_construct_after_residuecongruence = (x5) + (p) * pfa_offset_right_trace_construct_after_residuecongruence)))
  126. 0126specialize prime_field_residue_input_equal (p)
  127. 0127specialize prime_field_residue_input_equal (x2*t+x1)
  128. 0128specialize prime_field_residue_input_equal (x3)
  129. 0129specialize prime_field_residue_input_equal (x5)
  130. 0130apply prime_field_residue_input_equal
  131. 0131symm
  132. 0132exact hs_witness_witness_witness_right_right_right
  133. 0133specialize prime_field_polynomial_normalization_entry (p)
  134. 0134specialize prime_field_polynomial_normalization_entry (u)
  135. 0135specialize prime_field_polynomial_normalization_entry (v)
  136. 0136specialize prime_field_polynomial_normalization_entry (U)
  137. 0137specialize prime_field_polynomial_normalization_entry (V)
  138. 0138specialize prime_field_polynomial_normalization_entry (S l)
  139. 0139specialize prime_field_polynomial_normalization_entry (S i)
  140. 0140specialize prime_field_polynomial_normalization_entry (x3)
  141. 0141specialize prime_field_polynomial_normalization_entry (x5)
  142. 0142apply prime_field_polynomial_normalization_entry
  143. 0143exact hred
  144. 0144specialize succ_le_succ (S i)
  145. 0145specialize succ_le_succ (l)
  146. 0146apply succ_le_succ
  147. 0147exact hi
  148. 0148exact hs_witness_witness_witness_right_right_left
  149. 0149exact ha_witness
  150. 0150have hop : exists k. ((((exists pfa_gap_trace_construct_multiplyleft. pfa_gap_trace_construct_multiplyleft + S (x4) = (p)) /\ (((exists pfa_gap_trace_construct_multiplyright. pfa_gap_trace_construct_multiplyright + S (t) = (p)) /\ ((((exists pfa_gap_trace_construct_multiplyresultbound. pfa_gap_trace_construct_multiplyresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_trace_construct_multiplyresultcongruence pfa_offset_right_trace_construct_multiplyresultcongruence. ((x4) * (t)) + (p) * pfa_offset_left_trace_construct_multiplyresultcongruence = (k) + (p) * pfa_offset_right_trace_construct_multiplyresultcongruence))))))))) /\ ((((exists pfa_gap_trace_construct_addleft. pfa_gap_trace_construct_addleft + S (k) = (p)) /\ (((exists pfa_gap_trace_construct_addright. pfa_gap_trace_construct_addright + S (x1) = (p)) /\ ((((exists pfa_gap_trace_construct_addresultbound. pfa_gap_trace_construct_addresultbound + S (x5) = (p)) /\ ((exists pfa_offset_left_trace_construct_addresultcongruence pfa_offset_right_trace_construct_addresultcongruence. ((k) + (x1)) + (p) * pfa_offset_left_trace_construct_addresultcongruence = (x5) + (p) * pfa_offset_right_trace_construct_addresultcongruence)))))))))))
  151. 0151specialize prime_field_polynomial_horner_canonical_step (p)
  152. 0152specialize prime_field_polynomial_horner_canonical_step (x2)
  153. 0153specialize prime_field_polynomial_horner_canonical_step (t)
  154. 0154specialize prime_field_polynomial_horner_canonical_step (x1)
  155. 0155specialize prime_field_polynomial_horner_canonical_step (x4)
  156. 0156specialize prime_field_polynomial_horner_canonical_step (x5)
  157. 0157apply prime_field_polynomial_horner_canonical_step
  158. 0158exact hp
  159. 0159exact ht
  160. 0160specialize matrix_rank_bounded_prefix_value (b)
  161. 0161specialize matrix_rank_bounded_prefix_value (c)
  162. 0162specialize matrix_rank_bounded_prefix_value (l)
  163. 0163specialize matrix_rank_bounded_prefix_value (p)
  164. 0164specialize matrix_rank_bounded_prefix_value (i)
  165. 0165specialize matrix_rank_bounded_prefix_value (x1)
  166. 0166apply matrix_rank_bounded_prefix_value
  167. 0167exact hc
  168. 0168exact hi
  169. 0169exact hs_witness_witness_witness_left
  170. 0170exact hbefore
  171. 0171exact hafter
  172. 0172cases hop
  173. 0173cases hop_witness
  174. 0174exists x1
  175. 0175exists x4
  176. 0176exists x5
  177. 0177exists x6
  178. 0178split
  179. 0179exact hs_witness_witness_witness_left
  180. 0180split
  181. 0181exact hb_witness
  182. 0182split
  183. 0183exact ha_witness
  184. 0184split
  185. 0185exact hop_witness_left
  186. 0186exact hop_witness_right
  187. 0187exact hr