PG006D

prime_field_polynomial_nonzero_leading_equivalent_length_bound

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

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

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 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))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

le_or_lt Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized

Direct dependents

PG006E prime_field_polynomial_equivalent_represented_degrees_equal PG006F prime_field_polynomial_product_equivalent_nonzero_left_nonempty

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

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.

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 : (exists pfc_gap_length_order. pfc_gap_length_order+(M)=(d)) \/ (exists pfa_gap_length_strict. pfa_gap_length_strict + S (d) = (M))
  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 exact 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 : (exists pfc_gap_length_order. pfc_gap_length_order+(M)=(d)) \/ (exists pfa_gap_length_strict. pfa_gap_length_strict + S (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