PG0018

prime_field_polynomial_scale_zero_value

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

Every actual scalar-zero output is an actually all-zero prefix, without primality and without dropping the scalar bound on an empty input.

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 bb bc sb sc M. (((exists pfa_gap_scalar_zero_actualscalar. pfa_gap_scalar_zero_actualscalar + S (0) = (p)) /\ ((forall pfp_index_scalar_zero_actual. (exists pfa_gap_scalar_zero_actualindex. pfa_gap_scalar_zero_actualindex + S (pfp_index_scalar_zero_actual) = (M)) -> exists pfp_source_scalar_zero_actual pfp_value_scalar_zero_actual. ((((exists ff_h_pfp_scalar_zero_actualsource. ff_h_pfp_scalar_zero_actualsource + S (pfp_source_scalar_zero_actual) = S ((S (pfp_index_scalar_zero_actual)) * bc)) /\ exists ff_q_pfp_scalar_zero_actualsource. bb = ff_q_pfp_scalar_zero_actualsource * S ((S (pfp_index_scalar_zero_actual)) * bc) + (pfp_source_scalar_zero_actual))) /\ (((((exists ff_h_pfp_scalar_zero_actualtarget. ff_h_pfp_scalar_zero_actualtarget + S (pfp_value_scalar_zero_actual) = S ((S (pfp_index_scalar_zero_actual)) * sc)) /\ exists ff_q_pfp_scalar_zero_actualtarget. sb = ff_q_pfp_scalar_zero_actualtarget * S ((S (pfp_index_scalar_zero_actual)) * sc) + (pfp_value_scalar_zero_actual))) /\ ((((exists pfa_gap_scalar_zero_actualoperationleft. pfa_gap_scalar_zero_actualoperationleft + S (0) = (p)) /\ (((exists pfa_gap_scalar_zero_actualoperationright. pfa_gap_scalar_zero_actualoperationright + S (pfp_source_scalar_zero_actual) = (p)) /\ ((((exists pfa_gap_scalar_zero_actualoperationresultbound. pfa_gap_scalar_zero_actualoperationresultbound + S (pfp_value_scalar_zero_actual) = (p)) /\ ((exists pfa_offset_left_scalar_zero_actualoperationresultcongruence pfa_offset_right_scalar_zero_actualoperationresultcongruence. ((0) * (pfp_source_scalar_zero_actual)) + (p) * pfa_offset_left_scalar_zero_actualoperationresultcongruence = (pfp_value_scalar_zero_actual) + (p) * pfa_offset_right_scalar_zero_actualoperationresultcongruence))))))))))))))))) -> (forall pfp_repeat_index_scalar_zero_result. (exists pfa_gap_scalar_zero_resultindex. pfa_gap_scalar_zero_resultindex + S (pfp_repeat_index_scalar_zero_result) = (M)) -> (((exists ff_h_pfp_scalar_zero_resultentry. ff_h_pfp_scalar_zero_resultentry + S (0) = S ((S (pfp_repeat_index_scalar_zero_result)) * sc)) /\ exists ff_q_pfp_scalar_zero_resultentry. sb = ff_q_pfp_scalar_zero_resultentry * S ((S (pfp_repeat_index_scalar_zero_result)) * sc) + (0))))

Constructive proof overview

Generated structural guide

Every actual scalar-zero output is an actually all-zero prefix, without primality and without dropping the scalar bound on an empty input.

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

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

Proof neighborhood

Direct dependencies

mul_zero_left Alpha theorem; checked-use authorized prime_field_residue_bounded_value Alpha theorem; checked-use authorized

Direct dependents

PG0019 prime_field_polynomial_convolution_right_scale_zero

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

35 script commands · 9 reading checkpoints · 4 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 bb
  3. L3
    intro bc
  4. L4
    intro sb
  5. L5
    intro sc
  6. L6
    intro M
  7. L7
    intro hs
02Separate the logical casesL8–8

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

  1. L8
    cases hs
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 hs right.

  1. L11
    have hv : ∃ a. ∃ r. BetaAt(bb,bc,i,a) ∧ (BetaAt(sb,sc,i,r) ∧ FpMul(p,0,a,r))Definitions: FpMulBetaAt
  2. L12
    specialize hs_right (i)
  3. L13
    apply hs_right
  4. L14
    exact hi
05Separate the logical casesL15–18

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
06Establish hmL19–20

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

  1. L19
    have hm : FpMul(p,0,x,x1)Definitions: FpMul
  2. L20
    exact hv_witness_witness_right_right
