PQ0039

prime_field_polynomial_monic_normalization_leading

The actual scaled leading coefficient equals one by the recorded inverse, not by a monic output premise.

Alpha v34 checked-use · first admitted v32 · 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 coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ L. FpMonicNormalization(p,k,ab,ac,bb,bc,L) → BetaAt(bb,bc,0,1)

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

Definition DAG

FpMul(p,a,b,c) · 2FpMonicNormalization(p,k,ab,ac,bb,bc,L) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

one_le_of_ne_zero · checked external prerequisitebeta_at_exists · checked external prerequisiteprime_field_polynomial_monic_normalization_entryprime_field_multiply_commutative · checked external prerequisiteprime_field_multiply_functional · checked external prerequisite
Original expanded first-order statement 
forall p k ab ac bb bc L. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_leading_source. ((((exists ff_h_pfp_normalization_leading_sourcesource. ff_h_pfp_normalization_leading_sourcesource + S (pfm_leading_normalization_leading_source) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_leading_sourcesource. ab = ff_q_pfp_normalization_leading_sourcesource * S ((S (0)) * ac) + (pfm_leading_normalization_leading_source))) /\ ((((~((pfm_leading_normalization_leading_source) = 0)) /\ ((((exists pfa_gap_normalization_leading_sourceinversemultiplicationleft. pfa_gap_normalization_leading_sourceinversemultiplicationleft + S (pfm_leading_normalization_leading_source) = (p)) /\ (((exists pfa_gap_normalization_leading_sourceinversemultiplicationright. pfa_gap_normalization_leading_sourceinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_leading_sourceinversemultiplicationresultbound. pfa_gap_normalization_leading_sourceinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_leading_sourceinversemultiplicationresultcongruence pfa_offset_right_normalization_leading_sourceinversemultiplicationresultcongruence. ((pfm_leading_normalization_leading_source) * (k)) + (p) * pfa_offset_left_normalization_leading_sourceinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_leading_sourceinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_leading_sourcescalescalar. pfa_gap_normalization_leading_sourcescalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_leading_sourcescale. (exists pfa_gap_normalization_leading_sourcescaleindex. pfa_gap_normalization_leading_sourcescaleindex + S (pfp_index_normalization_leading_sourcescale) = (L)) -> exists pfp_source_normalization_leading_sourcescale pfp_value_normalization_leading_sourcescale. ((((exists ff_h_pfp_normalization_leading_sourcescalesource. ff_h_pfp_normalization_leading_sourcescalesource + S (pfp_source_normalization_leading_sourcescale) = S ((S (pfp_index_normalization_leading_sourcescale)) * ac)) /\ exists ff_q_pfp_normalization_leading_sourcescalesource. ab = ff_q_pfp_normalization_leading_sourcescalesource * S ((S (pfp_index_normalization_leading_sourcescale)) * ac) + (pfp_source_normalization_leading_sourcescale))) /\ (((((exists ff_h_pfp_normalization_leading_sourcescaletarget. ff_h_pfp_normalization_leading_sourcescaletarget + S (pfp_value_normalization_leading_sourcescale) = S ((S (pfp_index_normalization_leading_sourcescale)) * bc)) /\ exists ff_q_pfp_normalization_leading_sourcescaletarget. bb = ff_q_pfp_normalization_leading_sourcescaletarget * S ((S (pfp_index_normalization_leading_sourcescale)) * bc) + (pfp_value_normalization_leading_sourcescale))) /\ ((((exists pfa_gap_normalization_leading_sourcescaleoperationleft. pfa_gap_normalization_leading_sourcescaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_leading_sourcescaleoperationright. pfa_gap_normalization_leading_sourcescaleoperationright + S (pfp_source_normalization_leading_sourcescale) = (p)) /\ ((((exists pfa_gap_normalization_leading_sourcescaleoperationresultbound. pfa_gap_normalization_leading_sourcescaleoperationresultbound + S (pfp_value_normalization_leading_sourcescale) = (p)) /\ ((exists pfa_offset_left_normalization_leading_sourcescaleoperationresultcongruence pfa_offset_right_normalization_leading_sourcescaleoperationresultcongruence. ((k) * (pfp_source_normalization_leading_sourcescale)) + (p) * pfa_offset_left_normalization_leading_sourcescaleoperationresultcongruence = (pfp_value_normalization_leading_sourcescale) + (p) * pfa_offset_right_normalization_leading_sourcescaleoperationresultcongruence)))))))))))))))))))))) -> (((exists ff_h_pfp_normalization_leading_result. ff_h_pfp_normalization_leading_result + S (1) = S ((S (0)) * bc)) /\ exists ff_q_pfp_normalization_leading_result. bb = ff_q_pfp_normalization_leading_result * S ((S (0)) * bc) + (1)))

Complete tactic proof in conservative notation

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

60 script commands · 12 reading checkpoints · 6 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.

Named ingredients (1)
prime field polynomial monic normalization entry
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro L
  8. L8
    intro h
02Establish hcL9–10

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

  1. L9
    have hc : FpMonicNormalization(p,k,ab,ac,bb,bc,L)Definitions: FpMonicNormalization(p,k,ab,ac,bb,bc,L)Original native command in the exact edition
  2. L10
    exact h
03Separate the logical casesL11–15

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

  1. L11
    cases hc
  2. L12
    cases hc_right
  3. L13
    cases hc_right_left
  4. L14
    cases hc_right_left_witness
  5. L15
    cases hc_right_left_witness_right
