PQ004C

prime_field_polynomial_synthetic_functional

The remainder and all decoded quotient values are unique, independently of either beta encoding or the chosen execution history.

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

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

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ a. ∀ n. ∀ qb. ∀ qc. ∀ r. ∀ Qb. ∀ Qc. ∀ s. Prime(p) → FpSyntheticDivision(p,b,c,a,n,qb,qc,r) → FpSyntheticDivision(p,b,c,a,n,Qb,Qc,s) → r = s ∧ (∀ x. ∀ y. Lt(x,n) → BetaAt(qb,qc,x,y) → BetaAt(Qb,Qc,x,y))

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

Definition DAG

FpSyntheticDivision(p,b,c,a,n,qb,qc,r) · 2Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 3

Actual proof prerequisites

prime_field_polynomial_horner_functional · checked external prerequisiteprime_field_polynomial_synthetic_remainder_executionbeta_at_exists · checked external prerequisiteprime_field_polynomial_synthetic_quotient_entry
Original expanded first-order statement 
forall p b c a n qb qc r Qb Qc s. (~((p) = 1) /\ forall pfa_factor_left_functional_prime pfa_factor_right_functional_prime. (p) = pfa_factor_left_functional_prime * pfa_factor_right_functional_prime -> pfa_factor_left_functional_prime = 1 \/ pfa_factor_right_functional_prime = 1) -> (exists pfs_history_code_functional_first pfs_history_scale_functional_first. ((((exists pfa_gap_functional_firsttracebase. pfa_gap_functional_firsttracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_functional_firsttraceinitial. ff_h_pfp_functional_firsttraceinitial + S (0) = S ((S (0)) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceinitial. pfs_history_code_functional_first = ff_q_pfp_functional_firsttraceinitial * S ((S (0)) * pfs_history_scale_functional_first) + (0))) /\ (((((exists ff_h_pfp_functional_firsttraceterminal. ff_h_pfp_functional_firsttraceterminal + S (r) = S ((S (S (n))) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceterminal. pfs_history_code_functional_first = ff_q_pfp_functional_firsttraceterminal * S ((S (S (n))) * pfs_history_scale_functional_first) + (r))) /\ ((forall pfh_index_functional_firsttracesteps. (exists pfa_gap_functional_firsttracestepsindex. pfa_gap_functional_firsttracestepsindex + S (pfh_index_functional_firsttracesteps) = (S (n))) -> (exists pfh_coefficient_functional_firsttracestepsstep pfh_before_functional_firsttracestepsstep pfh_after_functional_firsttracestepsstep pfh_product_functional_firsttracestepsstep. ((((exists ff_h_pfp_functional_firsttracestepsstepcoefficient. ff_h_pfp_functional_firsttracestepsstepcoefficient + S (pfh_coefficient_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * c)) /\ exists ff_q_pfp_functional_firsttracestepsstepcoefficient. b = ff_q_pfp_functional_firsttracestepsstepcoefficient * S ((S (pfh_index_functional_firsttracesteps)) * c) + (pfh_coefficient_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepbefore. ff_h_pfp_functional_firsttracestepsstepbefore + S (pfh_before_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepbefore. pfs_history_code_functional_first = ff_q_pfp_functional_firsttracestepsstepbefore * S ((S (pfh_index_functional_firsttracesteps)) * pfs_history_scale_functional_first) + (pfh_before_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepafter. ff_h_pfp_functional_firsttracestepsstepafter + S (pfh_after_functional_firsttracestepsstep) = S ((S (S (pfh_index_functional_firsttracesteps))) * pfs_history_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepafter. pfs_history_code_functional_first = ff_q_pfp_functional_firsttracestepsstepafter * S ((S (S (pfh_index_functional_firsttracesteps))) * pfs_history_scale_functional_first) + (pfh_after_functional_firsttracestepsstep))) /\ (((((exists pfa_gap_functional_firsttracestepsstepmultiplyleft. pfa_gap_functional_firsttracestepsstepmultiplyleft + S (pfh_before_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepmultiplyright. pfa_gap_functional_firsttracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepmultiplyresultbound. pfa_gap_functional_firsttracestepsstepmultiplyresultbound + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence. ((pfh_before_functional_firsttracestepsstep) * (a)) + (p) * pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence = (pfh_product_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddleft. pfa_gap_functional_firsttracestepsstepaddleft + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepaddright. pfa_gap_functional_firsttracestepsstepaddright + S (pfh_coefficient_functional_firsttracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddresultbound. pfa_gap_functional_firsttracestepsstepaddresultbound + S (pfh_after_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepaddresultcongruence pfa_offset_right_functional_firsttracestepsstepaddresultcongruence. ((pfh_product_functional_firsttracestepsstep) + (pfh_coefficient_functional_firsttracestepsstep)) + (p) * pfa_offset_left_functional_firsttracestepsstepaddresultcongruence = (pfh_after_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_functional_firstquotient ff_source_mcp_pfs_functional_firstquotient ff_target_mcp_pfs_functional_firstquotient. (exists mcp_gap_pfs_functional_firstquotient_bound. mcp_gap_pfs_functional_firstquotient_bound + S (ff_index_mcp_pfs_functional_firstquotient) = (n)) -> (((exists fs_h_mcp_pfs_functional_firstquotient_source. fs_h_mcp_pfs_functional_firstquotient_source + S (ff_source_mcp_pfs_functional_firstquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_functional_firstquotient)) * pfs_history_scale_functional_first)) /\ exists fs_q_mcp_pfs_functional_firstquotient_source. pfs_history_code_functional_first = fs_q_mcp_pfs_functional_firstquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_functional_firstquotient)) * pfs_history_scale_functional_first) + (ff_source_mcp_pfs_functional_firstquotient))) -> (((exists fs_h_mcp_pfs_functional_firstquotient_target. fs_h_mcp_pfs_functional_firstquotient_target + S (ff_target_mcp_pfs_functional_firstquotient) = S ((S (ff_index_mcp_pfs_functional_firstquotient)) * qc)) /\ exists fs_q_mcp_pfs_functional_firstquotient_target. qb = fs_q_mcp_pfs_functional_firstquotient_target * S ((S (ff_index_mcp_pfs_functional_firstquotient)) * qc) + (ff_target_mcp_pfs_functional_firstquotient))) -> ff_target_mcp_pfs_functional_firstquotient = ff_source_mcp_pfs_functional_firstquotient)))) -> (exists pfs_history_code_functional_second pfs_history_scale_functional_second. ((((exists pfa_gap_functional_secondtracebase. pfa_gap_functional_secondtracebase + S (a) = (p)) /\ (((((exists ff_h_pfp_functional_secondtraceinitial. ff_h_pfp_functional_secondtraceinitial + S (0) = S ((S (0)) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceinitial. pfs_history_code_functional_second = ff_q_pfp_functional_secondtraceinitial * S ((S (0)) * pfs_history_scale_functional_second) + (0))) /\ (((((exists ff_h_pfp_functional_secondtraceterminal. ff_h_pfp_functional_secondtraceterminal + S (s) = S ((S (S (n))) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceterminal. pfs_history_code_functional_second = ff_q_pfp_functional_secondtraceterminal * S ((S (S (n))) * pfs_history_scale_functional_second) + (s))) /\ ((forall pfh_index_functional_secondtracesteps. (exists pfa_gap_functional_secondtracestepsindex. pfa_gap_functional_secondtracestepsindex + S (pfh_index_functional_secondtracesteps) = (S (n))) -> (exists pfh_coefficient_functional_secondtracestepsstep pfh_before_functional_secondtracestepsstep pfh_after_functional_secondtracestepsstep pfh_product_functional_secondtracestepsstep. ((((exists ff_h_pfp_functional_secondtracestepsstepcoefficient. ff_h_pfp_functional_secondtracestepsstepcoefficient + S (pfh_coefficient_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * c)) /\ exists ff_q_pfp_functional_secondtracestepsstepcoefficient. b = ff_q_pfp_functional_secondtracestepsstepcoefficient * S ((S (pfh_index_functional_secondtracesteps)) * c) + (pfh_coefficient_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepbefore. ff_h_pfp_functional_secondtracestepsstepbefore + S (pfh_before_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepbefore. pfs_history_code_functional_second = ff_q_pfp_functional_secondtracestepsstepbefore * S ((S (pfh_index_functional_secondtracesteps)) * pfs_history_scale_functional_second) + (pfh_before_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepafter. ff_h_pfp_functional_secondtracestepsstepafter + S (pfh_after_functional_secondtracestepsstep) = S ((S (S (pfh_index_functional_secondtracesteps))) * pfs_history_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepafter. pfs_history_code_functional_second = ff_q_pfp_functional_secondtracestepsstepafter * S ((S (S (pfh_index_functional_secondtracesteps))) * pfs_history_scale_functional_second) + (pfh_after_functional_secondtracestepsstep))) /\ (((((exists pfa_gap_functional_secondtracestepsstepmultiplyleft. pfa_gap_functional_secondtracestepsstepmultiplyleft + S (pfh_before_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepmultiplyright. pfa_gap_functional_secondtracestepsstepmultiplyright + S (a) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepmultiplyresultbound. pfa_gap_functional_secondtracestepsstepmultiplyresultbound + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence. ((pfh_before_functional_secondtracestepsstep) * (a)) + (p) * pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence = (pfh_product_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddleft. pfa_gap_functional_secondtracestepsstepaddleft + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepaddright. pfa_gap_functional_secondtracestepsstepaddright + S (pfh_coefficient_functional_secondtracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddresultbound. pfa_gap_functional_secondtracestepsstepaddresultbound + S (pfh_after_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepaddresultcongruence pfa_offset_right_functional_secondtracestepsstepaddresultcongruence. ((pfh_product_functional_secondtracestepsstep) + (pfh_coefficient_functional_secondtracestepsstep)) + (p) * pfa_offset_left_functional_secondtracestepsstepaddresultcongruence = (pfh_after_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((forall ff_index_mcp_pfs_functional_secondquotient ff_source_mcp_pfs_functional_secondquotient ff_target_mcp_pfs_functional_secondquotient. (exists mcp_gap_pfs_functional_secondquotient_bound. mcp_gap_pfs_functional_secondquotient_bound + S (ff_index_mcp_pfs_functional_secondquotient) = (n)) -> (((exists fs_h_mcp_pfs_functional_secondquotient_source. fs_h_mcp_pfs_functional_secondquotient_source + S (ff_source_mcp_pfs_functional_secondquotient) = S ((S ((1) + (1) * ff_index_mcp_pfs_functional_secondquotient)) * pfs_history_scale_functional_second)) /\ exists fs_q_mcp_pfs_functional_secondquotient_source. pfs_history_code_functional_second = fs_q_mcp_pfs_functional_secondquotient_source * S ((S ((1) + (1) * ff_index_mcp_pfs_functional_secondquotient)) * pfs_history_scale_functional_second) + (ff_source_mcp_pfs_functional_secondquotient))) -> (((exists fs_h_mcp_pfs_functional_secondquotient_target. fs_h_mcp_pfs_functional_secondquotient_target + S (ff_target_mcp_pfs_functional_secondquotient) = S ((S (ff_index_mcp_pfs_functional_secondquotient)) * Qc)) /\ exists fs_q_mcp_pfs_functional_secondquotient_target. Qb = fs_q_mcp_pfs_functional_secondquotient_target * S ((S (ff_index_mcp_pfs_functional_secondquotient)) * Qc) + (ff_target_mcp_pfs_functional_secondquotient))) -> ff_target_mcp_pfs_functional_secondquotient = ff_source_mcp_pfs_functional_secondquotient)))) -> ((r=s) /\ ((forall mdr_i_pfp_functional_values mdr_a_pfp_functional_values. (exists mdr_gap_pfp_functional_valuesb. mdr_gap_pfp_functional_valuesb + S (mdr_i_pfp_functional_values) = (n)) -> (((exists ff_h_mdr_pfp_functional_valueso. ff_h_mdr_pfp_functional_valueso + S (mdr_a_pfp_functional_values) = S ((S (mdr_i_pfp_functional_values)) * qc)) /\ exists ff_q_mdr_pfp_functional_valueso. qb = ff_q_mdr_pfp_functional_valueso * S ((S (mdr_i_pfp_functional_values)) * qc) + (mdr_a_pfp_functional_values))) -> (((exists ff_h_mdr_pfp_functional_valuesn. ff_h_mdr_pfp_functional_valuesn + S (mdr_a_pfp_functional_values) = S ((S (mdr_i_pfp_functional_values)) * Qc)) /\ exists ff_q_mdr_pfp_functional_valuesn. Qb = ff_q_mdr_pfp_functional_valuesn * S ((S (mdr_i_pfp_functional_values)) * Qc) + (mdr_a_pfp_functional_values))))))

Complete tactic proof in conservative notation

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

95 script commands · 15 reading checkpoints · 2 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
prime field polynomial synthetic remainder executionprime field polynomial synthetic quotient entry
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 a
  5. L5
    intro n
  6. L6
    intro qb
  7. L7
    intro qc
  8. L8
    intro r
  9. L9
    intro Qb
  10. L10
    intro Qc
02Fix variables and assumptionsL11–14

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

  1. L11
    intro s
  2. L12
    intro hp
  3. L13
    intro hq
  4. L14
    intro hQ
03Separate the logical casesL15–15

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

  1. L15
    split
04Use earlier factsL16–25

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

  1. L16
    specialize prime_field_polynomial_horner_functional (p)
  2. L17
    specialize prime_field_polynomial_horner_functional (b)
  3. L18
    specialize prime_field_polynomial_horner_functional (c)
  4. L19
    specialize prime_field_polynomial_horner_functional (a)
  5. L20
    specialize prime_field_polynomial_horner_functional (S n)
  6. L21
    specialize prime_field_polynomial_horner_functional (r)
  7. L22
    specialize prime_field_polynomial_horner_functional (s)
  8. L23
    apply prime_field_polynomial_horner_functional
  9. L24
    exact hp
  10. L25
    specialize prime_field_polynomial_synthetic_remainder_execution (p)
05Use earlier factsL26–35

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

  1. L26
    specialize prime_field_polynomial_synthetic_remainder_execution (b)
  2. L27
    specialize prime_field_polynomial_synthetic_remainder_execution (c)
  3. L28
    specialize prime_field_polynomial_synthetic_remainder_execution (a)
  4. L29
    specialize prime_field_polynomial_synthetic_remainder_execution (n)
  5. L30
    specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  6. L31
    specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  7. L32
    specialize prime_field_polynomial_synthetic_remainder_execution (r)
  8. L33
    apply prime_field_polynomial_synthetic_remainder_execution
  9. L34
    exact hq
  10. L35
    specialize prime_field_polynomial_synthetic_remainder_execution (p)
06Use earlier factsL36–44

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

  1. L36
    specialize prime_field_polynomial_synthetic_remainder_execution (b)
  2. L37
    specialize prime_field_polynomial_synthetic_remainder_execution (c)
  3. L38
    specialize prime_field_polynomial_synthetic_remainder_execution (a)
  4. L39
    specialize prime_field_polynomial_synthetic_remainder_execution (n)
  5. L40
    specialize prime_field_polynomial_synthetic_remainder_execution (Qb)
  6. L41
    specialize prime_field_polynomial_synthetic_remainder_execution (Qc)
  7. L42
    specialize prime_field_polynomial_synthetic_remainder_execution (s)
  8. L43
    apply prime_field_polynomial_synthetic_remainder_execution
  9. L44
    exact hQ
07Fix variables and assumptionsL45–48

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

  1. L45
    intro i
  2. L46
    intro h
  3. L47
    intro hi
  4. L48
    intro hh
08Establish htL49–53

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

  1. L49
    have ht : ∃ z. BetaAt(Qb,Qc,i,z)Definitions: BetaAt(Qb,Qc,i,z)Original native command in the exact edition
  2. L50
    specialize beta_at_exists (Qb)
  3. L51
    specialize beta_at_exists (Qc)
  4. L52
    specialize beta_at_exists (i)
  5. L53
    apply beta_at_exists
09Separate the logical casesL54–54

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

  1. L54
    cases ht
10Establish heqL55–64

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

  1. L55
    have heq : x=h
  2. L56
    specialize prime_field_polynomial_horner_functional (p)
  3. L57
    specialize prime_field_polynomial_horner_functional (b)
  4. L58
    specialize prime_field_polynomial_horner_functional (c)
  5. L59
    specialize prime_field_polynomial_horner_functional (a)
  6. L60
    specialize prime_field_polynomial_horner_functional (S i)
  7. L61
    specialize prime_field_polynomial_horner_functional (x)
  8. L62
    specialize prime_field_polynomial_horner_functional (h)
  9. L63
    apply prime_field_polynomial_horner_functional
  10. L64
    exact hp
11Use earlier factsL65–74

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

  1. L65
    specialize prime_field_polynomial_synthetic_quotient_entry (p)
  2. L66
    specialize prime_field_polynomial_synthetic_quotient_entry (b)
  3. L67
    specialize prime_field_polynomial_synthetic_quotient_entry (c)
  4. L68
    specialize prime_field_polynomial_synthetic_quotient_entry (a)
  5. L69
    specialize prime_field_polynomial_synthetic_quotient_entry (n)
  6. L70
    specialize prime_field_polynomial_synthetic_quotient_entry (Qb)
  7. L71
    specialize prime_field_polynomial_synthetic_quotient_entry (Qc)
  8. L72
    specialize prime_field_polynomial_synthetic_quotient_entry (s)
  9. L73
    specialize prime_field_polynomial_synthetic_quotient_entry (i)
  10. L74
    specialize prime_field_polynomial_synthetic_quotient_entry (x)
12Use earlier factsL75–84

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

  1. L75
    apply prime_field_polynomial_synthetic_quotient_entry
  2. L76
    exact hQ
  3. L77
    exact hi
  4. L78
    exact ht_witness
  5. L79
    specialize prime_field_polynomial_synthetic_quotient_entry (p)
  6. L80
    specialize prime_field_polynomial_synthetic_quotient_entry (b)
  7. L81
    specialize prime_field_polynomial_synthetic_quotient_entry (c)
  8. L82
    specialize prime_field_polynomial_synthetic_quotient_entry (a)
  9. L83
    specialize prime_field_polynomial_synthetic_quotient_entry (n)
  10. L84
    specialize prime_field_polynomial_synthetic_quotient_entry (qb)
13Use earlier factsL85–92

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

  1. L85
    specialize prime_field_polynomial_synthetic_quotient_entry (qc)
  2. L86
    specialize prime_field_polynomial_synthetic_quotient_entry (r)
  3. L87
    specialize prime_field_polynomial_synthetic_quotient_entry (i)
  4. L88
    specialize prime_field_polynomial_synthetic_quotient_entry (h)
  5. L89
    apply prime_field_polynomial_synthetic_quotient_entry
  6. L90
    exact hq
  7. L91
    exact hi
  8. L92
    exact hh
14Calculate and transport equalitiesL93–94

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

  1. L93
    rewrite heq at ht_witness
  2. L94
    rewrite heq at ht_witness
15Use earlier factsL95–95

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

  1. L95
    exact ht_witness

Library-wide reading audit

Original defined command ledger · 95 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro a
  5. 0005intro n
  6. 0006intro qb
  7. 0007intro qc
  8. 0008intro r
  9. 0009intro Qb
  10. 0010intro Qc
  11. 0011intro s
  12. 0012intro hp
  13. 0013intro hq
  14. 0014intro hQ
  15. 0015split
  16. 0016specialize prime_field_polynomial_horner_functional (p)
  17. 0017specialize prime_field_polynomial_horner_functional (b)
  18. 0018specialize prime_field_polynomial_horner_functional (c)
  19. 0019specialize prime_field_polynomial_horner_functional (a)
  20. 0020specialize prime_field_polynomial_horner_functional (S n)
  21. 0021specialize prime_field_polynomial_horner_functional (r)
  22. 0022specialize prime_field_polynomial_horner_functional (s)
  23. 0023apply prime_field_polynomial_horner_functional
  24. 0024exact hp
  25. 0025specialize prime_field_polynomial_synthetic_remainder_execution (p)
  26. 0026specialize prime_field_polynomial_synthetic_remainder_execution (b)
  27. 0027specialize prime_field_polynomial_synthetic_remainder_execution (c)
  28. 0028specialize prime_field_polynomial_synthetic_remainder_execution (a)
  29. 0029specialize prime_field_polynomial_synthetic_remainder_execution (n)
  30. 0030specialize prime_field_polynomial_synthetic_remainder_execution (qb)
  31. 0031specialize prime_field_polynomial_synthetic_remainder_execution (qc)
  32. 0032specialize prime_field_polynomial_synthetic_remainder_execution (r)
  33. 0033apply prime_field_polynomial_synthetic_remainder_execution
  34. 0034exact hq
  35. 0035specialize prime_field_polynomial_synthetic_remainder_execution (p)
  36. 0036specialize prime_field_polynomial_synthetic_remainder_execution (b)
  37. 0037specialize prime_field_polynomial_synthetic_remainder_execution (c)
  38. 0038specialize prime_field_polynomial_synthetic_remainder_execution (a)
  39. 0039specialize prime_field_polynomial_synthetic_remainder_execution (n)
  40. 0040specialize prime_field_polynomial_synthetic_remainder_execution (Qb)
  41. 0041specialize prime_field_polynomial_synthetic_remainder_execution (Qc)
  42. 0042specialize prime_field_polynomial_synthetic_remainder_execution (s)
  43. 0043apply prime_field_polynomial_synthetic_remainder_execution
  44. 0044exact hQ
  45. 0045intro i
  46. 0046intro h
  47. 0047intro hi
  48. 0048intro hh
  49. 0049have ht : ∃ z. BetaAt(Qb,Qc,i,z)
  50. 0050specialize beta_at_exists (Qb)
  51. 0051specialize beta_at_exists (Qc)
  52. 0052specialize beta_at_exists (i)
  53. 0053apply beta_at_exists
  54. 0054cases ht
  55. 0055have heq : x=h
  56. 0056specialize prime_field_polynomial_horner_functional (p)
  57. 0057specialize prime_field_polynomial_horner_functional (b)
  58. 0058specialize prime_field_polynomial_horner_functional (c)
  59. 0059specialize prime_field_polynomial_horner_functional (a)
  60. 0060specialize prime_field_polynomial_horner_functional (S i)
  61. 0061specialize prime_field_polynomial_horner_functional (x)
  62. 0062specialize prime_field_polynomial_horner_functional (h)
  63. 0063apply prime_field_polynomial_horner_functional
  64. 0064exact hp
  65. 0065specialize prime_field_polynomial_synthetic_quotient_entry (p)
  66. 0066specialize prime_field_polynomial_synthetic_quotient_entry (b)
  67. 0067specialize prime_field_polynomial_synthetic_quotient_entry (c)
  68. 0068specialize prime_field_polynomial_synthetic_quotient_entry (a)
  69. 0069specialize prime_field_polynomial_synthetic_quotient_entry (n)
  70. 0070specialize prime_field_polynomial_synthetic_quotient_entry (Qb)
  71. 0071specialize prime_field_polynomial_synthetic_quotient_entry (Qc)
  72. 0072specialize prime_field_polynomial_synthetic_quotient_entry (s)
  73. 0073specialize prime_field_polynomial_synthetic_quotient_entry (i)
  74. 0074specialize prime_field_polynomial_synthetic_quotient_entry (x)
  75. 0075apply prime_field_polynomial_synthetic_quotient_entry
  76. 0076exact hQ
  77. 0077exact hi
  78. 0078exact ht_witness
  79. 0079specialize prime_field_polynomial_synthetic_quotient_entry (p)
  80. 0080specialize prime_field_polynomial_synthetic_quotient_entry (b)
  81. 0081specialize prime_field_polynomial_synthetic_quotient_entry (c)
  82. 0082specialize prime_field_polynomial_synthetic_quotient_entry (a)
  83. 0083specialize prime_field_polynomial_synthetic_quotient_entry (n)
  84. 0084specialize prime_field_polynomial_synthetic_quotient_entry (qb)
  85. 0085specialize prime_field_polynomial_synthetic_quotient_entry (qc)
  86. 0086specialize prime_field_polynomial_synthetic_quotient_entry (r)
  87. 0087specialize prime_field_polynomial_synthetic_quotient_entry (i)
  88. 0088specialize prime_field_polynomial_synthetic_quotient_entry (h)
  89. 0089apply prime_field_polynomial_synthetic_quotient_entry
  90. 0090exact hq
  91. 0091exact hi
  92. 0092exact hh
  93. 0093rewrite heq at ht_witness
  94. 0094rewrite heq at ht_witness
  95. 0095exact ht_witness