PQ000B

prime_field_polynomial_negate_add_zero

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

Adding actual opposite coefficient values produces any genuine zero-prefix encoding.

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 zb zc l. (forall pfs_index_neg_add_graph. (exists pfa_gap_neg_add_graphindex. pfa_gap_neg_add_graphindex + S (pfs_index_neg_add_graph) = (l)) -> exists pfs_source_neg_add_graph pfs_result_neg_add_graph. ((((exists ff_h_pfp_neg_add_graphsource. ff_h_pfp_neg_add_graphsource + S (pfs_source_neg_add_graph) = S ((S (pfs_index_neg_add_graph)) * ac)) /\ exists ff_q_pfp_neg_add_graphsource. ab = ff_q_pfp_neg_add_graphsource * S ((S (pfs_index_neg_add_graph)) * ac) + (pfs_source_neg_add_graph))) /\ (((((exists ff_h_pfp_neg_add_graphresult. ff_h_pfp_neg_add_graphresult + S (pfs_result_neg_add_graph) = S ((S (pfs_index_neg_add_graph)) * rc)) /\ exists ff_q_pfp_neg_add_graphresult. rb = ff_q_pfp_neg_add_graphresult * S ((S (pfs_index_neg_add_graph)) * rc) + (pfs_result_neg_add_graph))) /\ ((((exists pfa_gap_neg_add_graphoperationadditionleft. pfa_gap_neg_add_graphoperationadditionleft + S (pfs_source_neg_add_graph) = (p)) /\ (((exists pfa_gap_neg_add_graphoperationadditionright. pfa_gap_neg_add_graphoperationadditionright + S (pfs_result_neg_add_graph) = (p)) /\ ((((exists pfa_gap_neg_add_graphoperationadditionresultbound. pfa_gap_neg_add_graphoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_neg_add_graphoperationadditionresultcongruence pfa_offset_right_neg_add_graphoperationadditionresultcongruence. ((pfs_source_neg_add_graph) + (pfs_result_neg_add_graph)) + (p) * pfa_offset_left_neg_add_graphoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_neg_add_graphoperationadditionresultcongruence)))))))))))))) -> (forall pfp_repeat_index_neg_add_zero. (exists pfa_gap_neg_add_zeroindex. pfa_gap_neg_add_zeroindex + S (pfp_repeat_index_neg_add_zero) = (l)) -> (((exists ff_h_pfp_neg_add_zeroentry. ff_h_pfp_neg_add_zeroentry + S (0) = S ((S (pfp_repeat_index_neg_add_zero)) * zc)) /\ exists ff_q_pfp_neg_add_zeroentry. zb = ff_q_pfp_neg_add_zeroentry * S ((S (pfp_repeat_index_neg_add_zero)) * zc) + (0)))) -> (forall pfp_index_neg_add_result. (exists pfa_gap_neg_add_resultindex. pfa_gap_neg_add_resultindex + S (pfp_index_neg_add_result) = (l)) -> exists pfp_left_neg_add_result pfp_right_neg_add_result pfp_value_neg_add_result. ((((exists ff_h_pfp_neg_add_resultleft. ff_h_pfp_neg_add_resultleft + S (pfp_left_neg_add_result) = S ((S (pfp_index_neg_add_result)) * ac)) /\ exists ff_q_pfp_neg_add_resultleft. ab = ff_q_pfp_neg_add_resultleft * S ((S (pfp_index_neg_add_result)) * ac) + (pfp_left_neg_add_result))) /\ (((((exists ff_h_pfp_neg_add_resultright. ff_h_pfp_neg_add_resultright + S (pfp_right_neg_add_result) = S ((S (pfp_index_neg_add_result)) * rc)) /\ exists ff_q_pfp_neg_add_resultright. rb = ff_q_pfp_neg_add_resultright * S ((S (pfp_index_neg_add_result)) * rc) + (pfp_right_neg_add_result))) /\ (((((exists ff_h_pfp_neg_add_resulttarget. ff_h_pfp_neg_add_resulttarget + S (pfp_value_neg_add_result) = S ((S (pfp_index_neg_add_result)) * zc)) /\ exists ff_q_pfp_neg_add_resulttarget. zb = ff_q_pfp_neg_add_resulttarget * S ((S (pfp_index_neg_add_result)) * zc) + (pfp_value_neg_add_result))) /\ ((((exists pfa_gap_neg_add_resultoperationleft. pfa_gap_neg_add_resultoperationleft + S (pfp_left_neg_add_result) = (p)) /\ (((exists pfa_gap_neg_add_resultoperationright. pfa_gap_neg_add_resultoperationright + S (pfp_right_neg_add_result) = (p)) /\ ((((exists pfa_gap_neg_add_resultoperationresultbound. pfa_gap_neg_add_resultoperationresultbound + S (pfp_value_neg_add_result) = (p)) /\ ((exists pfa_offset_left_neg_add_resultoperationresultcongruence pfa_offset_right_neg_add_resultoperationresultcongruence. ((pfp_left_neg_add_result) + (pfp_right_neg_add_result)) + (p) * pfa_offset_left_neg_add_resultoperationresultcongruence = (pfp_value_neg_add_result) + (p) * pfa_offset_right_neg_add_resultoperationresultcongruence))))))))))))))))

