PQ0018

prime_field_polynomial_subtract_equal_zero

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

Subtracting extensionally equal canonical prefixes gives an actual all-zero prefix even when their beta encodings differ.

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 bb bc rb rc l. (~((p) = 1) /\ forall pfa_factor_left_sub_equal_prime pfa_factor_right_sub_equal_prime. (p) = pfa_factor_left_sub_equal_prime * pfa_factor_right_sub_equal_prime -> pfa_factor_left_sub_equal_prime = 1 \/ pfa_factor_right_sub_equal_prime = 1) -> (forall mdr_i_pfp_sub_equal_inputs mdr_a_pfp_sub_equal_inputs. (exists mdr_gap_pfp_sub_equal_inputsb. mdr_gap_pfp_sub_equal_inputsb + S (mdr_i_pfp_sub_equal_inputs) = (l)) -> (((exists ff_h_mdr_pfp_sub_equal_inputso. ff_h_mdr_pfp_sub_equal_inputso + S (mdr_a_pfp_sub_equal_inputs) = S ((S (mdr_i_pfp_sub_equal_inputs)) * ac)) /\ exists ff_q_mdr_pfp_sub_equal_inputso. ab = ff_q_mdr_pfp_sub_equal_inputso * S ((S (mdr_i_pfp_sub_equal_inputs)) * ac) + (mdr_a_pfp_sub_equal_inputs))) -> (((exists ff_h_mdr_pfp_sub_equal_inputsn. ff_h_mdr_pfp_sub_equal_inputsn + S (mdr_a_pfp_sub_equal_inputs) = S ((S (mdr_i_pfp_sub_equal_inputs)) * bc)) /\ exists ff_q_mdr_pfp_sub_equal_inputsn. bb = ff_q_mdr_pfp_sub_equal_inputsn * S ((S (mdr_i_pfp_sub_equal_inputs)) * bc) + (mdr_a_pfp_sub_equal_inputs)))) -> (forall pfs_index_sub_equal_graph. (exists pfa_gap_sub_equal_graphindex. pfa_gap_sub_equal_graphindex + S (pfs_index_sub_equal_graph) = (l)) -> exists pfs_left_sub_equal_graph pfs_right_sub_equal_graph pfs_result_sub_equal_graph. ((((exists ff_h_pfp_sub_equal_graphleft. ff_h_pfp_sub_equal_graphleft + S (pfs_left_sub_equal_graph) = S ((S (pfs_index_sub_equal_graph)) * ac)) /\ exists ff_q_pfp_sub_equal_graphleft. ab = ff_q_pfp_sub_equal_graphleft * S ((S (pfs_index_sub_equal_graph)) * ac) + (pfs_left_sub_equal_graph))) /\ (((((exists ff_h_pfp_sub_equal_graphright. ff_h_pfp_sub_equal_graphright + S (pfs_right_sub_equal_graph) = S ((S (pfs_index_sub_equal_graph)) * bc)) /\ exists ff_q_pfp_sub_equal_graphright. bb = ff_q_pfp_sub_equal_graphright * S ((S (pfs_index_sub_equal_graph)) * bc) + (pfs_right_sub_equal_graph))) /\ (((((exists ff_h_pfp_sub_equal_graphresult. ff_h_pfp_sub_equal_graphresult + S (pfs_result_sub_equal_graph) = S ((S (pfs_index_sub_equal_graph)) * rc)) /\ exists ff_q_pfp_sub_equal_graphresult. rb = ff_q_pfp_sub_equal_graphresult * S ((S (pfs_index_sub_equal_graph)) * rc) + (pfs_result_sub_equal_graph))) /\ ((((exists pfa_gap_sub_equal_graphoperationleft. pfa_gap_sub_equal_graphoperationleft + S (pfs_right_sub_equal_graph) = (p)) /\ (((exists pfa_gap_sub_equal_graphoperationright. pfa_gap_sub_equal_graphoperationright + S (pfs_result_sub_equal_graph) = (p)) /\ ((((exists pfa_gap_sub_equal_graphoperationresultbound. pfa_gap_sub_equal_graphoperationresultbound + S (pfs_left_sub_equal_graph) = (p)) /\ ((exists pfa_offset_left_sub_equal_graphoperationresultcongruence pfa_offset_right_sub_equal_graphoperationresultcongruence. ((pfs_right_sub_equal_graph) + (pfs_result_sub_equal_graph)) + (p) * pfa_offset_left_sub_equal_graphoperationresultcongruence = (pfs_left_sub_equal_graph) + (p) * pfa_offset_right_sub_equal_graphoperationresultcongruence)))))))))))))))) -> (forall pfp_repeat_index_sub_equal_result. (exists pfa_gap_sub_equal_resultindex. pfa_gap_sub_equal_resultindex + S (pfp_repeat_index_sub_equal_result) = (l)) -> (((exists ff_h_pfp_sub_equal_resultentry. ff_h_pfp_sub_equal_resultentry + S (0) = S ((S (pfp_repeat_index_sub_equal_result)) * rc)) /\ exists ff_q_pfp_sub_equal_resultentry. rb = ff_q_pfp_sub_equal_resultentry * S ((S (pfp_repeat_index_sub_equal_result)) * rc) + (0))))

Constructive proof overview

Generated structural guide

Subtracting extensionally equal canonical prefixes gives an actual all-zero prefix even when their beta encodings differ.

The unchanged tactic script uses 2 declared prerequisites and contains 51 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized PQ0017 prime_field_polynomial_subtract_equal_entry_zero

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

51 script commands · 11 reading checkpoints · 3 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.

Named ingredients (1)
prime field polynomial subtract equal entry zero
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 bb
  5. L5
    intro bc
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro l
  9. L9
    intro hp
  10. L10
    intro he
