PX0003

prime_field_convolution_coefficient_prefix_transport

Every coefficient below the shared prefix is unchanged, with its actual diagonal and sum witnesses reused verbatim.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ AB. ∀ AC. ∀ K. ∀ bb. ∀ bc. ∀ M. ∀ N. ∀ i. ∀ r. Le(N,L) → Le(N,K) → BetaPrefixEqual(ab,ac,AB,AC,N) → Lt(i,N) → FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) → FpConvolutionCoefficient(p,AB,AC,K,bb,bc,M,i,r)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 1FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) · 2Le(a,b) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

polynomial_diagonal_left_prefix_transportlt_of_lt_of_le · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L AB AC K bb bc M N i r. (exists pfc_gap_tri_coefficient_old_length. pfc_gap_tri_coefficient_old_length+(N)=(L)) -> (exists pfc_gap_tri_coefficient_new_length. pfc_gap_tri_coefficient_new_length+(N)=(K)) -> (forall mdr_i_pfp_tri_coefficient_equal mdr_a_pfp_tri_coefficient_equal. (exists mdr_gap_pfp_tri_coefficient_equalb. mdr_gap_pfp_tri_coefficient_equalb + S (mdr_i_pfp_tri_coefficient_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_coefficient_equalo. ff_h_mdr_pfp_tri_coefficient_equalo + S (mdr_a_pfp_tri_coefficient_equal) = S ((S (mdr_i_pfp_tri_coefficient_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_coefficient_equalo. ab = ff_q_mdr_pfp_tri_coefficient_equalo * S ((S (mdr_i_pfp_tri_coefficient_equal)) * ac) + (mdr_a_pfp_tri_coefficient_equal))) -> (((exists ff_h_mdr_pfp_tri_coefficient_equaln. ff_h_mdr_pfp_tri_coefficient_equaln + S (mdr_a_pfp_tri_coefficient_equal) = S ((S (mdr_i_pfp_tri_coefficient_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_coefficient_equaln. AB = ff_q_mdr_pfp_tri_coefficient_equaln * S ((S (mdr_i_pfp_tri_coefficient_equal)) * AC) + (mdr_a_pfp_tri_coefficient_equal)))) -> (exists pfa_gap_tri_coefficient_index. pfa_gap_tri_coefficient_index + S (i) = (N)) -> (exists pfc_terms_code_tri_coefficient_old pfc_terms_scale_tri_coefficient_old pfc_natural_sum_tri_coefficient_old. ((forall pfc_index_tri_coefficient_olddiagonal. (exists pfa_gap_tri_coefficient_olddiagonalbound. pfa_gap_tri_coefficient_olddiagonalbound + S (pfc_index_tri_coefficient_olddiagonal) = (S (i))) -> exists pfc_value_tri_coefficient_olddiagonal. ((((exists ff_h_pfp_tri_coefficient_olddiagonalentry. ff_h_pfp_tri_coefficient_olddiagonalentry + S (pfc_value_tri_coefficient_olddiagonal) = S ((S (pfc_index_tri_coefficient_olddiagonal)) * pfc_terms_scale_tri_coefficient_old)) /\ exists ff_q_pfp_tri_coefficient_olddiagonalentry. pfc_terms_code_tri_coefficient_old = ff_q_pfp_tri_coefficient_olddiagonalentry * S ((S (pfc_index_tri_coefficient_olddiagonal)) * pfc_terms_scale_tri_coefficient_old) + (pfc_value_tri_coefficient_olddiagonal))) /\ ((exists pfc_complement_tri_coefficient_olddiagonalterm pfc_left_tri_coefficient_olddiagonalterm pfc_right_tri_coefficient_olddiagonalterm. (((pfc_index_tri_coefficient_olddiagonal)+pfc_complement_tri_coefficient_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_coefficient_olddiagonaltermleftinside. pfa_gap_tri_coefficient_olddiagonaltermleftinside + S (pfc_index_tri_coefficient_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_tri_coefficient_olddiagonaltermleftentry. ff_h_pfp_tri_coefficient_olddiagonaltermleftentry + S (pfc_left_tri_coefficient_olddiagonalterm) = S ((S (pfc_index_tri_coefficient_olddiagonal)) * ac)) /\ exists ff_q_pfp_tri_coefficient_olddiagonaltermleftentry. ab = ff_q_pfp_tri_coefficient_olddiagonaltermleftentry * S ((S (pfc_index_tri_coefficient_olddiagonal)) * ac) + (pfc_left_tri_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_olddiagonaltermleftoutside. pfc_gap_tri_coefficient_olddiagonaltermleftoutside+(L)=(pfc_index_tri_coefficient_olddiagonal)) /\ (((pfc_left_tri_coefficient_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_coefficient_olddiagonaltermrightinside. pfa_gap_tri_coefficient_olddiagonaltermrightinside + S (pfc_complement_tri_coefficient_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_coefficient_olddiagonaltermrightentry. ff_h_pfp_tri_coefficient_olddiagonaltermrightentry + S (pfc_right_tri_coefficient_olddiagonalterm) = S ((S (pfc_complement_tri_coefficient_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_coefficient_olddiagonaltermrightentry. bb = ff_q_pfp_tri_coefficient_olddiagonaltermrightentry * S ((S (pfc_complement_tri_coefficient_olddiagonalterm)) * bc) + (pfc_right_tri_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_olddiagonaltermrightoutside. pfc_gap_tri_coefficient_olddiagonaltermrightoutside+(M)=(pfc_complement_tri_coefficient_olddiagonalterm)) /\ (((pfc_right_tri_coefficient_olddiagonalterm)=0))))) /\ (((pfc_value_tri_coefficient_olddiagonal)=pfc_left_tri_coefficient_olddiagonalterm*pfc_right_tri_coefficient_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_coefficient_oldsum fs_v_pfc_tri_coefficient_oldsum. ((((exists fs_h_pfc_tri_coefficient_oldsum_body_start. fs_h_pfc_tri_coefficient_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_start. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_start * S ((S (0)) * fs_v_pfc_tri_coefficient_oldsum) + (0))) /\ ((((exists fs_h_pfc_tri_coefficient_oldsum_body_terminal. fs_h_pfc_tri_coefficient_oldsum_body_terminal + S (pfc_natural_sum_tri_coefficient_old) = S ((S (S (i))) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_terminal. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_coefficient_oldsum) + (pfc_natural_sum_tri_coefficient_old))) /\ forall fs_i_pfc_tri_coefficient_oldsum_body_steps. (exists fs_lt_pfc_tri_coefficient_oldsum_body_steps_bound. fs_lt_pfc_tri_coefficient_oldsum_body_steps_bound + S fs_i_pfc_tri_coefficient_oldsum_body_steps = S (i)) -> exists fs_a_pfc_tri_coefficient_oldsum_body_steps fs_r_pfc_tri_coefficient_oldsum_body_steps fs_s_pfc_tri_coefficient_oldsum_body_steps. ((((exists fs_h_pfc_tri_coefficient_oldsum_body_steps_summand. fs_h_pfc_tri_coefficient_oldsum_body_steps_summand + S (fs_a_pfc_tri_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * pfc_terms_scale_tri_coefficient_old)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_steps_summand. pfc_terms_code_tri_coefficient_old = fs_q_pfc_tri_coefficient_oldsum_body_steps_summand * S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * pfc_terms_scale_tri_coefficient_old) + (fs_a_pfc_tri_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_oldsum_body_steps_partial. fs_h_pfc_tri_coefficient_oldsum_body_steps_partial + S (fs_r_pfc_tri_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_steps_partial. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_steps_partial * S ((S (fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum) + (fs_r_pfc_tri_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_oldsum_body_steps_successor. fs_h_pfc_tri_coefficient_oldsum_body_steps_successor + S (fs_s_pfc_tri_coefficient_oldsum_body_steps) = S ((S (S fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum)) /\ exists fs_q_pfc_tri_coefficient_oldsum_body_steps_successor. fs_u_pfc_tri_coefficient_oldsum = fs_q_pfc_tri_coefficient_oldsum_body_steps_successor * S ((S (S fs_i_pfc_tri_coefficient_oldsum_body_steps)) * fs_v_pfc_tri_coefficient_oldsum) + (fs_s_pfc_tri_coefficient_oldsum_body_steps))) /\ fs_s_pfc_tri_coefficient_oldsum_body_steps = fs_r_pfc_tri_coefficient_oldsum_body_steps + fs_a_pfc_tri_coefficient_oldsum_body_steps)))))) /\ ((((exists pfa_gap_tri_coefficient_oldresiduebound. pfa_gap_tri_coefficient_oldresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_coefficient_oldresiduecongruence pfa_offset_right_tri_coefficient_oldresiduecongruence. (pfc_natural_sum_tri_coefficient_old) + (p) * pfa_offset_left_tri_coefficient_oldresiduecongruence = (r) + (p) * pfa_offset_right_tri_coefficient_oldresiduecongruence))))))))) -> (exists pfc_terms_code_tri_coefficient_new pfc_terms_scale_tri_coefficient_new pfc_natural_sum_tri_coefficient_new. ((forall pfc_index_tri_coefficient_newdiagonal. (exists pfa_gap_tri_coefficient_newdiagonalbound. pfa_gap_tri_coefficient_newdiagonalbound + S (pfc_index_tri_coefficient_newdiagonal) = (S (i))) -> exists pfc_value_tri_coefficient_newdiagonal. ((((exists ff_h_pfp_tri_coefficient_newdiagonalentry. ff_h_pfp_tri_coefficient_newdiagonalentry + S (pfc_value_tri_coefficient_newdiagonal) = S ((S (pfc_index_tri_coefficient_newdiagonal)) * pfc_terms_scale_tri_coefficient_new)) /\ exists ff_q_pfp_tri_coefficient_newdiagonalentry. pfc_terms_code_tri_coefficient_new = ff_q_pfp_tri_coefficient_newdiagonalentry * S ((S (pfc_index_tri_coefficient_newdiagonal)) * pfc_terms_scale_tri_coefficient_new) + (pfc_value_tri_coefficient_newdiagonal))) /\ ((exists pfc_complement_tri_coefficient_newdiagonalterm pfc_left_tri_coefficient_newdiagonalterm pfc_right_tri_coefficient_newdiagonalterm. (((pfc_index_tri_coefficient_newdiagonal)+pfc_complement_tri_coefficient_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_coefficient_newdiagonaltermleftinside. pfa_gap_tri_coefficient_newdiagonaltermleftinside + S (pfc_index_tri_coefficient_newdiagonal) = (K)) /\ ((((exists ff_h_pfp_tri_coefficient_newdiagonaltermleftentry. ff_h_pfp_tri_coefficient_newdiagonaltermleftentry + S (pfc_left_tri_coefficient_newdiagonalterm) = S ((S (pfc_index_tri_coefficient_newdiagonal)) * AC)) /\ exists ff_q_pfp_tri_coefficient_newdiagonaltermleftentry. AB = ff_q_pfp_tri_coefficient_newdiagonaltermleftentry * S ((S (pfc_index_tri_coefficient_newdiagonal)) * AC) + (pfc_left_tri_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_newdiagonaltermleftoutside. pfc_gap_tri_coefficient_newdiagonaltermleftoutside+(K)=(pfc_index_tri_coefficient_newdiagonal)) /\ (((pfc_left_tri_coefficient_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_coefficient_newdiagonaltermrightinside. pfa_gap_tri_coefficient_newdiagonaltermrightinside + S (pfc_complement_tri_coefficient_newdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_coefficient_newdiagonaltermrightentry. ff_h_pfp_tri_coefficient_newdiagonaltermrightentry + S (pfc_right_tri_coefficient_newdiagonalterm) = S ((S (pfc_complement_tri_coefficient_newdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_coefficient_newdiagonaltermrightentry. bb = ff_q_pfp_tri_coefficient_newdiagonaltermrightentry * S ((S (pfc_complement_tri_coefficient_newdiagonalterm)) * bc) + (pfc_right_tri_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_coefficient_newdiagonaltermrightoutside. pfc_gap_tri_coefficient_newdiagonaltermrightoutside+(M)=(pfc_complement_tri_coefficient_newdiagonalterm)) /\ (((pfc_right_tri_coefficient_newdiagonalterm)=0))))) /\ (((pfc_value_tri_coefficient_newdiagonal)=pfc_left_tri_coefficient_newdiagonalterm*pfc_right_tri_coefficient_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_coefficient_newsum fs_v_pfc_tri_coefficient_newsum. ((((exists fs_h_pfc_tri_coefficient_newsum_body_start. fs_h_pfc_tri_coefficient_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_start. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_start * S ((S (0)) * fs_v_pfc_tri_coefficient_newsum) + (0))) /\ ((((exists fs_h_pfc_tri_coefficient_newsum_body_terminal. fs_h_pfc_tri_coefficient_newsum_body_terminal + S (pfc_natural_sum_tri_coefficient_new) = S ((S (S (i))) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_terminal. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_coefficient_newsum) + (pfc_natural_sum_tri_coefficient_new))) /\ forall fs_i_pfc_tri_coefficient_newsum_body_steps. (exists fs_lt_pfc_tri_coefficient_newsum_body_steps_bound. fs_lt_pfc_tri_coefficient_newsum_body_steps_bound + S fs_i_pfc_tri_coefficient_newsum_body_steps = S (i)) -> exists fs_a_pfc_tri_coefficient_newsum_body_steps fs_r_pfc_tri_coefficient_newsum_body_steps fs_s_pfc_tri_coefficient_newsum_body_steps. ((((exists fs_h_pfc_tri_coefficient_newsum_body_steps_summand. fs_h_pfc_tri_coefficient_newsum_body_steps_summand + S (fs_a_pfc_tri_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * pfc_terms_scale_tri_coefficient_new)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_steps_summand. pfc_terms_code_tri_coefficient_new = fs_q_pfc_tri_coefficient_newsum_body_steps_summand * S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * pfc_terms_scale_tri_coefficient_new) + (fs_a_pfc_tri_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_newsum_body_steps_partial. fs_h_pfc_tri_coefficient_newsum_body_steps_partial + S (fs_r_pfc_tri_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_steps_partial. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_steps_partial * S ((S (fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum) + (fs_r_pfc_tri_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_coefficient_newsum_body_steps_successor. fs_h_pfc_tri_coefficient_newsum_body_steps_successor + S (fs_s_pfc_tri_coefficient_newsum_body_steps) = S ((S (S fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum)) /\ exists fs_q_pfc_tri_coefficient_newsum_body_steps_successor. fs_u_pfc_tri_coefficient_newsum = fs_q_pfc_tri_coefficient_newsum_body_steps_successor * S ((S (S fs_i_pfc_tri_coefficient_newsum_body_steps)) * fs_v_pfc_tri_coefficient_newsum) + (fs_s_pfc_tri_coefficient_newsum_body_steps))) /\ fs_s_pfc_tri_coefficient_newsum_body_steps = fs_r_pfc_tri_coefficient_newsum_body_steps + fs_a_pfc_tri_coefficient_newsum_body_steps)))))) /\ ((((exists pfa_gap_tri_coefficient_newresiduebound. pfa_gap_tri_coefficient_newresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_coefficient_newresiduecongruence pfa_offset_right_tri_coefficient_newresiduecongruence. (pfc_natural_sum_tri_coefficient_new) + (p) * pfa_offset_left_tri_coefficient_newresiduecongruence = (r) + (p) * pfa_offset_right_tri_coefficient_newresiduecongruence)))))))))

Complete tactic proof in conservative notation

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

65 script commands · 15 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.

Named ingredients (1)
polynomial diagonal left prefix transport
01Fix variables and assumptionsL1–10

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 AB
  6. L6
    intro AC
  7. L7
    intro K
  8. L8
    intro bb
  9. L9
    intro bc
  10. L10
    intro M
02Fix variables and assumptionsL11–18

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

  1. L11
    intro N
  2. L12
    intro i
  3. L13
    intro r
  4. L14
    intro hl
  5. L15
    intro hk
  6. L16
    intro he
  7. L17
    intro hi
  8. L18
    intro hr
03Separate the logical casesL19–23

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

  1. L19
    cases hr
  2. L20
    cases hr_witness
  3. L21
    cases hr_witness_witness
  4. L22
    cases hr_witness_witness_witness
  5. L23
    cases hr_witness_witness_witness_right
04Construct an explicit witnessL24–26

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

  1. L24
    exists x
  2. L25
    exists x1
  3. L26
    exists x2
05Separate the logical casesL27–27

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

  1. L27
    split
06Fix variables and assumptionsL28–29

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

  1. L28
    intro j
  2. L29
    intro hj
07Establish htL30–33

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

  1. L30
    have ht : ∃ t. BetaAt(x,x1,j,t) ∧ PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)Definitions: BetaAt(x,x1,j,t)PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)Original native command in the exact edition
  2. L31
    specialize hr_witness_witness_witness_left (j)
  3. L32
    apply hr_witness_witness_witness_left
  4. L33
    exact hj
08Separate the logical casesL34–35

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

  1. L34
    cases ht
  2. L35
    cases ht_witness
09Construct an explicit witnessL36–36

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

  1. L36
    exists x3
10Separate the logical casesL37–37

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

  1. L37
    split
11Use earlier factsL38–47

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

  1. L38
    exact ht_witness_left
  2. L39
    specialize polynomial_diagonal_left_prefix_transport (ab)
  3. L40
    specialize polynomial_diagonal_left_prefix_transport (ac)
  4. L41
    specialize polynomial_diagonal_left_prefix_transport (L)
  5. L42
    specialize polynomial_diagonal_left_prefix_transport (AB)
  6. L43
    specialize polynomial_diagonal_left_prefix_transport (AC)
  7. L44
    specialize polynomial_diagonal_left_prefix_transport (K)
  8. L45
    specialize polynomial_diagonal_left_prefix_transport (bb)
  9. L46
    specialize polynomial_diagonal_left_prefix_transport (bc)
  10. L47
    specialize polynomial_diagonal_left_prefix_transport (M)
12Use earlier factsL48–57

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

  1. L48
    specialize polynomial_diagonal_left_prefix_transport (N)
  2. L49
    specialize polynomial_diagonal_left_prefix_transport (i)
  3. L50
    specialize polynomial_diagonal_left_prefix_transport (j)
  4. L51
    specialize polynomial_diagonal_left_prefix_transport (x3)
  5. L52
    apply polynomial_diagonal_left_prefix_transport
  6. L53
    exact hl
  7. L54
    exact hk
  8. L55
    exact he
  9. L56
    specialize lt_of_lt_of_le (j)
  10. L57
    specialize lt_of_lt_of_le (S i)
13Use earlier factsL58–62

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

  1. L58
    specialize lt_of_lt_of_le (N)
  2. L59
    apply lt_of_lt_of_le
  3. L60
    exact hj
  4. L61
    exact hi
  5. L62
    exact ht_witness_right
14Separate the logical casesL63–63

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

  1. L63
    split
15Use earlier factsL64–65

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

  1. L64
    exact hr_witness_witness_witness_right_left
  2. L65
    exact hr_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro AB
  6. 0006intro AC
  7. 0007intro K
  8. 0008intro bb
  9. 0009intro bc
  10. 0010intro M
  11. 0011intro N
  12. 0012intro i
  13. 0013intro r
  14. 0014intro hl
  15. 0015intro hk
  16. 0016intro he
  17. 0017intro hi
  18. 0018intro hr
  19. 0019cases hr
  20. 0020cases hr_witness
  21. 0021cases hr_witness_witness
  22. 0022cases hr_witness_witness_witness
  23. 0023cases hr_witness_witness_witness_right
  24. 0024exists x
  25. 0025exists x1
  26. 0026exists x2
  27. 0027split
  28. 0028intro j
  29. 0029intro hj
  30. 0030have ht : ∃ t. BetaAt(x,x1,j,t) ∧ PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)
  31. 0031specialize hr_witness_witness_witness_left (j)
  32. 0032apply hr_witness_witness_witness_left
  33. 0033exact hj
  34. 0034cases ht
  35. 0035cases ht_witness
  36. 0036exists x3
  37. 0037split
  38. 0038exact ht_witness_left
  39. 0039specialize polynomial_diagonal_left_prefix_transport (ab)
  40. 0040specialize polynomial_diagonal_left_prefix_transport (ac)
  41. 0041specialize polynomial_diagonal_left_prefix_transport (L)
  42. 0042specialize polynomial_diagonal_left_prefix_transport (AB)
  43. 0043specialize polynomial_diagonal_left_prefix_transport (AC)
  44. 0044specialize polynomial_diagonal_left_prefix_transport (K)
  45. 0045specialize polynomial_diagonal_left_prefix_transport (bb)
  46. 0046specialize polynomial_diagonal_left_prefix_transport (bc)
  47. 0047specialize polynomial_diagonal_left_prefix_transport (M)
  48. 0048specialize polynomial_diagonal_left_prefix_transport (N)
  49. 0049specialize polynomial_diagonal_left_prefix_transport (i)
  50. 0050specialize polynomial_diagonal_left_prefix_transport (j)
  51. 0051specialize polynomial_diagonal_left_prefix_transport (x3)
  52. 0052apply polynomial_diagonal_left_prefix_transport
  53. 0053exact hl
  54. 0054exact hk
  55. 0055exact he
  56. 0056specialize lt_of_lt_of_le (j)
  57. 0057specialize lt_of_lt_of_le (S i)
  58. 0058specialize lt_of_lt_of_le (N)
  59. 0059apply lt_of_lt_of_le
  60. 0060exact hj
  61. 0061exact hi
  62. 0062exact ht_witness_right
  63. 0063split
  64. 0064exact hr_witness_witness_witness_right_left
  65. 0065exact hr_witness_witness_witness_right_right