PQ001B

prime_field_polynomial_suffix_exists

Construct every finite beta-coded suffix by the existing actual affine-slice constructor at stride one, including length zero.

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

∀ b. ∀ c. ∀ t. ∀ M. ∃ d. ∃ e. PolynomialSuffix(b,c,t,d,e,M)

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

Definition DAG

MatrixAffineSlice(b,c,s,d,u,v,l) · 1PolynomialSuffix(b,c,t,d,e,M) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_affine_matrix_slice_exists · checked external prerequisitebeta_at_exists · checked external prerequisiteone_mul · checked external prerequisite
Original expanded first-order statement 
forall b c t M. exists d e. (forall pftrim_index_suffix_exists pftrim_value_suffix_exists. (exists pfa_gap_suffix_existsbound. pfa_gap_suffix_existsbound + S (pftrim_index_suffix_exists) = (M)) -> (((exists ff_h_pfp_suffix_existssource. ff_h_pfp_suffix_existssource + S (pftrim_value_suffix_exists) = S ((S ((t)+pftrim_index_suffix_exists)) * c)) /\ exists ff_q_pfp_suffix_existssource. b = ff_q_pfp_suffix_existssource * S ((S ((t)+pftrim_index_suffix_exists)) * c) + (pftrim_value_suffix_exists))) -> (((exists ff_h_pfp_suffix_existsoutput. ff_h_pfp_suffix_existsoutput + S (pftrim_value_suffix_exists) = S ((S (pftrim_index_suffix_exists)) * e)) /\ exists ff_q_pfp_suffix_existsoutput. d = ff_q_pfp_suffix_existsoutput * S ((S (pftrim_index_suffix_exists)) * e) + (pftrim_value_suffix_exists))))

Complete tactic proof in conservative notation

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

40 script commands · 9 reading checkpoints · 4 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–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro t
  4. L4
    intro M
02Establish hsL5–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta affine matrix slice exists.

  1. L5
    have hs : ∃ d. ∃ e. MatrixAffineSlice(b,c,t,1,d,e,M)Definitions: MatrixAffineSlice(b,c,t,1,d,e,M)Original native command in the exact edition
  2. L6
    specialize beta_affine_matrix_slice_exists (b)
  3. L7
    specialize beta_affine_matrix_slice_exists (c)
  4. L8
    specialize beta_affine_matrix_slice_exists (t)
  5. L9
    specialize beta_affine_matrix_slice_exists (1)
  6. L10
    specialize beta_affine_matrix_slice_exists (M)
  7. L11
    apply beta_affine_matrix_slice_exists
03Separate the logical casesL12–13

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

  1. L12
    cases hs
  2. L13
    cases hs_witness
04Construct an explicit witnessL14–15

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

  1. L14
    exists x
  2. L15
    exists x1
05Fix variables and assumptionsL16–19

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

  1. L16
    intro i
  2. L17
    intro a
  3. L18
    intro hi
  4. L19
    intro ha
06Establish hzL20–24

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

  1. L20
    have hz : ∃ z. BetaAt(x,x1,i,z)Definitions: BetaAt(x,x1,i,z)Original native command in the exact edition
  2. L21
    specialize beta_at_exists (x)
  3. L22
    specialize beta_at_exists (x1)
  4. L23
    specialize beta_at_exists (i)
  5. L24
    apply beta_at_exists
07Separate the logical casesL25–25

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

  1. L25
    cases hz
08Establish heqL26–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hs witness witness.

  1. L26
    have heq : x2=a
  2. L27
    specialize hs_witness_witness (i)
  3. L28
    specialize hs_witness_witness (a)
  4. L29
    specialize hs_witness_witness (x2)
  5. L30
    apply hs_witness_witness
  6. L31
    exact hi
09Establish hindexL32–40

Establish this local claim before using it. It is not an additional assumption.

  1. L32
    have hindex : t+1*i=t+i
  2. L33
    simp [one_mul]
  3. L34
    rewrite hindex
  4. L35
    rewrite hindex
  5. L36
    exact ha
  6. L37
    exact hz_witness
  7. L38
    rewrite heq at hz_witness
  8. L39
    rewrite heq at hz_witness
  9. L40
    exact hz_witness

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro M
  5. 0005have hs : ∃ d. ∃ e. MatrixAffineSlice(b,c,t,1,d,e,M)
  6. 0006specialize beta_affine_matrix_slice_exists (b)
  7. 0007specialize beta_affine_matrix_slice_exists (c)
  8. 0008specialize beta_affine_matrix_slice_exists (t)
  9. 0009specialize beta_affine_matrix_slice_exists (1)
  10. 0010specialize beta_affine_matrix_slice_exists (M)
  11. 0011apply beta_affine_matrix_slice_exists
  12. 0012cases hs
  13. 0013cases hs_witness
  14. 0014exists x
  15. 0015exists x1
  16. 0016intro i
  17. 0017intro a
  18. 0018intro hi
  19. 0019intro ha
  20. 0020have hz : ∃ z. BetaAt(x,x1,i,z)
  21. 0021specialize beta_at_exists (x)
  22. 0022specialize beta_at_exists (x1)
  23. 0023specialize beta_at_exists (i)
  24. 0024apply beta_at_exists
  25. 0025cases hz
  26. 0026have heq : x2=a
  27. 0027specialize hs_witness_witness (i)
  28. 0028specialize hs_witness_witness (a)
  29. 0029specialize hs_witness_witness (x2)
  30. 0030apply hs_witness_witness
  31. 0031exact hi
  32. 0032have hindex : t+1*i=t+i
  33. 0033simp [one_mul]
  34. 0034rewrite hindex
  35. 0035rewrite hindex
  36. 0036exact ha
  37. 0037exact hz_witness
  38. 0038rewrite heq at hz_witness
  39. 0039rewrite heq at hz_witness
  40. 0040exact hz_witness