PG0035

prime_field_polynomial_bounded_representative_at_length_exists

From L<=K construct a genuine leading-zero beta prefix of length K, retain canonical coefficients, and prove formal equivalence to the input, including empty prefixes.

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

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ K. Prime(p) → BetaPrefixInto(ab,ac,L,p) → Le(L,K) → ∃ x. ∃ y. BetaPrefixInto(x,y,K,p) ∧ PolynomialEquivalent(ab,ac,L,x,y,K)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2PolynomialLeftPad(b,c,L,t,d,e) · 1PolynomialEquivalent(b,c,L,d,e,M) · 1Le(a,b) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_left_pad_exists · checked external prerequisiteprime_field_polynomial_left_pad_bounded · checked external prerequisiteprime_field_polynomial_left_pad_equivalent · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L K. (~((p) = 1) /\ forall pfa_factor_left_alignment_prime pfa_factor_right_alignment_prime. (p) = pfa_factor_left_alignment_prime * pfa_factor_right_alignment_prime -> pfa_factor_left_alignment_prime = 1 \/ pfa_factor_right_alignment_prime = 1) -> (forall fom_index_pfp_alignment_input. (exists fom_gap_pfp_alignment_input_index_bound. fom_gap_pfp_alignment_input_index_bound + S (fom_index_pfp_alignment_input) = L) -> exists fom_value_pfp_alignment_input. ((((exists fom_beta_height_pfp_alignment_input_entry. fom_beta_height_pfp_alignment_input_entry + S (fom_value_pfp_alignment_input) = S ((S (fom_index_pfp_alignment_input)) * ac)) /\ exists fom_beta_quotient_pfp_alignment_input_entry. ab = fom_beta_quotient_pfp_alignment_input_entry * S ((S (fom_index_pfp_alignment_input)) * ac) + (fom_value_pfp_alignment_input))) /\ (exists fom_gap_pfp_alignment_input_value_bound. fom_gap_pfp_alignment_input_value_bound + S (fom_value_pfp_alignment_input) = p))) -> (exists pfrep_gap_alignment_length_bound. pfrep_gap_alignment_length_bound+(L)=(K)) -> (exists ub uc. ((forall fom_index_pfp_alignment_output_bounded. (exists fom_gap_pfp_alignment_output_bounded_index_bound. fom_gap_pfp_alignment_output_bounded_index_bound + S (fom_index_pfp_alignment_output_bounded) = K) -> exists fom_value_pfp_alignment_output_bounded. ((((exists fom_beta_height_pfp_alignment_output_bounded_entry. fom_beta_height_pfp_alignment_output_bounded_entry + S (fom_value_pfp_alignment_output_bounded) = S ((S (fom_index_pfp_alignment_output_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_alignment_output_bounded_entry. ub = fom_beta_quotient_pfp_alignment_output_bounded_entry * S ((S (fom_index_pfp_alignment_output_bounded)) * uc) + (fom_value_pfp_alignment_output_bounded))) /\ (exists fom_gap_pfp_alignment_output_bounded_value_bound. fom_gap_pfp_alignment_output_bounded_value_bound + S (fom_value_pfp_alignment_output_bounded) = p))) /\ ((forall pfrep_power_alignment_output_equivalent pfrep_left_alignment_output_equivalent pfrep_right_alignment_output_equivalent. ((exists pfrep_position_alignment_output_equivalentfirst. ((pfrep_position_alignment_output_equivalentfirst+S (pfrep_power_alignment_output_equivalent)=(L)) /\ ((((exists ff_h_pfp_alignment_output_equivalentfirstentry. ff_h_pfp_alignment_output_equivalentfirstentry + S (pfrep_left_alignment_output_equivalent) = S ((S (pfrep_position_alignment_output_equivalentfirst)) * ac)) /\ exists ff_q_pfp_alignment_output_equivalentfirstentry. ab = ff_q_pfp_alignment_output_equivalentfirstentry * S ((S (pfrep_position_alignment_output_equivalentfirst)) * ac) + (pfrep_left_alignment_output_equivalent)))))) \/ (((exists pfrep_gap_alignment_output_equivalentfirstoutside. pfrep_gap_alignment_output_equivalentfirstoutside+(L)=(pfrep_power_alignment_output_equivalent)) /\ (((pfrep_left_alignment_output_equivalent)=0))))) -> ((exists pfrep_position_alignment_output_equivalentsecond. ((pfrep_position_alignment_output_equivalentsecond+S (pfrep_power_alignment_output_equivalent)=(K)) /\ ((((exists ff_h_pfp_alignment_output_equivalentsecondentry. ff_h_pfp_alignment_output_equivalentsecondentry + S (pfrep_right_alignment_output_equivalent) = S ((S (pfrep_position_alignment_output_equivalentsecond)) * uc)) /\ exists ff_q_pfp_alignment_output_equivalentsecondentry. ub = ff_q_pfp_alignment_output_equivalentsecondentry * S ((S (pfrep_position_alignment_output_equivalentsecond)) * uc) + (pfrep_right_alignment_output_equivalent)))))) \/ (((exists pfrep_gap_alignment_output_equivalentsecondoutside. pfrep_gap_alignment_output_equivalentsecondoutside+(K)=(pfrep_power_alignment_output_equivalent)) /\ (((pfrep_right_alignment_output_equivalent)=0))))) -> pfrep_left_alignment_output_equivalent=pfrep_right_alignment_output_equivalent))))

Complete tactic proof in conservative notation

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

42 script commands · 11 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–8

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro K
  6. L6
    intro hp
  7. L7
    intro ha
  8. L8
    intro hlen
02Separate the logical casesL9–9

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

  1. L9
    cases hlen
03Establish hpadL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad exists.

  1. L10
    have hpad : ∃ ub. ∃ uc. PolynomialLeftPad(ab,ac,L,x,ub,uc)Definitions: PolynomialLeftPad(ab,ac,L,x,ub,uc)Original native command in the exact edition
  2. L11
    specialize prime_field_polynomial_left_pad_exists (ab)
  3. L12
    specialize prime_field_polynomial_left_pad_exists (ac)
  4. L13
    specialize prime_field_polynomial_left_pad_exists (x)
  5. L14
    specialize prime_field_polynomial_left_pad_exists (L)
  6. L15
    apply prime_field_polynomial_left_pad_exists
04Separate the logical casesL16–17

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

  1. L16
    cases hpad
  2. L17
    cases hpad_witness
05Construct an explicit witnessL18–19

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

  1. L18
    exists x1
  2. L19
    exists x2
06Separate the logical casesL20–20

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

  1. L20
    split
07Calculate and transport equalitiesL21–21

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

  1. L21
    rewrite <- hlen_witness
08Use earlier factsL22–31

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

  1. L22
    specialize prime_field_polynomial_left_pad_bounded (p)
  2. L23
    specialize prime_field_polynomial_left_pad_bounded (ab)
  3. L24
    specialize prime_field_polynomial_left_pad_bounded (ac)
  4. L25
    specialize prime_field_polynomial_left_pad_bounded (L)
  5. L26
    specialize prime_field_polynomial_left_pad_bounded (x)
  6. L27
    specialize prime_field_polynomial_left_pad_bounded (x1)
  7. L28
    specialize prime_field_polynomial_left_pad_bounded (x2)
  8. L29
    apply prime_field_polynomial_left_pad_bounded
  9. L30
    exact hp
  10. L31
    exact ha
09Use earlier factsL32–32

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

  1. L32
    exact hpad_witness_witness
10Calculate and transport equalitiesL33–34

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

  1. L33
    rewrite <- hlen_witness
  2. L34
    rewrite <- hlen_witness
11Use earlier factsL35–42

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

  1. L35
    specialize prime_field_polynomial_left_pad_equivalent (ab)
  2. L36
    specialize prime_field_polynomial_left_pad_equivalent (ac)
  3. L37
    specialize prime_field_polynomial_left_pad_equivalent (L)
  4. L38
    specialize prime_field_polynomial_left_pad_equivalent (x)
  5. L39
    specialize prime_field_polynomial_left_pad_equivalent (x1)
  6. L40
    specialize prime_field_polynomial_left_pad_equivalent (x2)
  7. L41
    apply prime_field_polynomial_left_pad_equivalent
  8. L42
    exact hpad_witness_witness

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro K
  6. 0006intro hp
  7. 0007intro ha
  8. 0008intro hlen
  9. 0009cases hlen
  10. 0010have hpad : ∃ ub. ∃ uc. PolynomialLeftPad(ab,ac,L,x,ub,uc)
  11. 0011specialize prime_field_polynomial_left_pad_exists (ab)
  12. 0012specialize prime_field_polynomial_left_pad_exists (ac)
  13. 0013specialize prime_field_polynomial_left_pad_exists (x)
  14. 0014specialize prime_field_polynomial_left_pad_exists (L)
  15. 0015apply prime_field_polynomial_left_pad_exists
  16. 0016cases hpad
  17. 0017cases hpad_witness
  18. 0018exists x1
  19. 0019exists x2
  20. 0020split
  21. 0021rewrite <- hlen_witness
  22. 0022specialize prime_field_polynomial_left_pad_bounded (p)
  23. 0023specialize prime_field_polynomial_left_pad_bounded (ab)
  24. 0024specialize prime_field_polynomial_left_pad_bounded (ac)
  25. 0025specialize prime_field_polynomial_left_pad_bounded (L)
  26. 0026specialize prime_field_polynomial_left_pad_bounded (x)
  27. 0027specialize prime_field_polynomial_left_pad_bounded (x1)
  28. 0028specialize prime_field_polynomial_left_pad_bounded (x2)
  29. 0029apply prime_field_polynomial_left_pad_bounded
  30. 0030exact hp
  31. 0031exact ha
  32. 0032exact hpad_witness_witness
  33. 0033rewrite <- hlen_witness
  34. 0034rewrite <- hlen_witness
  35. 0035specialize prime_field_polynomial_left_pad_equivalent (ab)
  36. 0036specialize prime_field_polynomial_left_pad_equivalent (ac)
  37. 0037specialize prime_field_polynomial_left_pad_equivalent (L)
  38. 0038specialize prime_field_polynomial_left_pad_equivalent (x)
  39. 0039specialize prime_field_polynomial_left_pad_equivalent (x1)
  40. 0040specialize prime_field_polynomial_left_pad_equivalent (x2)
  41. 0041apply prime_field_polynomial_left_pad_equivalent
  42. 0042exact hpad_witness_witness