PQ001B

prime_field_polynomial_suffix_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_affine_matrix_slice_exists Alpha theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized

Direct dependents

PQ0021 prime_field_polynomial_trim_exists

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

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.

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–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
  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 : exists z. (((exists ff_h_pfp_suffix_output. ff_h_pfp_suffix_output + S (z) = S ((S (i)) * x1)) /\ exists ff_q_pfp_suffix_output. x = ff_q_pfp_suffix_output * S ((S (i)) * x1) + (z)))
  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 exact command ledger · 40 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro M
  5. 0005have hs : exists d e. (forall ff_index_mcp_trim_suffix_actual ff_source_mcp_trim_suffix_actual ff_target_mcp_trim_suffix_actual. (exists mcp_gap_trim_suffix_actual_bound. mcp_gap_trim_suffix_actual_bound + S (ff_index_mcp_trim_suffix_actual) = (M)) -> (((exists fs_h_mcp_trim_suffix_actual_source. fs_h_mcp_trim_suffix_actual_source + S (ff_source_mcp_trim_suffix_actual) = S ((S ((t) + (1) * ff_index_mcp_trim_suffix_actual)) * c)) /\ exists fs_q_mcp_trim_suffix_actual_source. b = fs_q_mcp_trim_suffix_actual_source * S ((S ((t) + (1) * ff_index_mcp_trim_suffix_actual)) * c) + (ff_source_mcp_trim_suffix_actual))) -> (((exists fs_h_mcp_trim_suffix_actual_target. fs_h_mcp_trim_suffix_actual_target + S (ff_target_mcp_trim_suffix_actual) = S ((S (ff_index_mcp_trim_suffix_actual)) * e)) /\ exists fs_q_mcp_trim_suffix_actual_target. d = fs_q_mcp_trim_suffix_actual_target * S ((S (ff_index_mcp_trim_suffix_actual)) * e) + (ff_target_mcp_trim_suffix_actual))) -> ff_target_mcp_trim_suffix_actual = ff_source_mcp_trim_suffix_actual)
  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 : exists z. (((exists ff_h_pfp_suffix_output. ff_h_pfp_suffix_output + S (z) = S ((S (i)) * x1)) /\ exists ff_q_pfp_suffix_output. x = ff_q_pfp_suffix_output * S ((S (i)) * x1) + (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