PP001B

prime_field_polynomial_scale_zero

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ zb. ∀ zc. ∀ l. Prime(p) → BetaPrefixInto(b,c,l,p) → Repeat(zb,zc,0,l) → FpPolyScale(p,0,b,c,zb,zc,l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaPrefixInto(b,c,l,B) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 1Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

prime_field_zero_below_prime · checked external prerequisiteprime_field_multiply_zero_left · checked external prerequisite
Original expanded first-order 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)))))))))))))))))

Complete tactic proof in conservative notation

All 34 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ a. BetaAt(b,c,i,a) ∧ Lt(a,p)Definitions: BetaAt(b,c,i,a)Lt(a,p)Original native command in the exact edition
  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 defined 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 : ∃ a. BetaAt(b,c,i,a) ∧ Lt(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