PQ003F

prime_field_polynomial_monic_normalization_value_functional

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 44 exact native proof lines.

Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PQ003E prime_field_polynomial_monic_normalization_functional beta_at_unique Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
prime field polynomial monic normalization functional

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: LtBetaAt
  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 exact 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 : forall mdr_i_pfp_normalization_value_prefix mdr_a_pfp_normalization_value_prefix. (exists mdr_gap_pfp_normalization_value_prefixb. mdr_gap_pfp_normalization_value_prefixb + S (mdr_i_pfp_normalization_value_prefix) = (L)) -> (((exists ff_h_mdr_pfp_normalization_value_prefixo. ff_h_mdr_pfp_normalization_value_prefixo + S (mdr_a_pfp_normalization_value_prefix) = S ((S (mdr_i_pfp_normalization_value_prefix)) * bc)) /\ exists ff_q_mdr_pfp_normalization_value_prefixo. bb = ff_q_mdr_pfp_normalization_value_prefixo * S ((S (mdr_i_pfp_normalization_value_prefix)) * bc) + (mdr_a_pfp_normalization_value_prefix))) -> (((exists ff_h_mdr_pfp_normalization_value_prefixn. ff_h_mdr_pfp_normalization_value_prefixn + S (mdr_a_pfp_normalization_value_prefix) = S ((S (mdr_i_pfp_normalization_value_prefix)) * cc)) /\ exists ff_q_mdr_pfp_normalization_value_prefixn. cb = ff_q_mdr_pfp_normalization_value_prefixn * S ((S (mdr_i_pfp_normalization_value_prefix)) * cc) + (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