PQ003E

prime_field_polynomial_monic_normalization_functional

Two actual normalizations have the same decoded length-L prefix; beta-code equality is deliberately not asserted.

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

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_monic_normalization_scalar_functionalprime_field_polynomial_scale_functional · checked external prerequisite
Original expanded first-order statement 
forall p k j ab ac bb bc cb cc L. (((~((L) = 0)) /\ (((exists pfm_leading_normalization_function_first. ((((exists ff_h_pfp_normalization_function_firstsource. ff_h_pfp_normalization_function_firstsource + S (pfm_leading_normalization_function_first) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_function_firstsource. ab = ff_q_pfp_normalization_function_firstsource * S ((S (0)) * ac) + (pfm_leading_normalization_function_first))) /\ ((((~((pfm_leading_normalization_function_first) = 0)) /\ ((((exists pfa_gap_normalization_function_firstinversemultiplicationleft. pfa_gap_normalization_function_firstinversemultiplicationleft + S (pfm_leading_normalization_function_first) = (p)) /\ (((exists pfa_gap_normalization_function_firstinversemultiplicationright. pfa_gap_normalization_function_firstinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_function_firstinversemultiplicationresultbound. pfa_gap_normalization_function_firstinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_function_firstinversemultiplicationresultcongruence pfa_offset_right_normalization_function_firstinversemultiplicationresultcongruence. ((pfm_leading_normalization_function_first) * (k)) + (p) * pfa_offset_left_normalization_function_firstinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_function_firstinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_function_firstscalescalar. pfa_gap_normalization_function_firstscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_function_firstscale. (exists pfa_gap_normalization_function_firstscaleindex. pfa_gap_normalization_function_firstscaleindex + S (pfp_index_normalization_function_firstscale) = (L)) -> exists pfp_source_normalization_function_firstscale pfp_value_normalization_function_firstscale. ((((exists ff_h_pfp_normalization_function_firstscalesource. ff_h_pfp_normalization_function_firstscalesource + S (pfp_source_normalization_function_firstscale) = S ((S (pfp_index_normalization_function_firstscale)) * ac)) /\ exists ff_q_pfp_normalization_function_firstscalesource. ab = ff_q_pfp_normalization_function_firstscalesource * S ((S (pfp_index_normalization_function_firstscale)) * ac) + (pfp_source_normalization_function_firstscale))) /\ (((((exists ff_h_pfp_normalization_function_firstscaletarget. ff_h_pfp_normalization_function_firstscaletarget + S (pfp_value_normalization_function_firstscale) = S ((S (pfp_index_normalization_function_firstscale)) * bc)) /\ exists ff_q_pfp_normalization_function_firstscaletarget. bb = ff_q_pfp_normalization_function_firstscaletarget * S ((S (pfp_index_normalization_function_firstscale)) * bc) + (pfp_value_normalization_function_firstscale))) /\ ((((exists pfa_gap_normalization_function_firstscaleoperationleft. pfa_gap_normalization_function_firstscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_function_firstscaleoperationright. pfa_gap_normalization_function_firstscaleoperationright + S (pfp_source_normalization_function_firstscale) = (p)) /\ ((((exists pfa_gap_normalization_function_firstscaleoperationresultbound. pfa_gap_normalization_function_firstscaleoperationresultbound + S (pfp_value_normalization_function_firstscale) = (p)) /\ ((exists pfa_offset_left_normalization_function_firstscaleoperationresultcongruence pfa_offset_right_normalization_function_firstscaleoperationresultcongruence. ((k) * (pfp_source_normalization_function_firstscale)) + (p) * pfa_offset_left_normalization_function_firstscaleoperationresultcongruence = (pfp_value_normalization_function_firstscale) + (p) * pfa_offset_right_normalization_function_firstscaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_function_second. ((((exists ff_h_pfp_normalization_function_secondsource. ff_h_pfp_normalization_function_secondsource + S (pfm_leading_normalization_function_second) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_function_secondsource. ab = ff_q_pfp_normalization_function_secondsource * S ((S (0)) * ac) + (pfm_leading_normalization_function_second))) /\ ((((~((pfm_leading_normalization_function_second) = 0)) /\ ((((exists pfa_gap_normalization_function_secondinversemultiplicationleft. pfa_gap_normalization_function_secondinversemultiplicationleft + S (pfm_leading_normalization_function_second) = (p)) /\ (((exists pfa_gap_normalization_function_secondinversemultiplicationright. pfa_gap_normalization_function_secondinversemultiplicationright + S (j) = (p)) /\ ((((exists pfa_gap_normalization_function_secondinversemultiplicationresultbound. pfa_gap_normalization_function_secondinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_function_secondinversemultiplicationresultcongruence pfa_offset_right_normalization_function_secondinversemultiplicationresultcongruence. ((pfm_leading_normalization_function_second) * (j)) + (p) * pfa_offset_left_normalization_function_secondinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_function_secondinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_function_secondscalescalar. pfa_gap_normalization_function_secondscalescalar + S (j) = (p)) /\ ((forall pfp_index_normalization_function_secondscale. (exists pfa_gap_normalization_function_secondscaleindex. pfa_gap_normalization_function_secondscaleindex + S (pfp_index_normalization_function_secondscale) = (L)) -> exists pfp_source_normalization_function_secondscale pfp_value_normalization_function_secondscale. ((((exists ff_h_pfp_normalization_function_secondscalesource. ff_h_pfp_normalization_function_secondscalesource + S (pfp_source_normalization_function_secondscale) = S ((S (pfp_index_normalization_function_secondscale)) * ac)) /\ exists ff_q_pfp_normalization_function_secondscalesource. ab = ff_q_pfp_normalization_function_secondscalesource * S ((S (pfp_index_normalization_function_secondscale)) * ac) + (pfp_source_normalization_function_secondscale))) /\ (((((exists ff_h_pfp_normalization_function_secondscaletarget. ff_h_pfp_normalization_function_secondscaletarget + S (pfp_value_normalization_function_secondscale) = S ((S (pfp_index_normalization_function_secondscale)) * cc)) /\ exists ff_q_pfp_normalization_function_secondscaletarget. cb = ff_q_pfp_normalization_function_secondscaletarget * S ((S (pfp_index_normalization_function_secondscale)) * cc) + (pfp_value_normalization_function_secondscale))) /\ ((((exists pfa_gap_normalization_function_secondscaleoperationleft. pfa_gap_normalization_function_secondscaleoperationleft + S (j) = (p)) /\ (((exists pfa_gap_normalization_function_secondscaleoperationright. pfa_gap_normalization_function_secondscaleoperationright + S (pfp_source_normalization_function_secondscale) = (p)) /\ ((((exists pfa_gap_normalization_function_secondscaleoperationresultbound. pfa_gap_normalization_function_secondscaleoperationresultbound + S (pfp_value_normalization_function_secondscale) = (p)) /\ ((exists pfa_offset_left_normalization_function_secondscaleoperationresultcongruence pfa_offset_right_normalization_function_secondscaleoperationresultcongruence. ((j) * (pfp_source_normalization_function_secondscale)) + (p) * pfa_offset_left_normalization_function_secondscaleoperationresultcongruence = (pfp_value_normalization_function_secondscale) + (p) * pfa_offset_right_normalization_function_secondscaleoperationresultcongruence)))))))))))))))))))))) -> (forall mdr_i_pfp_normalization_function_result mdr_a_pfp_normalization_function_result. (exists mdr_gap_pfp_normalization_function_resultb. mdr_gap_pfp_normalization_function_resultb + S (mdr_i_pfp_normalization_function_result) = (L)) -> (((exists ff_h_mdr_pfp_normalization_function_resulto. ff_h_mdr_pfp_normalization_function_resulto + S (mdr_a_pfp_normalization_function_result) = S ((S (mdr_i_pfp_normalization_function_result)) * bc)) /\ exists ff_q_mdr_pfp_normalization_function_resulto. bb = ff_q_mdr_pfp_normalization_function_resulto * S ((S (mdr_i_pfp_normalization_function_result)) * bc) + (mdr_a_pfp_normalization_function_result))) -> (((exists ff_h_mdr_pfp_normalization_function_resultn. ff_h_mdr_pfp_normalization_function_resultn + S (mdr_a_pfp_normalization_function_result) = S ((S (mdr_i_pfp_normalization_function_result)) * cc)) /\ exists ff_q_mdr_pfp_normalization_function_resultn. cb = ff_q_mdr_pfp_normalization_function_resultn * S ((S (mdr_i_pfp_normalization_function_result)) * cc) + (mdr_a_pfp_normalization_function_result))))

Complete tactic proof in conservative notation

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

45 script commands · 8 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 scalar 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–12

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

  1. L11
    intro hfirst
  2. L12
    intro hsecond
03Establish heL13–22

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

  1. L13
    have he : j=k
  2. L14
    specialize prime_field_polynomial_monic_normalization_scalar_functional (p)
  3. L15
    specialize prime_field_polynomial_monic_normalization_scalar_functional (j)
  4. L16
    specialize prime_field_polynomial_monic_normalization_scalar_functional (k)
  5. L17
    specialize prime_field_polynomial_monic_normalization_scalar_functional (ab)
  6. L18
    specialize prime_field_polynomial_monic_normalization_scalar_functional (ac)
  7. L19
    specialize prime_field_polynomial_monic_normalization_scalar_functional (cb)
  8. L20
    specialize prime_field_polynomial_monic_normalization_scalar_functional (cc)
  9. L21
    specialize prime_field_polynomial_monic_normalization_scalar_functional (bb)
  10. L22
    specialize prime_field_polynomial_monic_normalization_scalar_functional (bc)
04Use earlier factsL23–26

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

  1. L23
    specialize prime_field_polynomial_monic_normalization_scalar_functional (L)
  2. L24
    apply prime_field_polynomial_monic_normalization_scalar_functional
  3. L25
    exact hsecond
  4. L26
    exact hfirst
05Separate the logical casesL27–30

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

  1. L27
    cases hfirst
  2. L28
    cases hfirst_right
  3. L29
    cases hsecond
  4. L30
    cases hsecond_right
06Calculate and transport equalitiesL31–33

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

  1. L31
    rewrite he at hsecond_right_right
  2. L32
    rewrite he at hsecond_right_right
  3. L33
    rewrite he at hsecond_right_right
07Use earlier factsL34–43

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

  1. L34
    specialize prime_field_polynomial_scale_functional (p)
  2. L35
    specialize prime_field_polynomial_scale_functional (k)
  3. L36
    specialize prime_field_polynomial_scale_functional (ab)
  4. L37
    specialize prime_field_polynomial_scale_functional (ac)
  5. L38
    specialize prime_field_polynomial_scale_functional (bb)
  6. L39
    specialize prime_field_polynomial_scale_functional (bc)
  7. L40
    specialize prime_field_polynomial_scale_functional (cb)
  8. L41
    specialize prime_field_polynomial_scale_functional (cc)
  9. L42
    specialize prime_field_polynomial_scale_functional (L)
  10. L43
    apply prime_field_polynomial_scale_functional
08Use earlier factsL44–45

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

  1. L44
    exact hfirst_right_right
  2. L45
    exact hsecond_right_right

Library-wide reading audit

Original defined command ledger · 45 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 hfirst
  12. 0012intro hsecond
  13. 0013have he : j=k
  14. 0014specialize prime_field_polynomial_monic_normalization_scalar_functional (p)
  15. 0015specialize prime_field_polynomial_monic_normalization_scalar_functional (j)
  16. 0016specialize prime_field_polynomial_monic_normalization_scalar_functional (k)
  17. 0017specialize prime_field_polynomial_monic_normalization_scalar_functional (ab)
  18. 0018specialize prime_field_polynomial_monic_normalization_scalar_functional (ac)
  19. 0019specialize prime_field_polynomial_monic_normalization_scalar_functional (cb)
  20. 0020specialize prime_field_polynomial_monic_normalization_scalar_functional (cc)
  21. 0021specialize prime_field_polynomial_monic_normalization_scalar_functional (bb)
  22. 0022specialize prime_field_polynomial_monic_normalization_scalar_functional (bc)
  23. 0023specialize prime_field_polynomial_monic_normalization_scalar_functional (L)
  24. 0024apply prime_field_polynomial_monic_normalization_scalar_functional
  25. 0025exact hsecond
  26. 0026exact hfirst
  27. 0027cases hfirst
  28. 0028cases hfirst_right
  29. 0029cases hsecond
  30. 0030cases hsecond_right
  31. 0031rewrite he at hsecond_right_right
  32. 0032rewrite he at hsecond_right_right
  33. 0033rewrite he at hsecond_right_right
  34. 0034specialize prime_field_polynomial_scale_functional (p)
  35. 0035specialize prime_field_polynomial_scale_functional (k)
  36. 0036specialize prime_field_polynomial_scale_functional (ab)
  37. 0037specialize prime_field_polynomial_scale_functional (ac)
  38. 0038specialize prime_field_polynomial_scale_functional (bb)
  39. 0039specialize prime_field_polynomial_scale_functional (bc)
  40. 0040specialize prime_field_polynomial_scale_functional (cb)
  41. 0041specialize prime_field_polynomial_scale_functional (cc)
  42. 0042specialize prime_field_polynomial_scale_functional (L)
  43. 0043apply prime_field_polynomial_scale_functional
  44. 0044exact hfirst_right_right
  45. 0045exact hsecond_right_right