PQ003D

prime_field_polynomial_monic_normalization_scalar_functional

The recorded canonical leading inverse is unique even when the source and target beta encodings are not.

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) → k = j

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

Definition DAG

FpMonicNormalization(p,k,ab,ac,bb,bc,L) · 2

Actual proof prerequisites

beta_at_unique · checked external prerequisiteprime_field_inverse_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_scalar_first. ((((exists ff_h_pfp_normalization_scalar_firstsource. ff_h_pfp_normalization_scalar_firstsource + S (pfm_leading_normalization_scalar_first) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_scalar_firstsource. ab = ff_q_pfp_normalization_scalar_firstsource * S ((S (0)) * ac) + (pfm_leading_normalization_scalar_first))) /\ ((((~((pfm_leading_normalization_scalar_first) = 0)) /\ ((((exists pfa_gap_normalization_scalar_firstinversemultiplicationleft. pfa_gap_normalization_scalar_firstinversemultiplicationleft + S (pfm_leading_normalization_scalar_first) = (p)) /\ (((exists pfa_gap_normalization_scalar_firstinversemultiplicationright. pfa_gap_normalization_scalar_firstinversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_normalization_scalar_firstinversemultiplicationresultbound. pfa_gap_normalization_scalar_firstinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_scalar_firstinversemultiplicationresultcongruence pfa_offset_right_normalization_scalar_firstinversemultiplicationresultcongruence. ((pfm_leading_normalization_scalar_first) * (k)) + (p) * pfa_offset_left_normalization_scalar_firstinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_scalar_firstinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_scalar_firstscalescalar. pfa_gap_normalization_scalar_firstscalescalar + S (k) = (p)) /\ ((forall pfp_index_normalization_scalar_firstscale. (exists pfa_gap_normalization_scalar_firstscaleindex. pfa_gap_normalization_scalar_firstscaleindex + S (pfp_index_normalization_scalar_firstscale) = (L)) -> exists pfp_source_normalization_scalar_firstscale pfp_value_normalization_scalar_firstscale. ((((exists ff_h_pfp_normalization_scalar_firstscalesource. ff_h_pfp_normalization_scalar_firstscalesource + S (pfp_source_normalization_scalar_firstscale) = S ((S (pfp_index_normalization_scalar_firstscale)) * ac)) /\ exists ff_q_pfp_normalization_scalar_firstscalesource. ab = ff_q_pfp_normalization_scalar_firstscalesource * S ((S (pfp_index_normalization_scalar_firstscale)) * ac) + (pfp_source_normalization_scalar_firstscale))) /\ (((((exists ff_h_pfp_normalization_scalar_firstscaletarget. ff_h_pfp_normalization_scalar_firstscaletarget + S (pfp_value_normalization_scalar_firstscale) = S ((S (pfp_index_normalization_scalar_firstscale)) * bc)) /\ exists ff_q_pfp_normalization_scalar_firstscaletarget. bb = ff_q_pfp_normalization_scalar_firstscaletarget * S ((S (pfp_index_normalization_scalar_firstscale)) * bc) + (pfp_value_normalization_scalar_firstscale))) /\ ((((exists pfa_gap_normalization_scalar_firstscaleoperationleft. pfa_gap_normalization_scalar_firstscaleoperationleft + S (k) = (p)) /\ (((exists pfa_gap_normalization_scalar_firstscaleoperationright. pfa_gap_normalization_scalar_firstscaleoperationright + S (pfp_source_normalization_scalar_firstscale) = (p)) /\ ((((exists pfa_gap_normalization_scalar_firstscaleoperationresultbound. pfa_gap_normalization_scalar_firstscaleoperationresultbound + S (pfp_value_normalization_scalar_firstscale) = (p)) /\ ((exists pfa_offset_left_normalization_scalar_firstscaleoperationresultcongruence pfa_offset_right_normalization_scalar_firstscaleoperationresultcongruence. ((k) * (pfp_source_normalization_scalar_firstscale)) + (p) * pfa_offset_left_normalization_scalar_firstscaleoperationresultcongruence = (pfp_value_normalization_scalar_firstscale) + (p) * pfa_offset_right_normalization_scalar_firstscaleoperationresultcongruence)))))))))))))))))))))) -> (((~((L) = 0)) /\ (((exists pfm_leading_normalization_scalar_second. ((((exists ff_h_pfp_normalization_scalar_secondsource. ff_h_pfp_normalization_scalar_secondsource + S (pfm_leading_normalization_scalar_second) = S ((S (0)) * ac)) /\ exists ff_q_pfp_normalization_scalar_secondsource. ab = ff_q_pfp_normalization_scalar_secondsource * S ((S (0)) * ac) + (pfm_leading_normalization_scalar_second))) /\ ((((~((pfm_leading_normalization_scalar_second) = 0)) /\ ((((exists pfa_gap_normalization_scalar_secondinversemultiplicationleft. pfa_gap_normalization_scalar_secondinversemultiplicationleft + S (pfm_leading_normalization_scalar_second) = (p)) /\ (((exists pfa_gap_normalization_scalar_secondinversemultiplicationright. pfa_gap_normalization_scalar_secondinversemultiplicationright + S (j) = (p)) /\ ((((exists pfa_gap_normalization_scalar_secondinversemultiplicationresultbound. pfa_gap_normalization_scalar_secondinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_normalization_scalar_secondinversemultiplicationresultcongruence pfa_offset_right_normalization_scalar_secondinversemultiplicationresultcongruence. ((pfm_leading_normalization_scalar_second) * (j)) + (p) * pfa_offset_left_normalization_scalar_secondinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_normalization_scalar_secondinversemultiplicationresultcongruence))))))))))))))) /\ ((((exists pfa_gap_normalization_scalar_secondscalescalar. pfa_gap_normalization_scalar_secondscalescalar + S (j) = (p)) /\ ((forall pfp_index_normalization_scalar_secondscale. (exists pfa_gap_normalization_scalar_secondscaleindex. pfa_gap_normalization_scalar_secondscaleindex + S (pfp_index_normalization_scalar_secondscale) = (L)) -> exists pfp_source_normalization_scalar_secondscale pfp_value_normalization_scalar_secondscale. ((((exists ff_h_pfp_normalization_scalar_secondscalesource. ff_h_pfp_normalization_scalar_secondscalesource + S (pfp_source_normalization_scalar_secondscale) = S ((S (pfp_index_normalization_scalar_secondscale)) * ac)) /\ exists ff_q_pfp_normalization_scalar_secondscalesource. ab = ff_q_pfp_normalization_scalar_secondscalesource * S ((S (pfp_index_normalization_scalar_secondscale)) * ac) + (pfp_source_normalization_scalar_secondscale))) /\ (((((exists ff_h_pfp_normalization_scalar_secondscaletarget. ff_h_pfp_normalization_scalar_secondscaletarget + S (pfp_value_normalization_scalar_secondscale) = S ((S (pfp_index_normalization_scalar_secondscale)) * cc)) /\ exists ff_q_pfp_normalization_scalar_secondscaletarget. cb = ff_q_pfp_normalization_scalar_secondscaletarget * S ((S (pfp_index_normalization_scalar_secondscale)) * cc) + (pfp_value_normalization_scalar_secondscale))) /\ ((((exists pfa_gap_normalization_scalar_secondscaleoperationleft. pfa_gap_normalization_scalar_secondscaleoperationleft + S (j) = (p)) /\ (((exists pfa_gap_normalization_scalar_secondscaleoperationright. pfa_gap_normalization_scalar_secondscaleoperationright + S (pfp_source_normalization_scalar_secondscale) = (p)) /\ ((((exists pfa_gap_normalization_scalar_secondscaleoperationresultbound. pfa_gap_normalization_scalar_secondscaleoperationresultbound + S (pfp_value_normalization_scalar_secondscale) = (p)) /\ ((exists pfa_offset_left_normalization_scalar_secondscaleoperationresultcongruence pfa_offset_right_normalization_scalar_secondscaleoperationresultcongruence. ((j) * (pfp_source_normalization_scalar_secondscale)) + (p) * pfa_offset_left_normalization_scalar_secondscaleoperationresultcongruence = (pfp_value_normalization_scalar_secondscale) + (p) * pfa_offset_right_normalization_scalar_secondscaleoperationresultcongruence)))))))))))))))))))))) -> k=j

Complete tactic proof in conservative notation

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

39 script commands · 6 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.

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
03Separate the logical casesL13–20

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

  1. L13
    cases hfirst
  2. L14
    cases hfirst_right
  3. L15
    cases hsecond
  4. L16
    cases hsecond_right
  5. L17
    cases hfirst_right_left
  6. L18
    cases hfirst_right_left_witness
  7. L19
    cases hsecond_right_left
  8. L20
    cases hsecond_right_left_witness
04Establish heL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L21
    have he : x1=x
  2. L22
    specialize beta_at_unique (ab)
  3. L23
    specialize beta_at_unique (ac)
  4. L24
    specialize beta_at_unique (0)
  5. L25
    specialize beta_at_unique (x1)
  6. L26
    specialize beta_at_unique (x)
  7. L27
    apply beta_at_unique
  8. L28
    exact hsecond_right_left_witness_left
  9. L29
    exact hfirst_right_left_witness_left
  10. L30
    rewrite he at hsecond_right_left_witness_right
05Calculate and transport equalitiesL31–32

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

  1. L31
    rewrite he at hsecond_right_left_witness_right
  2. L32
    rewrite he at hsecond_right_left_witness_right
06Use earlier factsL33–39

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

  1. L33
    specialize prime_field_inverse_functional (p)
  2. L34
    specialize prime_field_inverse_functional (x)
  3. L35
    specialize prime_field_inverse_functional (k)
  4. L36
    specialize prime_field_inverse_functional (j)
  5. L37
    apply prime_field_inverse_functional
  6. L38
    exact hfirst_right_left_witness_right
  7. L39
    exact hsecond_right_left_witness_right

Library-wide reading audit

Original defined command ledger · 39 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. 0013cases hfirst
  14. 0014cases hfirst_right
  15. 0015cases hsecond
  16. 0016cases hsecond_right
  17. 0017cases hfirst_right_left
  18. 0018cases hfirst_right_left_witness
  19. 0019cases hsecond_right_left
  20. 0020cases hsecond_right_left_witness
  21. 0021have he : x1=x
  22. 0022specialize beta_at_unique (ab)
  23. 0023specialize beta_at_unique (ac)
  24. 0024specialize beta_at_unique (0)
  25. 0025specialize beta_at_unique (x1)
  26. 0026specialize beta_at_unique (x)
  27. 0027apply beta_at_unique
  28. 0028exact hsecond_right_left_witness_left
  29. 0029exact hfirst_right_left_witness_left
  30. 0030rewrite he at hsecond_right_left_witness_right
  31. 0031rewrite he at hsecond_right_left_witness_right
  32. 0032rewrite he at hsecond_right_left_witness_right
  33. 0033specialize prime_field_inverse_functional (p)
  34. 0034specialize prime_field_inverse_functional (x)
  35. 0035specialize prime_field_inverse_functional (k)
  36. 0036specialize prime_field_inverse_functional (j)
  37. 0037apply prime_field_inverse_functional
  38. 0038exact hfirst_right_left_witness_right
  39. 0039exact hsecond_right_left_witness_right