PG0018

prime_field_polynomial_scale_zero_value

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

Alpha v34 checked-use · first admitted v34 · 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.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ bb. ∀ bc. ∀ sb. ∀ sc. ∀ M. FpPolyScale(p,0,bb,bc,sb,sc,M) → Repeat(sb,sc,0,M)

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

Definition DAG

FpMul(p,a,b,c) · 2FpPolyScale(p,k,ab,ac,bb,bc,l) · 1BetaAt(b,c,i,x) · 2Repeat(b,c,a,l) · 1

Actual proof prerequisites

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

Complete tactic proof in conservative notation

All 35 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

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.

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–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: BetaAt(bb,bc,i,a)BetaAt(sb,sc,i,r)FpMul(p,0,a,r)Original native command in the exact edition
  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
  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 defined 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 : ∃ a. ∃ r. BetaAt(bb,bc,i,a) ∧ (BetaAt(sb,sc,i,r) ∧ FpMul(p,0,a,r))
  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 : FpMul(p,0,x,x1)
  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