PX0017

prime_field_polynomial_left_pad_functional

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

Any two constructed left pads have equal decoded coefficients on the full padded length.

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 L t d e f g. (((forall pfp_repeat_index_left_pad_functional_firstzeros. (exists pfa_gap_left_pad_functional_firstzerosindex. pfa_gap_left_pad_functional_firstzerosindex + S (pfp_repeat_index_left_pad_functional_firstzeros) = (t)) -> (((exists ff_h_pfp_left_pad_functional_firstzerosentry. ff_h_pfp_left_pad_functional_firstzerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_functional_firstzeros)) * e)) /\ exists ff_q_pfp_left_pad_functional_firstzerosentry. d = ff_q_pfp_left_pad_functional_firstzerosentry * S ((S (pfp_repeat_index_left_pad_functional_firstzeros)) * e) + (0)))) /\ ((forall pfrep_index_left_pad_functional_first pfrep_value_left_pad_functional_first. (exists pfa_gap_left_pad_functional_firstbound. pfa_gap_left_pad_functional_firstbound + S (pfrep_index_left_pad_functional_first) = (L)) -> (((exists ff_h_pfp_left_pad_functional_firstinput. ff_h_pfp_left_pad_functional_firstinput + S (pfrep_value_left_pad_functional_first) = S ((S (pfrep_index_left_pad_functional_first)) * c)) /\ exists ff_q_pfp_left_pad_functional_firstinput. b = ff_q_pfp_left_pad_functional_firstinput * S ((S (pfrep_index_left_pad_functional_first)) * c) + (pfrep_value_left_pad_functional_first))) -> (((exists ff_h_pfp_left_pad_functional_firstoutput. ff_h_pfp_left_pad_functional_firstoutput + S (pfrep_value_left_pad_functional_first) = S ((S ((t)+pfrep_index_left_pad_functional_first)) * e)) /\ exists ff_q_pfp_left_pad_functional_firstoutput. d = ff_q_pfp_left_pad_functional_firstoutput * S ((S ((t)+pfrep_index_left_pad_functional_first)) * e) + (pfrep_value_left_pad_functional_first))))))) -> (((forall pfp_repeat_index_left_pad_functional_secondzeros. (exists pfa_gap_left_pad_functional_secondzerosindex. pfa_gap_left_pad_functional_secondzerosindex + S (pfp_repeat_index_left_pad_functional_secondzeros) = (t)) -> (((exists ff_h_pfp_left_pad_functional_secondzerosentry. ff_h_pfp_left_pad_functional_secondzerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_functional_secondzeros)) * g)) /\ exists ff_q_pfp_left_pad_functional_secondzerosentry. f = ff_q_pfp_left_pad_functional_secondzerosentry * S ((S (pfp_repeat_index_left_pad_functional_secondzeros)) * g) + (0)))) /\ ((forall pfrep_index_left_pad_functional_second pfrep_value_left_pad_functional_second. (exists pfa_gap_left_pad_functional_secondbound. pfa_gap_left_pad_functional_secondbound + S (pfrep_index_left_pad_functional_second) = (L)) -> (((exists ff_h_pfp_left_pad_functional_secondinput. ff_h_pfp_left_pad_functional_secondinput + S (pfrep_value_left_pad_functional_second) = S ((S (pfrep_index_left_pad_functional_second)) * c)) /\ exists ff_q_pfp_left_pad_functional_secondinput. b = ff_q_pfp_left_pad_functional_secondinput * S ((S (pfrep_index_left_pad_functional_second)) * c) + (pfrep_value_left_pad_functional_second))) -> (((exists ff_h_pfp_left_pad_functional_secondoutput. ff_h_pfp_left_pad_functional_secondoutput + S (pfrep_value_left_pad_functional_second) = S ((S ((t)+pfrep_index_left_pad_functional_second)) * g)) /\ exists ff_q_pfp_left_pad_functional_secondoutput. f = ff_q_pfp_left_pad_functional_secondoutput * S ((S ((t)+pfrep_index_left_pad_functional_second)) * g) + (pfrep_value_left_pad_functional_second))))))) -> (forall mdr_i_pfp_left_pad_functional_result mdr_a_pfp_left_pad_functional_result. (exists mdr_gap_pfp_left_pad_functional_resultb. mdr_gap_pfp_left_pad_functional_resultb + S (mdr_i_pfp_left_pad_functional_result) = (t+L)) -> (((exists ff_h_mdr_pfp_left_pad_functional_resulto. ff_h_mdr_pfp_left_pad_functional_resulto + S (mdr_a_pfp_left_pad_functional_result) = S ((S (mdr_i_pfp_left_pad_functional_result)) * e)) /\ exists ff_q_mdr_pfp_left_pad_functional_resulto. d = ff_q_mdr_pfp_left_pad_functional_resulto * S ((S (mdr_i_pfp_left_pad_functional_result)) * e) + (mdr_a_pfp_left_pad_functional_result))) -> (((exists ff_h_mdr_pfp_left_pad_functional_resultn. ff_h_mdr_pfp_left_pad_functional_resultn + S (mdr_a_pfp_left_pad_functional_result) = S ((S (mdr_i_pfp_left_pad_functional_result)) * g)) /\ exists ff_q_mdr_pfp_left_pad_functional_resultn. f = ff_q_mdr_pfp_left_pad_functional_resultn * S ((S (mdr_i_pfp_left_pad_functional_result)) * g) + (mdr_a_pfp_left_pad_functional_result))))

