PG006D

prime_field_polynomial_nonzero_leading_equivalent_length_bound

A nonzero coefficient at the leading power cannot be matched by an outside-prefix zero. This length bound needs neither primality nor canonical coefficients.

Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ d. ∀ bb. ∀ bc. ∀ M. ∀ a. BetaAt(ab,ac,0,a) → ¬a = 0 → PolynomialEquivalent(ab,ac,S d,bb,bc,M) → Lt(d,M)

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

Definition DAG

PolynomialEquivalent(b,c,L,d,e,M) · 1Le(a,b) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 1

Actual proof prerequisites

le_or_lt · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall ab ac d bb bc M a. (((exists ff_h_pfp_length_head. ff_h_pfp_length_head + S (a) = S ((S (0)) * ac)) /\ exists ff_q_pfp_length_head. ab = ff_q_pfp_length_head * S ((S (0)) * ac) + (a))) -> (~(a=0)) -> (forall pfrep_power_length_equivalent pfrep_left_length_equivalent pfrep_right_length_equivalent. ((exists pfrep_position_length_equivalentfirst. ((pfrep_position_length_equivalentfirst+S (pfrep_power_length_equivalent)=(S d)) /\ ((((exists ff_h_pfp_length_equivalentfirstentry. ff_h_pfp_length_equivalentfirstentry + S (pfrep_left_length_equivalent) = S ((S (pfrep_position_length_equivalentfirst)) * ac)) /\ exists ff_q_pfp_length_equivalentfirstentry. ab = ff_q_pfp_length_equivalentfirstentry * S ((S (pfrep_position_length_equivalentfirst)) * ac) + (pfrep_left_length_equivalent)))))) \/ (((exists pfrep_gap_length_equivalentfirstoutside. pfrep_gap_length_equivalentfirstoutside+(S d)=(pfrep_power_length_equivalent)) /\ (((pfrep_left_length_equivalent)=0))))) -> ((exists pfrep_position_length_equivalentsecond. ((pfrep_position_length_equivalentsecond+S (pfrep_power_length_equivalent)=(M)) /\ ((((exists ff_h_pfp_length_equivalentsecondentry. ff_h_pfp_length_equivalentsecondentry + S (pfrep_right_length_equivalent) = S ((S (pfrep_position_length_equivalentsecond)) * bc)) /\ exists ff_q_pfp_length_equivalentsecondentry. bb = ff_q_pfp_length_equivalentsecondentry * S ((S (pfrep_position_length_equivalentsecond)) * bc) + (pfrep_right_length_equivalent)))))) \/ (((exists pfrep_gap_length_equivalentsecondoutside. pfrep_gap_length_equivalentsecondoutside+(M)=(pfrep_power_length_equivalent)) /\ (((pfrep_right_length_equivalent)=0))))) -> pfrep_left_length_equivalent=pfrep_right_length_equivalent) -> (exists pfc_gap_length_result. pfc_gap_length_result+(S d)=(M))

Complete tactic proof in conservative notation

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

31 script commands · 12 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 ab
  2. L2
    intro ac
  3. L3
    intro d
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro M
  7. L7
    intro a
  8. L8
    intro ha
  9. L9
    intro hne
  10. L10
    intro he
02Establish horderL11–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le or lt.

  1. L11
    have horder : Le(M,d) ∨ Lt(d,M)Definitions: Le(M,d)Lt(d,M)Original native command in the exact edition
  2. L12
    specialize le_or_lt (M)
  3. L13
    specialize le_or_lt (d)
  4. L14
    apply le_or_lt
03Separate the logical casesL15–16

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

  1. L15
    cases horder
  2. L16
    exfalso
04Use earlier factsL17–21

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

  1. L17
    apply hne
  2. L18
    specialize he (d)
  3. L19
    specialize he (a)
  4. L20
    specialize he (0)
  5. L21
    apply he
05Separate the logical casesL22–22

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

  1. L22
    left
06Construct an explicit witnessL23–23

Supply the displayed value, then prove that it has the required property.

  1. L23
    exists 0
07Separate the logical casesL24–24

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

  1. L24
    split
08Use earlier factsL25–26

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

  1. L25
    apply zero_add
  2. L26
    exact ha
09Separate the logical casesL27–28

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

  1. L27
    right
  2. L28
    split
10Use earlier factsL29–29

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

  1. L29
    exact horder_left
11Calculate and transport equalitiesL30–30

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

  1. L30
    refl
12Use earlier factsL31–31

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

  1. L31
    exact horder_right

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro d
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro M
  7. 0007intro a
  8. 0008intro ha
  9. 0009intro hne
  10. 0010intro he
  11. 0011have horder : Le(M,d) ∨ Lt(d,M)
  12. 0012specialize le_or_lt (M)
  13. 0013specialize le_or_lt (d)
  14. 0014apply le_or_lt
  15. 0015cases horder
  16. 0016exfalso
  17. 0017apply hne
  18. 0018specialize he (d)
  19. 0019specialize he (a)
  20. 0020specialize he (0)
  21. 0021apply he
  22. 0022left
  23. 0023exists 0
  24. 0024split
  25. 0025apply zero_add
  26. 0026exact ha
  27. 0027right
  28. 0028split
  29. 0029exact horder_left
  30. 0030refl
  31. 0031exact horder_right