04Establish hzeroL16–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L16
  2. L17
    specialize one_le_of_ne_zero (L)
  3. L18
    apply one_le_of_ne_zero
  4. L19
    exact hc_left
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 : ∃ r. BetaAt(bb,bc,0,r)Definitions: BetaAt(bb,bc,0,r)Original native command in the exact edition
  2. L21
    specialize beta_at_exists (bb)
  3. L22
    specialize beta_at_exists (bc)
  4. L23
    specialize beta_at_exists (0)
  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 hmL26–35

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

  1. L26
  2. L27
    specialize prime_field_polynomial_monic_normalization_entry (p)
  3. L28
    specialize prime_field_polynomial_monic_normalization_entry (k)
  4. L29
    specialize prime_field_polynomial_monic_normalization_entry (ab)
  5. L30
    specialize prime_field_polynomial_monic_normalization_entry (ac)
  6. L31
    specialize prime_field_polynomial_monic_normalization_entry (bb)
  7. L32
    specialize prime_field_polynomial_monic_normalization_entry (bc)
  8. L33
    specialize prime_field_polynomial_monic_normalization_entry (L)
  9. L34
    specialize prime_field_polynomial_monic_normalization_entry (0)
  10. L35
    specialize prime_field_polynomial_monic_normalization_entry (x)
08Use earlier factsL36–41

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

  1. L36
    specialize prime_field_polynomial_monic_normalization_entry (x1)
  2. L37
    apply prime_field_polynomial_monic_normalization_entry
  3. L38
    exact h
  4. L39
    exact hzero
  5. L40
    exact hc_right_left_witness_left
  6. L41
    exact hr_witness
09Establish huL42–48

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

  1. L42
  2. L43
    specialize prime_field_multiply_commutative (p)
  3. L44
    specialize prime_field_multiply_commutative (x)
  4. L45
    specialize prime_field_multiply_commutative (k)
  5. L46
    specialize prime_field_multiply_commutative (1)
  6. L47
    apply prime_field_multiply_commutative
  7. L48
    exact hc_right_left_witness_right_right
10Establish heL49–58

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

  1. L49
    have he : x1=1
  2. L50
    specialize prime_field_multiply_functional (p)
  3. L51
    specialize prime_field_multiply_functional (k)
  4. L52
    specialize prime_field_multiply_functional (x)
  5. L53
    specialize prime_field_multiply_functional (x1)
  6. L54
    specialize prime_field_multiply_functional (1)
  7. L55
    apply prime_field_multiply_functional
  8. L56
    exact hm
  9. L57
    exact hu
  10. L58
    rewrite he at hr_witness
11Calculate and transport equalitiesL59–59

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

  1. L59
    rewrite he at hr_witness
12Use earlier factsL60–60

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

  1. L60
    exact hr_witness

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro L
  8. 0008intro h
  9. 0009have hc : FpMonicNormalization(p,k,ab,ac,bb,bc,L)
  10. 0010exact h
  11. 0011cases hc
  12. 0012cases hc_right
  13. 0013cases hc_right_left
  14. 0014cases hc_right_left_witness
  15. 0015cases hc_right_left_witness_right
  16. 0016have hzero : Lt(0,L)
  17. 0017specialize one_le_of_ne_zero (L)
  18. 0018apply one_le_of_ne_zero
  19. 0019exact hc_left
  20. 0020have hr : ∃ r. BetaAt(bb,bc,0,r)
  21. 0021specialize beta_at_exists (bb)
  22. 0022specialize beta_at_exists (bc)
  23. 0023specialize beta_at_exists (0)
  24. 0024apply beta_at_exists
  25. 0025cases hr
  26. 0026have hm : FpMul(p,k,x,x1)
  27. 0027specialize prime_field_polynomial_monic_normalization_entry (p)
  28. 0028specialize prime_field_polynomial_monic_normalization_entry (k)
  29. 0029specialize prime_field_polynomial_monic_normalization_entry (ab)
  30. 0030specialize prime_field_polynomial_monic_normalization_entry (ac)
  31. 0031specialize prime_field_polynomial_monic_normalization_entry (bb)
  32. 0032specialize prime_field_polynomial_monic_normalization_entry (bc)
  33. 0033specialize prime_field_polynomial_monic_normalization_entry (L)
  34. 0034specialize prime_field_polynomial_monic_normalization_entry (0)
  35. 0035specialize prime_field_polynomial_monic_normalization_entry (x)
  36. 0036specialize prime_field_polynomial_monic_normalization_entry (x1)
  37. 0037apply prime_field_polynomial_monic_normalization_entry
  38. 0038exact h
  39. 0039exact hzero
  40. 0040exact hc_right_left_witness_left
  41. 0041exact hr_witness
  42. 0042have hu : FpMul(p,k,x,1)
  43. 0043specialize prime_field_multiply_commutative (p)
  44. 0044specialize prime_field_multiply_commutative (x)
  45. 0045specialize prime_field_multiply_commutative (k)
  46. 0046specialize prime_field_multiply_commutative (1)
  47. 0047apply prime_field_multiply_commutative
  48. 0048exact hc_right_left_witness_right_right
  49. 0049have he : x1=1
  50. 0050specialize prime_field_multiply_functional (p)
  51. 0051specialize prime_field_multiply_functional (k)
  52. 0052specialize prime_field_multiply_functional (x)
  53. 0053specialize prime_field_multiply_functional (x1)
  54. 0054specialize prime_field_multiply_functional (1)
  55. 0055apply prime_field_multiply_functional
  56. 0056exact hm
  57. 0057exact hu
  58. 0058rewrite he at hr_witness
  59. 0059rewrite he at hr_witness
  60. 0060exact hr_witness