Constructive proof overview

Generated structural guide

Any two constructed left pads have equal decoded coefficients on the full padded length.

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

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

Proof neighborhood

Direct dependencies

PX000A prime_field_polynomial_left_pad_index_cases beta_at_unique Alpha theorem; checked-use authorized beta_at_exists Alpha theorem; checked-use authorized

Direct dependents

none

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

71 script commands · 16 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.

Named ingredients (1)
prime field polynomial left pad index cases
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro L
  4. L4
    intro t
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro hd
  10. L10
    intro hf
02Fix variables and assumptionsL11–14

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

  1. L11
    intro i
  2. L12
    intro a
  3. L13
    intro hi
  4. L14
    intro ha
03Separate the logical casesL15–16

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

  1. L15
    cases hd
  2. L16
    cases hf
04Establish hoL17–22

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

  1. L17
    have ho : (exists pfa_gap_left_pad_equal_zero. pfa_gap_left_pad_equal_zero + S (i) = (t)) \/ exists j. (((exists pfa_gap_left_pad_equal_source. pfa_gap_left_pad_equal_source + S (j) = (L)) /\ ((i=t+j))))
  2. L18
    specialize prime_field_polynomial_left_pad_index_cases (t)
  3. L19
    specialize prime_field_polynomial_left_pad_index_cases (L)
  4. L20
    specialize prime_field_polynomial_left_pad_index_cases (i)
  5. L21
    apply prime_field_polynomial_left_pad_index_cases
  6. L22
    exact hi
05Separate the logical casesL23–23

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

  1. L23
    cases ho
06Establish heqL24–33

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

  1. L24
    have heq : a=0
  2. L25
    specialize beta_at_unique (d)
  3. L26
    specialize beta_at_unique (e)
  4. L27
    specialize beta_at_unique (i)
  5. L28
    specialize beta_at_unique (a)
  6. L29
    specialize beta_at_unique (0)
  7. L30
    apply beta_at_unique
  8. L31
    exact ha
  9. L32
    specialize hd_left (i)
  10. L33
    apply hd_left
07Use earlier factsL34–34

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

  1. L34
    exact ho_left
08Calculate and transport equalitiesL35–36

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

  1. L35
    rewrite heq
  2. L36
    rewrite heq
09Use earlier factsL37–39

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

  1. L37
    specialize hf_left (i)
  2. L38
    apply hf_left
  3. L39
    exact ho_left
10Separate the logical casesL40–41

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

  1. L40
    cases ho_right
  2. L41
    cases ho_right_witness
11Establish hvL42–46

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

  1. L42
    have hv : exists z. (((exists ff_h_pfp_left_pad_equal_choice. ff_h_pfp_left_pad_equal_choice + S (z) = S ((S (x)) * c)) /\ exists ff_q_pfp_left_pad_equal_choice. b = ff_q_pfp_left_pad_equal_choice * S ((S (x)) * c) + (z)))
  2. L43
    specialize beta_at_exists (b)
  3. L44
    specialize beta_at_exists (c)
  4. L45
    specialize beta_at_exists (x)
  5. L46
    apply beta_at_exists
12Separate the logical casesL47–47

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

  1. L47
    cases hv
