PQ003F

prime_field_polynomial_monic_normalization_value_functional

Every pair of actual in-range output decodings agrees; no claim is made for indices outside the prefix.

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. ∀ j. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ cb. ∀ cc. ∀ L. ∀ i. ∀ a. ∀ b. FpMonicNormalization(p,k,ab,ac,bb,bc,L) → FpMonicNormalization(p,j,ab,ac,cb,cc,L) → Lt(i,L) → BetaAt(bb,bc,i,a) → BetaAt(cb,cc,i,b) → a = b

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_monic_normalization_functionalbeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall p k j ab ac bb bc cb cc L i a b. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_value_first. ((((exists ff_h_pfp_normalization_value_firstsource. ff_h_pfp_normalization_value_firstsource + S (pfm_leading_normalization_value_first) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_value_firstsource. ab = ff_q_pfp_normalization_value_firstsource * S ((S (0)) * ac) + (pfm_leading_normalization_value_first))) /\ ((((~((pfm_leading_normalization_value_first) = 0)) /\ ((((exists pfa_gap_normalization_value_firstinversemultiplicationleft. pfa_gap_normalization_value_firstinversemultiplicationleft + S (pfm_leading_normalization_value_first) = (p)) /\ (((exists pfa_gap_normalization_value_firstinversemultiplicationright. pfa_gap_normalization_value_firstinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_value_firstinversemultiplicationresultbound. pfa_gap_normalization_value_firstinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_value_firstinversemultiplicationresultcongruence pfa_offset_right_normalization_value_firstinversemultiplicationresultcongruence. ((pfm_leading_normalization_value_first) * (k)) + (p) * pfa_offset_left_normalization_value_firstinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_value_firstinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_value_firstscalescalar. pfa_gap_normalization_value_firstscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_value_firstscale. (exists pfa_gap_normalization_value_firstscaleindex. pfa_gap_normalization_value_firstscaleindex + S (pfp_index_normalization_value_firstscale) = (L)) -> exists pfp_source_normalization_value_firstscale pfp_value_normalization_value_firstscale. ((((exists ff_h_pfp_normalization_value_firstscalesource. ff_h_pfp_normalization_value_firstscalesource + S (pfp_source_normalization_value_firstscale) = S ((S (pfp_index_normalization_value_firstscale)) * ac)) /\ exists ff_q_pfp_normalization_value_firstscalesource. ab = ff_q_pfp_normalization_value_firstscalesource * S ((S (pfp_index_normalization_value_firstscale)) * ac) + (pfp_source_normalization_value_firstscale))) /\ (((((exists ff_h_pfp_normalization_value_firstscaletarget. ff_h_pfp_normalization_value_firstscaletarget + S (pfp_value_normalization_value_firstscale) = S ((S (pfp_index_normalization_value_firstscale)) * bc)) /\ exists ff_q_pfp_normalization_value_firstscaletarget. bb = ff_q_pfp_normalization_value_firstscaletarget * S ((S (pfp_index_normalization_value_firstscale)) * bc) + (pfp_value_normalization_value_firstscale))) /\ ((((exists pfa_gap_normalization_value_firstscaleoperationleft. pfa_gap_normalization_value_firstscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_value_firstscaleoperationright. pfa_gap_normalization_value_firstscaleoperationright + S (pfp_source_normalization_value_firstscale) = (p)) /\ ((((exists pfa_gap_normalization_value_firstscaleoperationresultbound. pfa_gap_normalization_value_firstscaleoperationresultbound + S (pfp_value_normalization_value_firstscale) = (p)) /\ ((exists pfa_offset_left_normalization_value_firstscaleoperationresultcongruence pfa_offset_right_normalization_value_firstscaleoperationresultcongruence. ((k) * (pfp_source_normalization_value_firstscale)) + (p) * pfa_offset_left_normalization_value_firstscaleoperationresultcongruence = (pfp_value_normalization_value_firstscale) + (p) * pfa_offset_right_normalization_value_firstscaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_value_second. ((((exists ff_h_pfp_normalization_value_secondsource. ff_h_pfp_normalization_value_secondsource + S (pfm_leading_normalization_value_second) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_value_secondsource. ab = ff_q_pfp_normalization_value_secondsource * S ((S (0)) * ac) + (pfm_leading_normalization_value_second))) /\ ((((~((pfm_leading_normalization_value_second) = 0)) /\ ((((exists pfa_gap_normalization_value_secondinversemultiplicationleft. pfa_gap_normalization_value_secondinversemultiplicationleft + S (pfm_leading_normalization_value_second) = (p)) /\ (((exists pfa_gap_normalization_value_secondinversemultiplicationright. pfa_gap_normalization_value_secondinversemultiplicationright + S (j) = (p)) /\ ((((exists pfa_gap_normalization_value_secondinversemultiplicationresultbound. pfa_gap_normalization_value_secondinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_value_secondinversemultiplicationresultcongruence pfa_offset_right_normalization_value_secondinversemultiplicationresultcongruence. ((pfm_leading_normalization_value_second) * (j)) + (p) * pfa_offset_left_normalization_value_secondinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_value_secondinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_value_secondscalescalar. pfa_gap_normalization_value_secondscalescalar + S (j) = (p)) /\ ((forall pfp_index_normalization_value_secondscale. (exists pfa_gap_normalization_value_secondscaleindex. pfa_gap_normalization_value_secondscaleindex + S (pfp_index_normalization_value_secondscale) = (L)) -> exists pfp_source_normalization_value_secondscale pfp_value_normalization_value_secondscale. ((((exists ff_h_pfp_normalization_value_secondscalesource. ff_h_pfp_normalization_value_secondscalesource + S (pfp_source_normalization_value_secondscale) = S ((S (pfp_index_normalization_value_secondscale)) * ac)) /\ exists ff_q_pfp_normalization_value_secondscalesource. ab = ff_q_pfp_normalization_value_secondscalesource * S ((S (pfp_index_normalization_value_secondscale)) * ac) + (pfp_source_normalization_value_secondscale))) /\ (((((exists ff_h_pfp_normalization_value_secondscaletarget. ff_h_pfp_normalization_value_secondscaletarget + S (pfp_value_normalization_value_secondscale) = S ((S (pfp_index_normalization_value_secondscale)) * cc)) /\ exists ff_q_pfp_normalization_value_secondscaletarget. cb = ff_q_pfp_normalization_value_secondscaletarget * S ((S (pfp_index_normalization_value_secondscale)) * cc) + (pfp_value_normalization_value_secondscale))) /\ ((((exists pfa_gap_normalization_value_secondscaleoperationleft. pfa_gap_normalization_value_secondscaleoperationleft + S (j) = (p)) /\ (((exists pfa_gap_normalization_value_secondscaleoperationright. pfa_gap_normalization_value_secondscaleoperationright + S (pfp_source_normalization_value_secondscale) = (p)) /\ ((((exists pfa_gap_normalization_value_secondscaleoperationresultbound. pfa_gap_normalization_value_secondscaleoperationresultbound + S (pfp_value_normalization_value_secondscale) = (p)) /\ ((exists pfa_offset_left_normalization_value_secondscaleoperationresultcongruence pfa_offset_right_normalization_value_secondscaleoperationresultcongruence. ((j) * (pfp_source_normalization_value_secondscale)) + (p) * pfa_offset_left_normalization_value_secondscaleoperationresultcongruence = (pfp_value_normalization_value_secondscale) + (p) * pfa_offset_right_normalization_value_secondscaleoperationresultcongruence)))))))))))))))))))))) -> (exists pfa_gap_normalization_value_bound. pfa_gap_normalization_value_bound + S (i) = (L)) -> (((exists ff_h_pfp_normalization_value_left. ff_h_pfp_normalization_value_left + S (a) = S ((S (i)) * bc)) /\ exists ff_q_pfp_normalization_value_left. bb = ff_q_pfp_normalization_value_left * S ((S (i)) * bc) + (a))) -> (((exists ff_h_pfp_normalization_value_right. ff_h_pfp_normalization_value_right + S (b) = S ((S (i)) * cc)) /\ exists ff_q_pfp_normalization_value_right. cb = ff_q_pfp_normalization_value_right * S ((S (i)) * cc) + (b))) -> a=b

Complete tactic proof in conservative notation

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

44 script commands · 5 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.

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

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro j
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro bb
  7. L7
    intro bc
  8. L8
    intro cb
  9. L9
    intro cc
  10. L10
    intro L
02Fix variables and assumptionsL11–18

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

  1. L11
    intro i
  2. L12
    intro a
  3. L13
    intro b
  4. L14
    intro hfirst
  5. L15
    intro hsecond
  6. L16
    intro hi
  7. L17
    intro ha
  8. L18
    intro hb
03Establish heL19–28

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

  1. L19
    have he : ∀ mdr_i_pfp_normalization_value_prefix. ∀ mdr_a_pfp_normalization_value_prefix. Lt(mdr_i_pfp_normalization_value_prefix,L) → BetaAt(bb,bc,mdr_i_pfp_normalization_value_prefix,mdr_a_pfp_normalization_value_prefix) → BetaAt(cb,cc,mdr_i_pfp_normalization_value_prefix,mdr_a_pfp_normalization_value_prefix)Definitions: Lt(mdr_i_pfp_normalization_value_prefix,L)BetaAt(bb,bc,mdr_i_pfp_normalization_value_prefix,mdr_a_pfp_normalization_value_prefix)BetaAt(cb,cc,mdr_i_pfp_normalization_value_prefix,mdr_a_pfp_normalization_value_prefix)Original native command in the exact edition
  2. L20
    specialize prime_field_polynomial_monic_normalization_functional (p)
  3. L21
    specialize prime_field_polynomial_monic_normalization_functional (k)
  4. L22
    specialize prime_field_polynomial_monic_normalization_functional (j)
  5. L23
    specialize prime_field_polynomial_monic_normalization_functional (ab)
  6. L24
    specialize prime_field_polynomial_monic_normalization_functional (ac)
  7. L25
    specialize prime_field_polynomial_monic_normalization_functional (bb)
  8. L26
    specialize prime_field_polynomial_monic_normalization_functional (bc)
  9. L27
    specialize prime_field_polynomial_monic_normalization_functional (cb)
  10. L28
    specialize prime_field_polynomial_monic_normalization_functional (cc)
04Use earlier factsL29–38

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

  1. L29
    specialize prime_field_polynomial_monic_normalization_functional (L)
  2. L30
    apply prime_field_polynomial_monic_normalization_functional
  3. L31
    exact hfirst
  4. L32
    exact hsecond
  5. L33
    specialize beta_at_unique (cb)
  6. L34
    specialize beta_at_unique (cc)
  7. L35
    specialize beta_at_unique (i)
  8. L36
    specialize beta_at_unique (a)
  9. L37
    specialize beta_at_unique (b)
  10. L38
    apply beta_at_unique
05Use earlier factsL39–44

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

  1. L39
    specialize he (i)
  2. L40
    specialize he (a)
  3. L41
    apply he
  4. L42
    exact hi
  5. L43
    exact ha
  6. L44
    exact hb

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro j
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro bb
  7. 0007intro bc
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro L
  11. 0011intro i
  12. 0012intro a
  13. 0013intro b
  14. 0014intro hfirst
  15. 0015intro hsecond
  16. 0016intro hi
  17. 0017intro ha
  18. 0018intro hb
  19. 0019have he : ∀ mdr_i_pfp_normalization_value_prefix. ∀ mdr_a_pfp_normalization_value_prefix. Lt(mdr_i_pfp_normalization_value_prefix,L) → BetaAt(bb,bc,mdr_i_pfp_normalization_value_prefix,mdr_a_pfp_normalization_value_prefix) → BetaAt(cb,cc,mdr_i_pfp_normalization_value_prefix,mdr_a_pfp_normalization_value_prefix)
  20. 0020specialize prime_field_polynomial_monic_normalization_functional (p)
  21. 0021specialize prime_field_polynomial_monic_normalization_functional (k)
  22. 0022specialize prime_field_polynomial_monic_normalization_functional (j)
  23. 0023specialize prime_field_polynomial_monic_normalization_functional (ab)
  24. 0024specialize prime_field_polynomial_monic_normalization_functional (ac)
  25. 0025specialize prime_field_polynomial_monic_normalization_functional (bb)
  26. 0026specialize prime_field_polynomial_monic_normalization_functional (bc)
  27. 0027specialize prime_field_polynomial_monic_normalization_functional (cb)
  28. 0028specialize prime_field_polynomial_monic_normalization_functional (cc)
  29. 0029specialize prime_field_polynomial_monic_normalization_functional (L)
  30. 0030apply prime_field_polynomial_monic_normalization_functional
  31. 0031exact hfirst
  32. 0032exact hsecond
  33. 0033specialize beta_at_unique (cb)
  34. 0034specialize beta_at_unique (cc)
  35. 0035specialize beta_at_unique (i)
  36. 0036specialize beta_at_unique (a)
  37. 0037specialize beta_at_unique (b)
  38. 0038apply beta_at_unique
  39. 0039specialize he (i)
  40. 0040specialize he (a)
  41. 0041apply he
  42. 0042exact hi
  43. 0043exact ha
  44. 0044exact hb