PQ0006

prime_field_polynomial_negate_bounded

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

The actual operation graph itself forces every source and result coefficient to be canonical.

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 ab ac rb rc l. (forall pfs_index_negate_bounded_graph. (exists pfa_gap_negate_bounded_graphindex. pfa_gap_negate_bounded_graphindex + S (pfs_index_negate_bounded_graph) = (l)) -> exists pfs_source_negate_bounded_graph pfs_result_negate_bounded_graph. ((((exists ff_h_pfp_negate_bounded_graphsource. ff_h_pfp_negate_bounded_graphsource + S (pfs_source_negate_bounded_graph) = S ((S (pfs_index_negate_bounded_graph)) * ac)) /\ exists ff_q_pfp_negate_bounded_graphsource. ab = ff_q_pfp_negate_bounded_graphsource * S ((S (pfs_index_negate_bounded_graph)) * ac) + (pfs_source_negate_bounded_graph))) /\ (((((exists ff_h_pfp_negate_bounded_graphresult. ff_h_pfp_negate_bounded_graphresult + S (pfs_result_negate_bounded_graph) = S ((S (pfs_index_negate_bounded_graph)) * rc)) /\ exists ff_q_pfp_negate_bounded_graphresult. rb = ff_q_pfp_negate_bounded_graphresult * S ((S (pfs_index_negate_bounded_graph)) * rc) + (pfs_result_negate_bounded_graph))) /\ ((((exists pfa_gap_negate_bounded_graphoperationadditionleft. pfa_gap_negate_bounded_graphoperationadditionleft + S (pfs_source_negate_bounded_graph) = (p)) /\ (((exists pfa_gap_negate_bounded_graphoperationadditionright. pfa_gap_negate_bounded_graphoperationadditionright + S (pfs_result_negate_bounded_graph) = (p)) /\ ((((exists pfa_gap_negate_bounded_graphoperationadditionresultbound. pfa_gap_negate_bounded_graphoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_bounded_graphoperationadditionresultcongruence pfa_offset_right_negate_bounded_graphoperationadditionresultcongruence. ((pfs_source_negate_bounded_graph) + (pfs_result_negate_bounded_graph)) + (p) * pfa_offset_left_negate_bounded_graphoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_bounded_graphoperationadditionresultcongruence)))))))))))))) -> ((forall fom_index_pfp_negate_bounded_ab. (exists fom_gap_pfp_negate_bounded_ab_index_bound. fom_gap_pfp_negate_bounded_ab_index_bound + S (fom_index_pfp_negate_bounded_ab) = l) -> exists fom_value_pfp_negate_bounded_ab. ((((exists fom_beta_height_pfp_negate_bounded_ab_entry. fom_beta_height_pfp_negate_bounded_ab_entry + S (fom_value_pfp_negate_bounded_ab) = S ((S (fom_index_pfp_negate_bounded_ab)) * ac)) /\ exists fom_beta_quotient_pfp_negate_bounded_ab_entry. ab = fom_beta_quotient_pfp_negate_bounded_ab_entry * S ((S (fom_index_pfp_negate_bounded_ab)) * ac) + (fom_value_pfp_negate_bounded_ab))) /\ (exists fom_gap_pfp_negate_bounded_ab_value_bound. fom_gap_pfp_negate_bounded_ab_value_bound + S (fom_value_pfp_negate_bounded_ab) = p))) /\ ((forall fom_index_pfp_negate_bounded_rb. (exists fom_gap_pfp_negate_bounded_rb_index_bound. fom_gap_pfp_negate_bounded_rb_index_bound + S (fom_index_pfp_negate_bounded_rb) = l) -> exists fom_value_pfp_negate_bounded_rb. ((((exists fom_beta_height_pfp_negate_bounded_rb_entry. fom_beta_height_pfp_negate_bounded_rb_entry + S (fom_value_pfp_negate_bounded_rb) = S ((S (fom_index_pfp_negate_bounded_rb)) * rc)) /\ exists fom_beta_quotient_pfp_negate_bounded_rb_entry. rb = fom_beta_quotient_pfp_negate_bounded_rb_entry * S ((S (fom_index_pfp_negate_bounded_rb)) * rc) + (fom_value_pfp_negate_bounded_rb))) /\ (exists fom_gap_pfp_negate_bounded_rb_value_bound. fom_gap_pfp_negate_bounded_rb_value_bound + S (fom_value_pfp_negate_bounded_rb) = p)))))

Constructive proof overview

Generated structural guide

The actual operation graph itself forces every source and result coefficient to be canonical.

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

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

Proof neighborhood

Direct dependencies

none

Direct dependents

none

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

42 script commands · 14 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.

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 ab
  3. L3
    intro ac
  4. L4
    intro rb
  5. L5
    intro rc
  6. L6
    intro l
  7. L7
    intro h
02Separate the logical casesL8–8

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

  1. L8
    split
03Fix variables and assumptionsL9–10

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

  1. L9
    intro i
  2. L10
    intro hi
04Establish hvL11–14

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

  1. L11
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))Definitions: FpAddBetaAt
  2. L12
    specialize h (i)
  3. L13
    apply h
  4. L14
    exact hi
