PP0023

prime_field_polynomial_horner_input_bounds

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 0 declared prerequisites and contains 34 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

PP0027 prime_field_polynomial_horner_normalization_residue PP0028 prime_field_polynomial_horner_residue PP002C prime_field_polynomial_horner_successor_construct

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

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.

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–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
  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 exact 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 : exists pfh_coefficient_bounds_step pfh_before_bounds_step pfh_after_bounds_step pfh_product_bounds_step. ((((exists ff_h_pfp_bounds_stepcoefficient. ff_h_pfp_bounds_stepcoefficient + S (pfh_coefficient_bounds_step) = S ((S (i)) * c)) /\ exists ff_q_pfp_bounds_stepcoefficient. b = ff_q_pfp_bounds_stepcoefficient * S ((S (i)) * c) + (pfh_coefficient_bounds_step))) /\ (((((exists ff_h_pfp_bounds_stepbefore. ff_h_pfp_bounds_stepbefore + S (pfh_before_bounds_step) = S ((S (i)) * x1)) /\ exists ff_q_pfp_bounds_stepbefore. x = ff_q_pfp_bounds_stepbefore * S ((S (i)) * x1) + (pfh_before_bounds_step))) /\ (((((exists ff_h_pfp_bounds_stepafter. ff_h_pfp_bounds_stepafter + S (pfh_after_bounds_step) = S ((S (S (i))) * x1)) /\ exists ff_q_pfp_bounds_stepafter. x = ff_q_pfp_bounds_stepafter * S ((S (S (i))) * x1) + (pfh_after_bounds_step))) /\ (((((exists pfa_gap_bounds_stepmultiplyleft. pfa_gap_bounds_stepmultiplyleft + S (pfh_before_bounds_step) = (p)) /\ (((exists pfa_gap_bounds_stepmultiplyright. pfa_gap_bounds_stepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_bounds_stepmultiplyresultbound. pfa_gap_bounds_stepmultiplyresultbound + S (pfh_product_bounds_step) = (p)) /\ ((exists pfa_offset_left_bounds_stepmultiplyresultcongruence pfa_offset_right_bounds_stepmultiplyresultcongruence. ((pfh_before_bounds_step) * (t)) + (p) * pfa_offset_left_bounds_stepmultiplyresultcongruence = (pfh_product_bounds_step) + (p) * pfa_offset_right_bounds_stepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_bounds_stepaddleft. pfa_gap_bounds_stepaddleft + S (pfh_product_bounds_step) = (p)) /\ (((exists pfa_gap_bounds_stepaddright. pfa_gap_bounds_stepaddright + S (pfh_coefficient_bounds_step) = (p)) /\ ((((exists pfa_gap_bounds_stepaddresultbound. pfa_gap_bounds_stepaddresultbound + S (pfh_after_bounds_step) = (p)) /\ ((exists pfa_offset_left_bounds_stepaddresultcongruence pfa_offset_right_bounds_stepaddresultcongruence. ((pfh_product_bounds_step) + (pfh_coefficient_bounds_step)) + (p) * pfa_offset_left_bounds_stepaddresultcongruence = (pfh_after_bounds_step) + (p) * pfa_offset_right_bounds_stepaddresultcongruence)))))))))))))))))
  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