02Fix variables and assumptionsL11–13

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

  1. L11
    intro h
  2. L12
    intro i
  3. L13
    intro hi
03Establish haL14–18

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

  1. L14
    have ha : exists a. (((exists ff_h_pfp_sub_all_zero_a. ff_h_pfp_sub_all_zero_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_sub_all_zero_a. ab = ff_q_pfp_sub_all_zero_a * S ((S (i)) * ac) + (a)))
  2. L15
    specialize beta_at_exists (ab)
  3. L16
    specialize beta_at_exists (ac)
  4. L17
    specialize beta_at_exists (i)
  5. L18
    apply beta_at_exists
04Separate the logical casesL19–19

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

  1. L19
    cases ha
05Establish hrL20–24

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

  1. L20
    have hr : exists r. (((exists ff_h_pfp_sub_all_zero_r. ff_h_pfp_sub_all_zero_r + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_sub_all_zero_r. rb = ff_q_pfp_sub_all_zero_r * S ((S (i)) * rc) + (r)))
  2. L21
    specialize beta_at_exists (rb)
  3. L22
    specialize beta_at_exists (rc)
  4. L23
    specialize beta_at_exists (i)
  5. L24
    apply beta_at_exists
06Separate the logical casesL25–25

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

  1. L25
    cases hr
07Establish hzL26–35

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hz : x1=0
  2. L27
    specialize prime_field_polynomial_subtract_equal_entry_zero (p)
  3. L28
    specialize prime_field_polynomial_subtract_equal_entry_zero (ab)
  4. L29
    specialize prime_field_polynomial_subtract_equal_entry_zero (ac)
  5. L30
    specialize prime_field_polynomial_subtract_equal_entry_zero (bb)
  6. L31
    specialize prime_field_polynomial_subtract_equal_entry_zero (bc)
  7. L32
    specialize prime_field_polynomial_subtract_equal_entry_zero (rb)
  8. L33
    specialize prime_field_polynomial_subtract_equal_entry_zero (rc)
  9. L34
    specialize prime_field_polynomial_subtract_equal_entry_zero (l)
  10. L35
    specialize prime_field_polynomial_subtract_equal_entry_zero (i)
08Use earlier factsL36–45

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

  1. L36
    specialize prime_field_polynomial_subtract_equal_entry_zero (x)
  2. L37
    specialize prime_field_polynomial_subtract_equal_entry_zero (x1)
  3. L38
    apply prime_field_polynomial_subtract_equal_entry_zero
  4. L39
    exact hp
  5. L40
    exact h
  6. L41
    exact hi
  7. L42
    exact ha_witness
  8. L43
    specialize he (i)
  9. L44
    specialize he (x)
  10. L45
    apply he
09Use earlier factsL46–48

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

  1. L46
    exact hi
  2. L47
    exact ha_witness
  3. L48
    exact hr_witness
10Calculate and transport equalitiesL49–50

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

  1. L49
    rewrite hz at hr_witness
  2. L50
    rewrite hz at hr_witness
11Use earlier factsL51–51

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

  1. L51
    exact hr_witness

Library-wide reading audit

Original exact command ledger · 51 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro l
  9. 0009intro hp
  10. 0010intro he
  11. 0011intro h
  12. 0012intro i
  13. 0013intro hi
  14. 0014have ha : exists a. (((exists ff_h_pfp_sub_all_zero_a. ff_h_pfp_sub_all_zero_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_sub_all_zero_a. ab = ff_q_pfp_sub_all_zero_a * S ((S (i)) * ac) + (a)))
  15. 0015specialize beta_at_exists (ab)
  16. 0016specialize beta_at_exists (ac)
  17. 0017specialize beta_at_exists (i)
  18. 0018apply beta_at_exists
  19. 0019cases ha
  20. 0020have hr : exists r. (((exists ff_h_pfp_sub_all_zero_r. ff_h_pfp_sub_all_zero_r + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_sub_all_zero_r. rb = ff_q_pfp_sub_all_zero_r * S ((S (i)) * rc) + (r)))
  21. 0021specialize beta_at_exists (rb)
  22. 0022specialize beta_at_exists (rc)
  23. 0023specialize beta_at_exists (i)
  24. 0024apply beta_at_exists
  25. 0025cases hr
  26. 0026have hz : x1=0
  27. 0027specialize prime_field_polynomial_subtract_equal_entry_zero (p)
  28. 0028specialize prime_field_polynomial_subtract_equal_entry_zero (ab)
  29. 0029specialize prime_field_polynomial_subtract_equal_entry_zero (ac)
  30. 0030specialize prime_field_polynomial_subtract_equal_entry_zero (bb)
  31. 0031specialize prime_field_polynomial_subtract_equal_entry_zero (bc)
  32. 0032specialize prime_field_polynomial_subtract_equal_entry_zero (rb)
  33. 0033specialize prime_field_polynomial_subtract_equal_entry_zero (rc)
  34. 0034specialize prime_field_polynomial_subtract_equal_entry_zero (l)
  35. 0035specialize prime_field_polynomial_subtract_equal_entry_zero (i)
  36. 0036specialize prime_field_polynomial_subtract_equal_entry_zero (x)
  37. 0037specialize prime_field_polynomial_subtract_equal_entry_zero (x1)
  38. 0038apply prime_field_polynomial_subtract_equal_entry_zero
  39. 0039exact hp
  40. 0040exact h
  41. 0041exact hi
  42. 0042exact ha_witness
  43. 0043specialize he (i)
  44. 0044specialize he (x)
  45. 0045apply he
  46. 0046exact hi
  47. 0047exact ha_witness
  48. 0048exact hr_witness
  49. 0049rewrite hz at hr_witness
  50. 0050rewrite hz at hr_witness
  51. 0051exact hr_witness