PX0001

polynomial_diagonal_left_prefix_transport

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

A genuine antidiagonal term below a shared left prefix survives changing its code and its declared input 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 ab ac L AB AC K bb bc M N i j t. (exists pfc_gap_tri_term_old_length. pfc_gap_tri_term_old_length+(N)=(L)) -> (exists pfc_gap_tri_term_new_length. pfc_gap_tri_term_new_length+(N)=(K)) -> (forall mdr_i_pfp_tri_term_equal mdr_a_pfp_tri_term_equal. (exists mdr_gap_pfp_tri_term_equalb. mdr_gap_pfp_tri_term_equalb + S (mdr_i_pfp_tri_term_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_term_equalo. ff_h_mdr_pfp_tri_term_equalo + S (mdr_a_pfp_tri_term_equal) = S ((S (mdr_i_pfp_tri_term_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_term_equalo. ab = ff_q_mdr_pfp_tri_term_equalo * S ((S (mdr_i_pfp_tri_term_equal)) * ac) + (mdr_a_pfp_tri_term_equal))) -> (((exists ff_h_mdr_pfp_tri_term_equaln. ff_h_mdr_pfp_tri_term_equaln + S (mdr_a_pfp_tri_term_equal) = S ((S (mdr_i_pfp_tri_term_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_term_equaln. AB = ff_q_mdr_pfp_tri_term_equaln * S ((S (mdr_i_pfp_tri_term_equal)) * AC) + (mdr_a_pfp_tri_term_equal)))) -> (exists pfa_gap_tri_term_index. pfa_gap_tri_term_index + S (j) = (N)) -> (exists pfc_complement_tri_term_old pfc_left_tri_term_old pfc_right_tri_term_old. (((j)+pfc_complement_tri_term_old=(i)) /\ ((((((exists pfa_gap_tri_term_oldleftinside. pfa_gap_tri_term_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_tri_term_oldleftentry. ff_h_pfp_tri_term_oldleftentry + S (pfc_left_tri_term_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_tri_term_oldleftentry. ab = ff_q_pfp_tri_term_oldleftentry * S ((S (j)) * ac) + (pfc_left_tri_term_old)))))) \/ (((exists pfc_gap_tri_term_oldleftoutside. pfc_gap_tri_term_oldleftoutside+(L)=(j)) /\ (((pfc_left_tri_term_old)=0))))) /\ ((((((exists pfa_gap_tri_term_oldrightinside. pfa_gap_tri_term_oldrightinside + S (pfc_complement_tri_term_old) = (M)) /\ ((((exists ff_h_pfp_tri_term_oldrightentry. ff_h_pfp_tri_term_oldrightentry + S (pfc_right_tri_term_old) = S ((S (pfc_complement_tri_term_old)) * bc)) /\ exists ff_q_pfp_tri_term_oldrightentry. bb = ff_q_pfp_tri_term_oldrightentry * S ((S (pfc_complement_tri_term_old)) * bc) + (pfc_right_tri_term_old)))))) \/ (((exists pfc_gap_tri_term_oldrightoutside. pfc_gap_tri_term_oldrightoutside+(M)=(pfc_complement_tri_term_old)) /\ (((pfc_right_tri_term_old)=0))))) /\ (((t)=pfc_left_tri_term_old*pfc_right_tri_term_old)))))))) -> (exists pfc_complement_tri_term_new pfc_left_tri_term_new pfc_right_tri_term_new. (((j)+pfc_complement_tri_term_new=(i)) /\ ((((((exists pfa_gap_tri_term_newleftinside. pfa_gap_tri_term_newleftinside + S (j) = (K)) /\ ((((exists ff_h_pfp_tri_term_newleftentry. ff_h_pfp_tri_term_newleftentry + S (pfc_left_tri_term_new) = S ((S (j)) * AC)) /\ exists ff_q_pfp_tri_term_newleftentry. AB = ff_q_pfp_tri_term_newleftentry * S ((S (j)) * AC) + (pfc_left_tri_term_new)))))) \/ (((exists pfc_gap_tri_term_newleftoutside. pfc_gap_tri_term_newleftoutside+(K)=(j)) /\ (((pfc_left_tri_term_new)=0))))) /\ ((((((exists pfa_gap_tri_term_newrightinside. pfa_gap_tri_term_newrightinside + S (pfc_complement_tri_term_new) = (M)) /\ ((((exists ff_h_pfp_tri_term_newrightentry. ff_h_pfp_tri_term_newrightentry + S (pfc_right_tri_term_new) = S ((S (pfc_complement_tri_term_new)) * bc)) /\ exists ff_q_pfp_tri_term_newrightentry. bb = ff_q_pfp_tri_term_newrightentry * S ((S (pfc_complement_tri_term_new)) * bc) + (pfc_right_tri_term_new)))))) \/ (((exists pfc_gap_tri_term_newrightoutside. pfc_gap_tri_term_newrightoutside+(M)=(pfc_complement_tri_term_new)) /\ (((pfc_right_tri_term_new)=0))))) /\ (((t)=pfc_left_tri_term_new*pfc_right_tri_term_new))))))))

Constructive proof overview

Generated structural guide

A genuine antidiagonal term below a shared left prefix survives changing its code and its declared input length.

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

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

Proof neighborhood

Direct dependencies

lt_of_lt_of_le Alpha theorem; checked-use authorized polynomial_zero_extended_entry_inside Alpha theorem; checked-use authorized

Direct dependents

PX0002 polynomial_diagonal_prefix_left_transport PX0003 prime_field_convolution_coefficient_prefix_transport

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

64 script commands · 13 reading checkpoints · 3 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 L
  4. L4
    intro AB
  5. L5
    intro AC
  6. L6
    intro K
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro M
  10. L10
    intro N
02Fix variables and assumptionsL11–18

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

  1. L11
    intro i
  2. L12
    intro j
  3. L13
    intro t
  4. L14
    intro hl
  5. L15
    intro hk
  6. L16
    intro he
  7. L17
    intro hj
  8. L18
    intro ht
03Separate the logical casesL19–24

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

  1. L19
    cases ht
  2. L20
    cases ht_witness
  3. L21
    cases ht_witness_witness
  4. L22
    cases ht_witness_witness_witness
  5. L23
    cases ht_witness_witness_witness_right
  6. L24
    cases ht_witness_witness_witness_right_right
04Establish hjlL25–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L25
    have hjl : exists pfa_gap_tri_term_inside_old. pfa_gap_tri_term_inside_old + S (j) = (L)
  2. L26
    specialize lt_of_lt_of_le (j)
  3. L27
    specialize lt_of_lt_of_le (N)
  4. L28
    specialize lt_of_lt_of_le (L)
  5. L29
    apply lt_of_lt_of_le
  6. L30
    exact hj
  7. L31
    exact hl
05Establish hjkL32–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L32
    have hjk : exists pfa_gap_tri_term_inside_new. pfa_gap_tri_term_inside_new + S (j) = (K)
  2. L33
    specialize lt_of_lt_of_le (j)
  3. L34
    specialize lt_of_lt_of_le (N)
  4. L35
    specialize lt_of_lt_of_le (K)
  5. L36
    apply lt_of_lt_of_le
  6. L37
    exact hj
  7. L38
    exact hk
06Establish haL39–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry inside.

  1. L39
    have ha : ((exists ff_h_pfp_tri_term_source_entry. ff_h_pfp_tri_term_source_entry + S (x1) = S ((S (j)) * ac)) /\ exists ff_q_pfp_tri_term_source_entry. ab = ff_q_pfp_tri_term_source_entry * S ((S (j)) * ac) + (x1))
  2. L40
    specialize polynomial_zero_extended_entry_inside (ab)
  3. L41
    specialize polynomial_zero_extended_entry_inside (ac)
  4. L42
    specialize polynomial_zero_extended_entry_inside (L)
  5. L43
    specialize polynomial_zero_extended_entry_inside (j)
  6. L44
    specialize polynomial_zero_extended_entry_inside (x1)
  7. L45
    apply polynomial_zero_extended_entry_inside
  8. L46
    exact hjl
  9. L47
    exact ht_witness_witness_witness_right_left
07Construct an explicit witnessL48–50

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

  1. L48
    exists x
  2. L49
    exists x1
  3. L50
    exists x2
08Separate the logical casesL51–51

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

  1. L51
    split
09Use earlier factsL52–52

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

  1. L52
    exact ht_witness_witness_witness_left
10Separate the logical casesL53–55

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

  1. L53
    split
  2. L54
    left
  3. L55
    split
11Use earlier factsL56–61

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

  1. L56
    exact hjk
  2. L57
    specialize he (j)
  3. L58
    specialize he (x1)
  4. L59
    apply he
  5. L60
    exact hj
  6. L61
    exact ha
12Separate the logical casesL62–62

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

  1. L62
    split
13Use earlier factsL63–64

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

  1. L63
    exact ht_witness_witness_witness_right_right_left
  2. L64
    exact ht_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 64 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro AB
  5. 0005intro AC
  6. 0006intro K
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro M
  10. 0010intro N
  11. 0011intro i
  12. 0012intro j
  13. 0013intro t
  14. 0014intro hl
  15. 0015intro hk
  16. 0016intro he
  17. 0017intro hj
  18. 0018intro ht
  19. 0019cases ht
  20. 0020cases ht_witness
  21. 0021cases ht_witness_witness
  22. 0022cases ht_witness_witness_witness
  23. 0023cases ht_witness_witness_witness_right
  24. 0024cases ht_witness_witness_witness_right_right
  25. 0025have hjl : exists pfa_gap_tri_term_inside_old. pfa_gap_tri_term_inside_old + S (j) = (L)
  26. 0026specialize lt_of_lt_of_le (j)
  27. 0027specialize lt_of_lt_of_le (N)
  28. 0028specialize lt_of_lt_of_le (L)
  29. 0029apply lt_of_lt_of_le
  30. 0030exact hj
  31. 0031exact hl
  32. 0032have hjk : exists pfa_gap_tri_term_inside_new. pfa_gap_tri_term_inside_new + S (j) = (K)
  33. 0033specialize lt_of_lt_of_le (j)
  34. 0034specialize lt_of_lt_of_le (N)
  35. 0035specialize lt_of_lt_of_le (K)
  36. 0036apply lt_of_lt_of_le
  37. 0037exact hj
  38. 0038exact hk
  39. 0039have ha : ((exists ff_h_pfp_tri_term_source_entry. ff_h_pfp_tri_term_source_entry + S (x1) = S ((S (j)) * ac)) /\ exists ff_q_pfp_tri_term_source_entry. ab = ff_q_pfp_tri_term_source_entry * S ((S (j)) * ac) + (x1))
  40. 0040specialize polynomial_zero_extended_entry_inside (ab)
  41. 0041specialize polynomial_zero_extended_entry_inside (ac)
  42. 0042specialize polynomial_zero_extended_entry_inside (L)
  43. 0043specialize polynomial_zero_extended_entry_inside (j)
  44. 0044specialize polynomial_zero_extended_entry_inside (x1)
  45. 0045apply polynomial_zero_extended_entry_inside
  46. 0046exact hjl
  47. 0047exact ht_witness_witness_witness_right_left
  48. 0048exists x
  49. 0049exists x1
  50. 0050exists x2
  51. 0051split
  52. 0052exact ht_witness_witness_witness_left
  53. 0053split
  54. 0054left
  55. 0055split
  56. 0056exact hjk
  57. 0057specialize he (j)
  58. 0058specialize he (x1)
  59. 0059apply he
  60. 0060exact hj
  61. 0061exact ha
  62. 0062split
  63. 0063exact ht_witness_witness_witness_right_right_left
  64. 0064exact ht_witness_witness_witness_right_right_right