PP001B

prime_field_polynomial_scale_zero

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

Scalar zero produces a genuinely encoded zero polynomial, not merely a zero output claim.

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 zb zc l. (~((p) = 1) /\ forall pfa_factor_left_scale_zero_prime pfa_factor_right_scale_zero_prime. (p) = pfa_factor_left_scale_zero_prime * pfa_factor_right_scale_zero_prime -> pfa_factor_left_scale_zero_prime = 1 \/ pfa_factor_right_scale_zero_prime = 1) -> (forall fom_index_pfp_scale_zero_coefficients. (exists fom_gap_pfp_scale_zero_coefficients_index_bound. fom_gap_pfp_scale_zero_coefficients_index_bound + S (fom_index_pfp_scale_zero_coefficients) = l) -> exists fom_value_pfp_scale_zero_coefficients. ((((exists fom_beta_height_pfp_scale_zero_coefficients_entry. fom_beta_height_pfp_scale_zero_coefficients_entry + S (fom_value_pfp_scale_zero_coefficients) = S ((S (fom_index_pfp_scale_zero_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_scale_zero_coefficients_entry. b = fom_beta_quotient_pfp_scale_zero_coefficients_entry * S ((S (fom_index_pfp_scale_zero_coefficients)) * c) + (fom_value_pfp_scale_zero_coefficients))) /\ (exists fom_gap_pfp_scale_zero_coefficients_value_bound. fom_gap_pfp_scale_zero_coefficients_value_bound + S (fom_value_pfp_scale_zero_coefficients) = p))) -> (forall pfp_repeat_index_scale_zero_table. (exists pfa_gap_scale_zero_tableindex. pfa_gap_scale_zero_tableindex + S (pfp_repeat_index_scale_zero_table) = (l)) -> (((exists ff_h_pfp_scale_zero_tableentry. ff_h_pfp_scale_zero_tableentry + S (0) = S ((S (pfp_repeat_index_scale_zero_table)) * zc)) /\ exists ff_q_pfp_scale_zero_tableentry. zb = ff_q_pfp_scale_zero_tableentry * S ((S (pfp_repeat_index_scale_zero_table)) * zc) + (0)))) -> (((exists pfa_gap_scale_zero_resultscalar. pfa_gap_scale_zero_resultscalar + S (0) = (p)) /\ ((forall pfp_index_scale_zero_result. (exists pfa_gap_scale_zero_resultindex. pfa_gap_scale_zero_resultindex + S (pfp_index_scale_zero_result) = (l)) -> exists pfp_source_scale_zero_result pfp_value_scale_zero_result. ((((exists ff_h_pfp_scale_zero_resultsource. ff_h_pfp_scale_zero_resultsource + S (pfp_source_scale_zero_result) = S ((S (pfp_index_scale_zero_result)) * c)) /\ exists ff_q_pfp_scale_zero_resultsource. b = ff_q_pfp_scale_zero_resultsource * S ((S (pfp_index_scale_zero_result)) * c) + (pfp_source_scale_zero_result))) /\ (((((exists ff_h_pfp_scale_zero_resulttarget. ff_h_pfp_scale_zero_resulttarget + S (pfp_value_scale_zero_result) = S ((S (pfp_index_scale_zero_result)) * zc)) /\ exists ff_q_pfp_scale_zero_resulttarget. zb = ff_q_pfp_scale_zero_resulttarget * S ((S (pfp_index_scale_zero_result)) * zc) + (pfp_value_scale_zero_result))) /\ ((((exists pfa_gap_scale_zero_resultoperationleft. pfa_gap_scale_zero_resultoperationleft + S (0) = (p)) /\ (((exists pfa_gap_scale_zero_resultoperationright. pfa_gap_scale_zero_resultoperationright + S (pfp_source_scale_zero_result) = (p)) /\ ((((exists pfa_gap_scale_zero_resultoperationresultbound. pfa_gap_scale_zero_resultoperationresultbound + S (pfp_value_scale_zero_result) = (p)) /\ ((exists pfa_offset_left_scale_zero_resultoperationresultcongruence pfa_offset_right_scale_zero_resultoperationresultcongruence. ((0) * (pfp_source_scale_zero_result)) + (p) * pfa_offset_left_scale_zero_resultoperationresultcongruence = (pfp_value_scale_zero_result) + (p) * pfa_offset_right_scale_zero_resultoperationresultcongruence)))))))))))))))))

Constructive proof overview

Generated structural guide

Scalar zero produces a genuinely encoded zero polynomial, not merely a zero output claim.

The unchanged tactic script uses 2 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

prime_field_zero_below_prime Alpha theorem; checked-use authorized prime_field_multiply_zero_left Alpha theorem; checked-use authorized

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

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

01Fix variables and assumptionsL1–9

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 zb
  5. L5
    intro zc
  6. L6
    intro l
  7. L7
    intro hp
  8. L8
    intro hc
  9. L9
    intro hz
02Separate the logical casesL10–10

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

  1. L10
    split
03Use earlier factsL11–13

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

  1. L11
    specialize prime_field_zero_below_prime (p)
  2. L12
    apply prime_field_zero_below_prime
  3. L13
    exact hp
04Fix variables and assumptionsL14–15

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

  1. L14
    intro i
  2. L15
    intro hi
05Establish haL16–19

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

  1. L16
    have ha : exists a. ((((exists ff_h_pfp_scale_zero_chosen. ff_h_pfp_scale_zero_chosen + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_scale_zero_chosen. b = ff_q_pfp_scale_zero_chosen * S ((S (i)) * c) + (a))) /\ ((exists pfa_gap_scale_zero_bound. pfa_gap_scale_zero_bound + S (a) = (p))))
  2. L17
    specialize hc (i)
  3. L18
    apply hc
  4. L19
    exact hi
06Separate the logical casesL20–21

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

  1. L20
    cases ha
  2. L21
    cases ha_witness
07Construct an explicit witnessL22–23

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

  1. L22
    exists x
  2. L23
    exists 0
08Separate the logical casesL24–24

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

  1. L24
    split
09Use earlier factsL25–25

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

  1. L25
    exact ha_witness_left
10Separate the logical casesL26–26

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

  1. L26
    split
11Use earlier factsL27–34

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

  1. L27
    specialize hz (i)
  2. L28
    apply hz
  3. L29
    exact hi
  4. L30
    specialize prime_field_multiply_zero_left (p)
  5. L31
    specialize prime_field_multiply_zero_left (x)
  6. L32
    apply prime_field_multiply_zero_left
  7. L33
    exact hp
  8. L34
    exact ha_witness_right

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro zb
  5. 0005intro zc
  6. 0006intro l
  7. 0007intro hp
  8. 0008intro hc
  9. 0009intro hz
  10. 0010split
  11. 0011specialize prime_field_zero_below_prime (p)
  12. 0012apply prime_field_zero_below_prime
  13. 0013exact hp
  14. 0014intro i
  15. 0015intro hi
  16. 0016have ha : exists a. ((((exists ff_h_pfp_scale_zero_chosen. ff_h_pfp_scale_zero_chosen + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_scale_zero_chosen. b = ff_q_pfp_scale_zero_chosen * S ((S (i)) * c) + (a))) /\ ((exists pfa_gap_scale_zero_bound. pfa_gap_scale_zero_bound + S (a) = (p))))
  17. 0017specialize hc (i)
  18. 0018apply hc
  19. 0019exact hi
  20. 0020cases ha
  21. 0021cases ha_witness
  22. 0022exists x
  23. 0023exists 0
  24. 0024split
  25. 0025exact ha_witness_left
  26. 0026split
  27. 0027specialize hz (i)
  28. 0028apply hz
  29. 0029exact hi
  30. 0030specialize prime_field_multiply_zero_left (p)
  31. 0031specialize prime_field_multiply_zero_left (x)
  32. 0032apply prime_field_multiply_zero_left
  33. 0033exact hp
  34. 0034exact ha_witness_right