Constructive proof overview

Generated structural guide

Adding actual opposite coefficient values produces any genuine zero-prefix encoding.

The unchanged tactic script uses 0 declared prerequisites and contains 32 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

PQ0016 prime_field_polynomial_subtract_zero_left

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

32 script commands · 11 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–10

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 zb
  7. L7
    intro zc
  8. L8
    intro l
  9. L9
    intro h
  10. L10
    intro hz
02Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
03Establish hvL13–16

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

  1. L13
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))Definitions: FpAddBetaAt
  2. L14
    specialize h (i)
  3. L15
    apply h
  4. L16
    exact hi
04Separate the logical casesL17–20

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

  1. L17
    cases hv
  2. L18
    cases hv_witness
  3. L19
    cases hv_witness_witness
  4. L20
    cases hv_witness_witness_right
05Construct an explicit witnessL21–23

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

  1. L21
    exists x
  2. L22
    exists x1
  3. L23
    exists 0
06Separate the logical casesL24–24

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

  1. L24
    split
07Use earlier factsL25–25

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

  1. L25
    exact hv_witness_witness_left
08Separate the logical casesL26–26

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

  1. L26
    split
09Use earlier factsL27–27

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

  1. L27
    exact hv_witness_witness_right_left
10Separate the logical casesL28–28

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

  1. L28
    split
11Use earlier factsL29–32

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

  1. L29
    specialize hz (i)
  2. L30
    apply hz
  3. L31
    exact hi
  4. L32
    exact hv_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro zb
  7. 0007intro zc
  8. 0008intro l
  9. 0009intro h
  10. 0010intro hz
  11. 0011intro i
  12. 0012intro hi
  13. 0013have hv : exists a r. (((((exists ff_h_pfp_neg_law_source. ff_h_pfp_neg_law_source + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_neg_law_source. ab = ff_q_pfp_neg_law_source * S ((S (i)) * ac) + (a))) /\ (((((exists ff_h_pfp_neg_law_result. ff_h_pfp_neg_law_result + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_neg_law_result. rb = ff_q_pfp_neg_law_result * S ((S (i)) * rc) + (r))) /\ ((((exists pfa_gap_neg_law_valueadditionleft. pfa_gap_neg_law_valueadditionleft + S (a) = (p)) /\ (((exists pfa_gap_neg_law_valueadditionright. pfa_gap_neg_law_valueadditionright + S (r) = (p)) /\ ((((exists pfa_gap_neg_law_valueadditionresultbound. pfa_gap_neg_law_valueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_neg_law_valueadditionresultcongruence pfa_offset_right_neg_law_valueadditionresultcongruence. ((a) + (r)) + (p) * pfa_offset_left_neg_law_valueadditionresultcongruence = (0) + (p) * pfa_offset_right_neg_law_valueadditionresultcongruence))))))))))))))
  14. 0014specialize h (i)
  15. 0015apply h
  16. 0016exact hi
  17. 0017cases hv
  18. 0018cases hv_witness
  19. 0019cases hv_witness_witness
  20. 0020cases hv_witness_witness_right
  21. 0021exists x
  22. 0022exists x1
  23. 0023exists 0
  24. 0024split
  25. 0025exact hv_witness_witness_left
  26. 0026split
  27. 0027exact hv_witness_witness_right_left
  28. 0028split
  29. 0029specialize hz (i)
  30. 0030apply hz
  31. 0031exact hi
  32. 0032exact hv_witness_witness_right_right