PP0023

prime_field_polynomial_horner_input_bounds

The actual execution graph entails canonical input coefficients and base; no separate input-bound certificates are hidden in its steps.

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

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

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

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ t. ∀ l. ∀ r. FpHorner(p,b,c,t,l,r) → Lt(t,p) ∧ BetaPrefixInto(b,c,l,p)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1FpHornerStep(p,b,c,x,u,v,i) · 1FpHorner(p,b,c,x,l,r) · 1Lt(a,b) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall p b c t l r. (exists pfh_trace_code_input_bounds_execution pfh_trace_scale_input_bounds_execution. (((exists pfa_gap_input_bounds_executiontracebase. pfa_gap_input_bounds_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_input_bounds_executiontraceinitial. ff_h_pfp_input_bounds_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_input_bounds_execution)) /\ exists ff_q_pfp_input_bounds_executiontraceinitial. pfh_trace_code_input_bounds_execution = ff_q_pfp_input_bounds_executiontraceinitial * S ((S (0)) * pfh_trace_scale_input_bounds_execution) + (0))) /\ (((((exists ff_h_pfp_input_bounds_executiontraceterminal. ff_h_pfp_input_bounds_executiontraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_input_bounds_execution)) /\ exists ff_q_pfp_input_bounds_executiontraceterminal. pfh_trace_code_input_bounds_execution = ff_q_pfp_input_bounds_executiontraceterminal * S ((S (l)) * pfh_trace_scale_input_bounds_execution) + (r))) /\ ((forall pfh_index_input_bounds_executiontracesteps. (exists pfa_gap_input_bounds_executiontracestepsindex. pfa_gap_input_bounds_executiontracestepsindex + S (pfh_index_input_bounds_executiontracesteps) = (l)) -> (exists pfh_coefficient_input_bounds_executiontracestepsstep pfh_before_input_bounds_executiontracestepsstep pfh_after_input_bounds_executiontracestepsstep pfh_product_input_bounds_executiontracestepsstep. ((((exists ff_h_pfp_input_bounds_executiontracestepsstepcoefficient. ff_h_pfp_input_bounds_executiontracestepsstepcoefficient + S (pfh_coefficient_input_bounds_executiontracestepsstep) = S ((S (pfh_index_input_bounds_executiontracesteps)) * c)) /\ exists ff_q_pfp_input_bounds_executiontracestepsstepcoefficient. b = ff_q_pfp_input_bounds_executiontracestepsstepcoefficient * S ((S (pfh_index_input_bounds_executiontracesteps)) * c) + (pfh_coefficient_input_bounds_executiontracestepsstep))) /\ (((((exists ff_h_pfp_input_bounds_executiontracestepsstepbefore. ff_h_pfp_input_bounds_executiontracestepsstepbefore + S (pfh_before_input_bounds_executiontracestepsstep) = S ((S (pfh_index_input_bounds_executiontracesteps)) * pfh_trace_scale_input_bounds_execution)) /\ exists ff_q_pfp_input_bounds_executiontracestepsstepbefore. pfh_trace_code_input_bounds_execution = ff_q_pfp_input_bounds_executiontracestepsstepbefore * S ((S (pfh_index_input_bounds_executiontracesteps)) * pfh_trace_scale_input_bounds_execution) + (pfh_before_input_bounds_executiontracestepsstep))) /\ (((((exists ff_h_pfp_input_bounds_executiontracestepsstepafter. ff_h_pfp_input_bounds_executiontracestepsstepafter + S (pfh_after_input_bounds_executiontracestepsstep) = S ((S (S (pfh_index_input_bounds_executiontracesteps))) * pfh_trace_scale_input_bounds_execution)) /\ exists ff_q_pfp_input_bounds_executiontracestepsstepafter. pfh_trace_code_input_bounds_execution = ff_q_pfp_input_bounds_executiontracestepsstepafter * S ((S (S (pfh_index_input_bounds_executiontracesteps))) * pfh_trace_scale_input_bounds_execution) + (pfh_after_input_bounds_executiontracestepsstep))) /\ (((((exists pfa_gap_input_bounds_executiontracestepsstepmultiplyleft. pfa_gap_input_bounds_executiontracestepsstepmultiplyleft + S (pfh_before_input_bounds_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_input_bounds_executiontracestepsstepmultiplyright. pfa_gap_input_bounds_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_input_bounds_executiontracestepsstepmultiplyresultbound. pfa_gap_input_bounds_executiontracestepsstepmultiplyresultbound + S (pfh_product_input_bounds_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_input_bounds_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_input_bounds_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_input_bounds_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_input_bounds_executiontracestepsstepmultiplyresultcongruence = (pfh_product_input_bounds_executiontracestepsstep) + (p) * pfa_offset_right_input_bounds_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_input_bounds_executiontracestepsstepaddleft. pfa_gap_input_bounds_executiontracestepsstepaddleft + S (pfh_product_input_bounds_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_input_bounds_executiontracestepsstepaddright. pfa_gap_input_bounds_executiontracestepsstepaddright + S (pfh_coefficient_input_bounds_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_input_bounds_executiontracestepsstepaddresultbound. pfa_gap_input_bounds_executiontracestepsstepaddresultbound + S (pfh_after_input_bounds_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_input_bounds_executiontracestepsstepaddresultcongruence pfa_offset_right_input_bounds_executiontracestepsstepaddresultcongruence. ((pfh_product_input_bounds_executiontracestepsstep) + (pfh_coefficient_input_bounds_executiontracestepsstep)) + (p) * pfa_offset_left_input_bounds_executiontracestepsstepaddresultcongruence = (pfh_after_input_bounds_executiontracestepsstep) + (p) * pfa_offset_right_input_bounds_executiontracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> ((exists pfa_gap_input_bounds_base. pfa_gap_input_bounds_base + S (t) = (p)) /\ ((forall fom_index_pfp_input_bounds_coefficients. (exists fom_gap_pfp_input_bounds_coefficients_index_bound. fom_gap_pfp_input_bounds_coefficients_index_bound + S (fom_index_pfp_input_bounds_coefficients) = l) -> exists fom_value_pfp_input_bounds_coefficients. ((((exists fom_beta_height_pfp_input_bounds_coefficients_entry. fom_beta_height_pfp_input_bounds_coefficients_entry + S (fom_value_pfp_input_bounds_coefficients) = S ((S (fom_index_pfp_input_bounds_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_input_bounds_coefficients_entry. b = fom_beta_quotient_pfp_input_bounds_coefficients_entry * S ((S (fom_index_pfp_input_bounds_coefficients)) * c) + (fom_value_pfp_input_bounds_coefficients))) /\ (exists fom_gap_pfp_input_bounds_coefficients_value_bound. fom_gap_pfp_input_bounds_coefficients_value_bound + S (fom_value_pfp_input_bounds_coefficients) = p)))))

Complete tactic proof in conservative notation

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

34 script commands · 9 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–7

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 r
  7. L7
    intro h
02Separate the logical casesL8–13

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

  1. L8
    cases h
  2. L9
    cases h_witness
  3. L10
    cases h_witness_witness
  4. L11
    cases h_witness_witness_right
  5. L12
    cases h_witness_witness_right_right
  6. L13
    split
03Use earlier factsL14–14

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

  1. L14
    exact h_witness_witness_left
04Fix variables and assumptionsL15–16

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

  1. L15
    intro i
  2. L16
    intro hi
05Establish hsL17–20

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

  1. L17
    have hs : FpHornerStep(p,b,c,t,x,x1,i)Definitions: FpHornerStep(p,b,c,t,x,x1,i)Original native command in the exact edition
  2. L18
    specialize h_witness_witness_right_right_right (i)
  3. L19
    apply h_witness_witness_right_right_right
  4. L20
    exact hi
06Separate the logical casesL21–30

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

  1. L21
    cases hs
  2. L22
    cases hs_witness
  3. L23
    cases hs_witness_witness
  4. L24
    cases hs_witness_witness_witness
  5. L25
    cases hs_witness_witness_witness_witness
  6. L26
    cases hs_witness_witness_witness_witness_right
  7. L27
    cases hs_witness_witness_witness_witness_right_right
  8. L28
    cases hs_witness_witness_witness_witness_right_right_right
  9. L29
    cases hs_witness_witness_witness_witness_right_right_right_right
  10. L30
    cases hs_witness_witness_witness_witness_right_right_right_right_right
07Construct an explicit witnessL31–31

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

  1. L31
    exists x2
08Separate the logical casesL32–32

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

  1. L32
    split
09Use earlier factsL33–34

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

  1. L33
    exact hs_witness_witness_witness_witness_left
  2. L34
    exact hs_witness_witness_witness_witness_right_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro r
  7. 0007intro h
  8. 0008cases h
  9. 0009cases h_witness
  10. 0010cases h_witness_witness
  11. 0011cases h_witness_witness_right
  12. 0012cases h_witness_witness_right_right
  13. 0013split
  14. 0014exact h_witness_witness_left
  15. 0015intro i
  16. 0016intro hi
  17. 0017have hs : FpHornerStep(p,b,c,t,x,x1,i)
  18. 0018specialize h_witness_witness_right_right_right (i)
  19. 0019apply h_witness_witness_right_right_right
  20. 0020exact hi
  21. 0021cases hs
  22. 0022cases hs_witness
  23. 0023cases hs_witness_witness
  24. 0024cases hs_witness_witness_witness
  25. 0025cases hs_witness_witness_witness_witness
  26. 0026cases hs_witness_witness_witness_witness_right
  27. 0027cases hs_witness_witness_witness_witness_right_right
  28. 0028cases hs_witness_witness_witness_witness_right_right_right
  29. 0029cases hs_witness_witness_witness_witness_right_right_right_right
  30. 0030cases hs_witness_witness_witness_witness_right_right_right_right_right
  31. 0031exists x2
  32. 0032split
  33. 0033exact hs_witness_witness_witness_witness_left
  34. 0034exact hs_witness_witness_witness_witness_right_right_right_right_right_left