05Separate the logical casesL15–21

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

  1. L15
    cases hv
  2. L16
    cases hv_witness
  3. L17
    cases hv_witness_witness
  4. L18
    cases hv_witness_witness_right
  5. L19
    cases hv_witness_witness_right_right
  6. L20
    cases hv_witness_witness_right_right_right
  7. L21
    cases hv_witness_witness_right_right_right_right
06Construct an explicit witnessL22–22

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

  1. L22
    exists x
07Separate the logical casesL23–23

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

  1. L23
    split
08Use earlier factsL24–25

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

  1. L24
    exact hv_witness_witness_left
  2. L25
    exact hv_witness_witness_right_right_left
09Fix variables and assumptionsL26–27

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

  1. L26
    intro i
  2. L27
    intro hi
10Establish hvL28–31

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

  1. L28
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))Definitions: FpAddBetaAt
  2. L29
    specialize h (i)
  3. L30
    apply h
  4. L31
    exact hi
11Separate the logical casesL32–38

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

  1. L32
    cases hv
  2. L33
    cases hv_witness
  3. L34
    cases hv_witness_witness
  4. L35
    cases hv_witness_witness_right
  5. L36
    cases hv_witness_witness_right_right
  6. L37
    cases hv_witness_witness_right_right_right
  7. L38
    cases hv_witness_witness_right_right_right_right
12Construct an explicit witnessL39–39

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

  1. L39
    exists x1
13Separate the logical casesL40–40

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

  1. L40
    split
14Use earlier factsL41–42

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

  1. L41
    exact hv_witness_witness_right_left
  2. L42
    exact hv_witness_witness_right_right_right_left

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro l
  7. 0007intro h
  8. 0008split
  9. 0009intro i
  10. 0010intro hi
  11. 0011have hv : exists a r. (((((exists ff_h_pfp_negate_bound_chosen0. ff_h_pfp_negate_bound_chosen0 + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_negate_bound_chosen0. ab = ff_q_pfp_negate_bound_chosen0 * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_negate_bound_chosen1. ff_h_pfp_negate_bound_chosen1 + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_negate_bound_chosen1. rb = ff_q_pfp_negate_bound_chosen1 * S ((S (i)) * rc) + (r))) /\ ((((exists pfa_gap_negate_bound_chosenoperationadditionleft. pfa_gap_negate_bound_chosenoperationadditionleft + S (a) = (p)) /\ (((exists pfa_gap_negate_bound_chosenoperationadditionright. pfa_gap_negate_bound_chosenoperationadditionright + S (r) = (p)) /\ ((((exists pfa_gap_negate_bound_chosenoperationadditionresultbound. pfa_gap_negate_bound_chosenoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_bound_chosenoperationadditionresultcongruence pfa_offset_right_negate_bound_chosenoperationadditionresultcongruence. ((a) + (r)) + (p) * pfa_offset_left_negate_bound_chosenoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_bound_chosenoperationadditionresultcongruence))))))))))))))
  12. 0012specialize h (i)
  13. 0013apply h
  14. 0014exact hi
  15. 0015cases hv
  16. 0016cases hv_witness
  17. 0017cases hv_witness_witness
  18. 0018cases hv_witness_witness_right
  19. 0019cases hv_witness_witness_right_right
  20. 0020cases hv_witness_witness_right_right_right
  21. 0021cases hv_witness_witness_right_right_right_right
  22. 0022exists x
  23. 0023split
  24. 0024exact hv_witness_witness_left
  25. 0025exact hv_witness_witness_right_right_left
  26. 0026intro i
  27. 0027intro hi
  28. 0028have hv : exists a r. (((((exists ff_h_pfp_negate_bound_chosen0. ff_h_pfp_negate_bound_chosen0 + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_negate_bound_chosen0. ab = ff_q_pfp_negate_bound_chosen0 * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_negate_bound_chosen1. ff_h_pfp_negate_bound_chosen1 + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_negate_bound_chosen1. rb = ff_q_pfp_negate_bound_chosen1 * S ((S (i)) * rc) + (r))) /\ ((((exists pfa_gap_negate_bound_chosenoperationadditionleft. pfa_gap_negate_bound_chosenoperationadditionleft + S (a) = (p)) /\ (((exists pfa_gap_negate_bound_chosenoperationadditionright. pfa_gap_negate_bound_chosenoperationadditionright + S (r) = (p)) /\ ((((exists pfa_gap_negate_bound_chosenoperationadditionresultbound. pfa_gap_negate_bound_chosenoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_bound_chosenoperationadditionresultcongruence pfa_offset_right_negate_bound_chosenoperationadditionresultcongruence. ((a) + (r)) + (p) * pfa_offset_left_negate_bound_chosenoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_bound_chosenoperationadditionresultcongruence))))))))))))))
  29. 0029specialize h (i)
  30. 0030apply h
  31. 0031exact hi
  32. 0032cases hv
  33. 0033cases hv_witness
  34. 0034cases hv_witness_witness
  35. 0035cases hv_witness_witness_right
  36. 0036cases hv_witness_witness_right_right
  37. 0037cases hv_witness_witness_right_right_right
  38. 0038cases hv_witness_witness_right_right_right_right
  39. 0039exists x1
  40. 0040split
  41. 0041exact hv_witness_witness_right_left
  42. 0042exact hv_witness_witness_right_right_right_left