07Separate the logical casesL21–22

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

  1. L21
    cases hm
  2. L22
    cases hm_right
08Establish hzeroL23–25

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

  1. L23
    have hzero : 0*x=0
  2. L24
    apply mul_zero_left
  3. L25
    rewrite hzero at hm_right_right
09Establish heqL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field residue bounded value.

  1. L26
    have heq : x1=0
  2. L27
    specialize prime_field_residue_bounded_value (p)
  3. L28
    specialize prime_field_residue_bounded_value (0)
  4. L29
    specialize prime_field_residue_bounded_value (x1)
  5. L30
    apply prime_field_residue_bounded_value
  6. L31
    exact hs_left
  7. L32
    exact hm_right_right
  8. L33
    rewrite heq at hv_witness_witness_right_left
  9. L34
    rewrite heq at hv_witness_witness_right_left
  10. L35
    exact hv_witness_witness_right_left

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro p
  2. 0002intro bb
  3. 0003intro bc
  4. 0004intro sb
  5. 0005intro sc
  6. 0006intro M
  7. 0007intro hs
  8. 0008cases hs
  9. 0009intro i
  10. 0010intro hi
  11. 0011have hv : exists a r. ((((exists ff_h_pfp_scalar_zero_chosen_source. ff_h_pfp_scalar_zero_chosen_source + S (a) = S ((S (i)) * bc)) /\ exists ff_q_pfp_scalar_zero_chosen_source. bb = ff_q_pfp_scalar_zero_chosen_source * S ((S (i)) * bc) + (a))) /\ (((((exists ff_h_pfp_scalar_zero_chosen_target. ff_h_pfp_scalar_zero_chosen_target + S (r) = S ((S (i)) * sc)) /\ exists ff_q_pfp_scalar_zero_chosen_target. sb = ff_q_pfp_scalar_zero_chosen_target * S ((S (i)) * sc) + (r))) /\ ((((exists pfa_gap_scalar_zero_chosen_productleft. pfa_gap_scalar_zero_chosen_productleft + S (0) = (p)) /\ (((exists pfa_gap_scalar_zero_chosen_productright. pfa_gap_scalar_zero_chosen_productright + S (a) = (p)) /\ ((((exists pfa_gap_scalar_zero_chosen_productresultbound. pfa_gap_scalar_zero_chosen_productresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_scalar_zero_chosen_productresultcongruence pfa_offset_right_scalar_zero_chosen_productresultcongruence. ((0) * (a)) + (p) * pfa_offset_left_scalar_zero_chosen_productresultcongruence = (r) + (p) * pfa_offset_right_scalar_zero_chosen_productresultcongruence)))))))))))))
  12. 0012specialize hs_right (i)
  13. 0013apply hs_right
  14. 0014exact hi
  15. 0015cases hv
  16. 0016cases hv_witness
  17. 0017cases hv_witness_witness
  18. 0018cases hv_witness_witness_right
  19. 0019have hm : ((exists pfa_gap_scalar_zero_actual_productleft. pfa_gap_scalar_zero_actual_productleft + S (0) = (p)) /\ (((exists pfa_gap_scalar_zero_actual_productright. pfa_gap_scalar_zero_actual_productright + S (x) = (p)) /\ ((((exists pfa_gap_scalar_zero_actual_productresultbound. pfa_gap_scalar_zero_actual_productresultbound + S (x1) = (p)) /\ ((exists pfa_offset_left_scalar_zero_actual_productresultcongruence pfa_offset_right_scalar_zero_actual_productresultcongruence. ((0) * (x)) + (p) * pfa_offset_left_scalar_zero_actual_productresultcongruence = (x1) + (p) * pfa_offset_right_scalar_zero_actual_productresultcongruence))))))))
  20. 0020exact hv_witness_witness_right_right
  21. 0021cases hm
  22. 0022cases hm_right
  23. 0023have hzero : 0*x=0
  24. 0024apply mul_zero_left
  25. 0025rewrite hzero at hm_right_right
  26. 0026have heq : x1=0
  27. 0027specialize prime_field_residue_bounded_value (p)
  28. 0028specialize prime_field_residue_bounded_value (0)
  29. 0029specialize prime_field_residue_bounded_value (x1)
  30. 0030apply prime_field_residue_bounded_value
  31. 0031exact hs_left
  32. 0032exact hm_right_right
  33. 0033rewrite heq at hv_witness_witness_right_left
  34. 0034rewrite heq at hv_witness_witness_right_left
  35. 0035exact hv_witness_witness_right_left