13Establish heqL48–57

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

  1. L48
    have heq : a=x1
  2. L49
    specialize beta_at_unique (d)
  3. L50
    specialize beta_at_unique (e)
  4. L51
    specialize beta_at_unique (t+x)
  5. L52
    specialize beta_at_unique (a)
  6. L53
    specialize beta_at_unique (x1)
  7. L54
    apply beta_at_unique
  8. L55
    rewrite ho_right_witness_right at ha
  9. L56
    rewrite ho_right_witness_right at ha
  10. L57
    exact ha
14Use earlier factsL58–62

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

  1. L58
    specialize hd_right (x)
  2. L59
    specialize hd_right (x1)
  3. L60
    apply hd_right
  4. L61
    exact ho_right_witness_left
  5. L62
    exact hv_witness
15Calculate and transport equalitiesL63–66

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

  1. L63
    rewrite ho_right_witness_right
  2. L64
    rewrite ho_right_witness_right
  3. L65
    rewrite heq
  4. L66
    rewrite heq
16Use earlier factsL67–71

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

  1. L67
    specialize hf_right (x)
  2. L68
    specialize hf_right (x1)
  3. L69
    apply hf_right
  4. L70
    exact ho_right_witness_left
  5. L71
    exact hv_witness

Library-wide reading audit

Original exact command ledger · 71 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro t
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro hd
  10. 0010intro hf
  11. 0011intro i
  12. 0012intro a
  13. 0013intro hi
  14. 0014intro ha
  15. 0015cases hd
  16. 0016cases hf
  17. 0017have ho : (exists pfa_gap_left_pad_equal_zero. pfa_gap_left_pad_equal_zero + S (i) = (t)) \/ exists j. (((exists pfa_gap_left_pad_equal_source. pfa_gap_left_pad_equal_source + S (j) = (L)) /\ ((i=t+j))))
  18. 0018specialize prime_field_polynomial_left_pad_index_cases (t)
  19. 0019specialize prime_field_polynomial_left_pad_index_cases (L)
  20. 0020specialize prime_field_polynomial_left_pad_index_cases (i)
  21. 0021apply prime_field_polynomial_left_pad_index_cases
  22. 0022exact hi
  23. 0023cases ho
  24. 0024have heq : a=0
  25. 0025specialize beta_at_unique (d)
  26. 0026specialize beta_at_unique (e)
  27. 0027specialize beta_at_unique (i)
  28. 0028specialize beta_at_unique (a)
  29. 0029specialize beta_at_unique (0)
  30. 0030apply beta_at_unique
  31. 0031exact ha
  32. 0032specialize hd_left (i)
  33. 0033apply hd_left
  34. 0034exact ho_left
  35. 0035rewrite heq
  36. 0036rewrite heq
  37. 0037specialize hf_left (i)
  38. 0038apply hf_left
  39. 0039exact ho_left
  40. 0040cases ho_right
  41. 0041cases ho_right_witness
  42. 0042have hv : exists z. (((exists ff_h_pfp_left_pad_equal_choice. ff_h_pfp_left_pad_equal_choice + S (z) = S ((S (x)) * c)) /\ exists ff_q_pfp_left_pad_equal_choice. b = ff_q_pfp_left_pad_equal_choice * S ((S (x)) * c) + (z)))
  43. 0043specialize beta_at_exists (b)
  44. 0044specialize beta_at_exists (c)
  45. 0045specialize beta_at_exists (x)
  46. 0046apply beta_at_exists
  47. 0047cases hv
  48. 0048have heq : a=x1
  49. 0049specialize beta_at_unique (d)
  50. 0050specialize beta_at_unique (e)
  51. 0051specialize beta_at_unique (t+x)
  52. 0052specialize beta_at_unique (a)
  53. 0053specialize beta_at_unique (x1)
  54. 0054apply beta_at_unique
  55. 0055rewrite ho_right_witness_right at ha
  56. 0056rewrite ho_right_witness_right at ha
  57. 0057exact ha
  58. 0058specialize hd_right (x)
  59. 0059specialize hd_right (x1)
  60. 0060apply hd_right
  61. 0061exact ho_right_witness_left
  62. 0062exact hv_witness
  63. 0063rewrite ho_right_witness_right
  64. 0064rewrite ho_right_witness_right
  65. 0065rewrite heq
  66. 0066rewrite heq
  67. 0067specialize hf_right (x)
  68. 0068specialize hf_right (x1)
  69. 0069apply hf_right
  70. 0070exact ho_right_witness_left
  71. 0071exact hv_witness