PX0066

prime_field_convolution_coefficient_left_padding_left

Construct an actual padded antidiagonal table and actual sum trace, proving the shifted coefficient has the same canonical residue without assuming an equality of sums.

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. ∀ bb. ∀ bc. ∀ M. ∀ AB. ∀ AC. ∀ t. ∀ i. ∀ r. PolynomialLeftPad(ab,ac,L,t,AB,AC) → FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) → FpConvolutionCoefficient(p,AB,AC,t + L,bb,bc,M,t + i,r)

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

Definition DAG

PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l) · 1FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) · 2PolynomialLeftPad(b,c,L,t,d,e) · 2Sum(b,c,l,z) · 1

Actual proof prerequisites

polynomial_diagonal_prefix_exists · checked external prerequisitebeta_sum_exists · checked external prerequisitepolynomial_diagonal_left_padding_leftpolynomial_left_pad_natural_sum_invariant
Original expanded first-order statement 
forall p ab ac L bb bc M AB AC t i r. (((forall pfp_repeat_index_coefficient_padding_leftzeros. (exists pfa_gap_coefficient_padding_leftzerosindex. pfa_gap_coefficient_padding_leftzerosindex + S (pfp_repeat_index_coefficient_padding_leftzeros) = (t)) -> (((exists ff_h_pfp_coefficient_padding_leftzerosentry. ff_h_pfp_coefficient_padding_leftzerosentry + S (0) = S ((S (pfp_repeat_index_coefficient_padding_leftzeros)) * AC)) /\ exists ff_q_pfp_coefficient_padding_leftzerosentry. AB = ff_q_pfp_coefficient_padding_leftzerosentry * S ((S (pfp_repeat_index_coefficient_padding_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_coefficient_padding_left pfrep_value_coefficient_padding_left. (exists pfa_gap_coefficient_padding_leftbound. pfa_gap_coefficient_padding_leftbound + S (pfrep_index_coefficient_padding_left) = (L)) -> (((exists ff_h_pfp_coefficient_padding_leftinput. ff_h_pfp_coefficient_padding_leftinput + S (pfrep_value_coefficient_padding_left) = S ((S (pfrep_index_coefficient_padding_left)) * ac)) /\ exists ff_q_pfp_coefficient_padding_leftinput. ab = ff_q_pfp_coefficient_padding_leftinput * S ((S (pfrep_index_coefficient_padding_left)) * ac) + (pfrep_value_coefficient_padding_left))) -> (((exists ff_h_pfp_coefficient_padding_leftoutput. ff_h_pfp_coefficient_padding_leftoutput + S (pfrep_value_coefficient_padding_left) = S ((S ((t)+pfrep_index_coefficient_padding_left)) * AC)) /\ exists ff_q_pfp_coefficient_padding_leftoutput. AB = ff_q_pfp_coefficient_padding_leftoutput * S ((S ((t)+pfrep_index_coefficient_padding_left)) * AC) + (pfrep_value_coefficient_padding_left))))))) -> (exists pfc_terms_code_coefficient_original_left pfc_terms_scale_coefficient_original_left pfc_natural_sum_coefficient_original_left. ((forall pfc_index_coefficient_original_leftdiagonal. (exists pfa_gap_coefficient_original_leftdiagonalbound. pfa_gap_coefficient_original_leftdiagonalbound + S (pfc_index_coefficient_original_leftdiagonal) = (S (i))) -> exists pfc_value_coefficient_original_leftdiagonal. ((((exists ff_h_pfp_coefficient_original_leftdiagonalentry. ff_h_pfp_coefficient_original_leftdiagonalentry + S (pfc_value_coefficient_original_leftdiagonal) = S ((S (pfc_index_coefficient_original_leftdiagonal)) * pfc_terms_scale_coefficient_original_left)) /\ exists ff_q_pfp_coefficient_original_leftdiagonalentry. pfc_terms_code_coefficient_original_left = ff_q_pfp_coefficient_original_leftdiagonalentry * S ((S (pfc_index_coefficient_original_leftdiagonal)) * pfc_terms_scale_coefficient_original_left) + (pfc_value_coefficient_original_leftdiagonal))) /\ ((exists pfc_complement_coefficient_original_leftdiagonalterm pfc_left_coefficient_original_leftdiagonalterm pfc_right_coefficient_original_leftdiagonalterm. (((pfc_index_coefficient_original_leftdiagonal)+pfc_complement_coefficient_original_leftdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_original_leftdiagonaltermleftinside. pfa_gap_coefficient_original_leftdiagonaltermleftinside + S (pfc_index_coefficient_original_leftdiagonal) = (L)) /\ ((((exists ff_h_pfp_coefficient_original_leftdiagonaltermleftentry. ff_h_pfp_coefficient_original_leftdiagonaltermleftentry + S (pfc_left_coefficient_original_leftdiagonalterm) = S ((S (pfc_index_coefficient_original_leftdiagonal)) * ac)) /\ exists ff_q_pfp_coefficient_original_leftdiagonaltermleftentry. ab = ff_q_pfp_coefficient_original_leftdiagonaltermleftentry * S ((S (pfc_index_coefficient_original_leftdiagonal)) * ac) + (pfc_left_coefficient_original_leftdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_original_leftdiagonaltermleftoutside. pfc_gap_coefficient_original_leftdiagonaltermleftoutside+(L)=(pfc_index_coefficient_original_leftdiagonal)) /\ (((pfc_left_coefficient_original_leftdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_original_leftdiagonaltermrightinside. pfa_gap_coefficient_original_leftdiagonaltermrightinside + S (pfc_complement_coefficient_original_leftdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_coefficient_original_leftdiagonaltermrightentry. ff_h_pfp_coefficient_original_leftdiagonaltermrightentry + S (pfc_right_coefficient_original_leftdiagonalterm) = S ((S (pfc_complement_coefficient_original_leftdiagonalterm)) * bc)) /\ exists ff_q_pfp_coefficient_original_leftdiagonaltermrightentry. bb = ff_q_pfp_coefficient_original_leftdiagonaltermrightentry * S ((S (pfc_complement_coefficient_original_leftdiagonalterm)) * bc) + (pfc_right_coefficient_original_leftdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_original_leftdiagonaltermrightoutside. pfc_gap_coefficient_original_leftdiagonaltermrightoutside+(M)=(pfc_complement_coefficient_original_leftdiagonalterm)) /\ (((pfc_right_coefficient_original_leftdiagonalterm)=0))))) /\ (((pfc_value_coefficient_original_leftdiagonal)=pfc_left_coefficient_original_leftdiagonalterm*pfc_right_coefficient_original_leftdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_original_leftsum fs_v_pfc_coefficient_original_leftsum. ((((exists fs_h_pfc_coefficient_original_leftsum_body_start. fs_h_pfc_coefficient_original_leftsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_original_leftsum)) /\ exists fs_q_pfc_coefficient_original_leftsum_body_start. fs_u_pfc_coefficient_original_leftsum = fs_q_pfc_coefficient_original_leftsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_original_leftsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_original_leftsum_body_terminal. fs_h_pfc_coefficient_original_leftsum_body_terminal + S (pfc_natural_sum_coefficient_original_left) = S ((S (S (i))) * fs_v_pfc_coefficient_original_leftsum)) /\ exists fs_q_pfc_coefficient_original_leftsum_body_terminal. fs_u_pfc_coefficient_original_leftsum = fs_q_pfc_coefficient_original_leftsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_original_leftsum) + (pfc_natural_sum_coefficient_original_left))) /\ forall fs_i_pfc_coefficient_original_leftsum_body_steps. (exists fs_lt_pfc_coefficient_original_leftsum_body_steps_bound. fs_lt_pfc_coefficient_original_leftsum_body_steps_bound + S fs_i_pfc_coefficient_original_leftsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_original_leftsum_body_steps fs_r_pfc_coefficient_original_leftsum_body_steps fs_s_pfc_coefficient_original_leftsum_body_steps. ((((exists fs_h_pfc_coefficient_original_leftsum_body_steps_summand. fs_h_pfc_coefficient_original_leftsum_body_steps_summand + S (fs_a_pfc_coefficient_original_leftsum_body_steps) = S ((S (fs_i_pfc_coefficient_original_leftsum_body_steps)) * pfc_terms_scale_coefficient_original_left)) /\ exists fs_q_pfc_coefficient_original_leftsum_body_steps_summand. pfc_terms_code_coefficient_original_left = fs_q_pfc_coefficient_original_leftsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_original_leftsum_body_steps)) * pfc_terms_scale_coefficient_original_left) + (fs_a_pfc_coefficient_original_leftsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_original_leftsum_body_steps_partial. fs_h_pfc_coefficient_original_leftsum_body_steps_partial + S (fs_r_pfc_coefficient_original_leftsum_body_steps) = S ((S (fs_i_pfc_coefficient_original_leftsum_body_steps)) * fs_v_pfc_coefficient_original_leftsum)) /\ exists fs_q_pfc_coefficient_original_leftsum_body_steps_partial. fs_u_pfc_coefficient_original_leftsum = fs_q_pfc_coefficient_original_leftsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_original_leftsum_body_steps)) * fs_v_pfc_coefficient_original_leftsum) + (fs_r_pfc_coefficient_original_leftsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_original_leftsum_body_steps_successor. fs_h_pfc_coefficient_original_leftsum_body_steps_successor + S (fs_s_pfc_coefficient_original_leftsum_body_steps) = S ((S (S fs_i_pfc_coefficient_original_leftsum_body_steps)) * fs_v_pfc_coefficient_original_leftsum)) /\ exists fs_q_pfc_coefficient_original_leftsum_body_steps_successor. fs_u_pfc_coefficient_original_leftsum = fs_q_pfc_coefficient_original_leftsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_original_leftsum_body_steps)) * fs_v_pfc_coefficient_original_leftsum) + (fs_s_pfc_coefficient_original_leftsum_body_steps))) /\ fs_s_pfc_coefficient_original_leftsum_body_steps = fs_r_pfc_coefficient_original_leftsum_body_steps + fs_a_pfc_coefficient_original_leftsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_original_leftresiduebound. pfa_gap_coefficient_original_leftresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_coefficient_original_leftresiduecongruence pfa_offset_right_coefficient_original_leftresiduecongruence. (pfc_natural_sum_coefficient_original_left) + (p) * pfa_offset_left_coefficient_original_leftresiduecongruence = (r) + (p) * pfa_offset_right_coefficient_original_leftresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_shifted_left pfc_terms_scale_coefficient_shifted_left pfc_natural_sum_coefficient_shifted_left. ((forall pfc_index_coefficient_shifted_leftdiagonal. (exists pfa_gap_coefficient_shifted_leftdiagonalbound. pfa_gap_coefficient_shifted_leftdiagonalbound + S (pfc_index_coefficient_shifted_leftdiagonal) = (S (t+i))) -> exists pfc_value_coefficient_shifted_leftdiagonal. ((((exists ff_h_pfp_coefficient_shifted_leftdiagonalentry. ff_h_pfp_coefficient_shifted_leftdiagonalentry + S (pfc_value_coefficient_shifted_leftdiagonal) = S ((S (pfc_index_coefficient_shifted_leftdiagonal)) * pfc_terms_scale_coefficient_shifted_left)) /\ exists ff_q_pfp_coefficient_shifted_leftdiagonalentry. pfc_terms_code_coefficient_shifted_left = ff_q_pfp_coefficient_shifted_leftdiagonalentry * S ((S (pfc_index_coefficient_shifted_leftdiagonal)) * pfc_terms_scale_coefficient_shifted_left) + (pfc_value_coefficient_shifted_leftdiagonal))) /\ ((exists pfc_complement_coefficient_shifted_leftdiagonalterm pfc_left_coefficient_shifted_leftdiagonalterm pfc_right_coefficient_shifted_leftdiagonalterm. (((pfc_index_coefficient_shifted_leftdiagonal)+pfc_complement_coefficient_shifted_leftdiagonalterm=(t+i)) /\ ((((((exists pfa_gap_coefficient_shifted_leftdiagonaltermleftinside. pfa_gap_coefficient_shifted_leftdiagonaltermleftinside + S (pfc_index_coefficient_shifted_leftdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_coefficient_shifted_leftdiagonaltermleftentry. ff_h_pfp_coefficient_shifted_leftdiagonaltermleftentry + S (pfc_left_coefficient_shifted_leftdiagonalterm) = S ((S (pfc_index_coefficient_shifted_leftdiagonal)) * AC)) /\ exists ff_q_pfp_coefficient_shifted_leftdiagonaltermleftentry. AB = ff_q_pfp_coefficient_shifted_leftdiagonaltermleftentry * S ((S (pfc_index_coefficient_shifted_leftdiagonal)) * AC) + (pfc_left_coefficient_shifted_leftdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_shifted_leftdiagonaltermleftoutside. pfc_gap_coefficient_shifted_leftdiagonaltermleftoutside+(t+L)=(pfc_index_coefficient_shifted_leftdiagonal)) /\ (((pfc_left_coefficient_shifted_leftdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_shifted_leftdiagonaltermrightinside. pfa_gap_coefficient_shifted_leftdiagonaltermrightinside + S (pfc_complement_coefficient_shifted_leftdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_coefficient_shifted_leftdiagonaltermrightentry. ff_h_pfp_coefficient_shifted_leftdiagonaltermrightentry + S (pfc_right_coefficient_shifted_leftdiagonalterm) = S ((S (pfc_complement_coefficient_shifted_leftdiagonalterm)) * bc)) /\ exists ff_q_pfp_coefficient_shifted_leftdiagonaltermrightentry. bb = ff_q_pfp_coefficient_shifted_leftdiagonaltermrightentry * S ((S (pfc_complement_coefficient_shifted_leftdiagonalterm)) * bc) + (pfc_right_coefficient_shifted_leftdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_shifted_leftdiagonaltermrightoutside. pfc_gap_coefficient_shifted_leftdiagonaltermrightoutside+(M)=(pfc_complement_coefficient_shifted_leftdiagonalterm)) /\ (((pfc_right_coefficient_shifted_leftdiagonalterm)=0))))) /\ (((pfc_value_coefficient_shifted_leftdiagonal)=pfc_left_coefficient_shifted_leftdiagonalterm*pfc_right_coefficient_shifted_leftdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_shifted_leftsum fs_v_pfc_coefficient_shifted_leftsum. ((((exists fs_h_pfc_coefficient_shifted_leftsum_body_start. fs_h_pfc_coefficient_shifted_leftsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_shifted_leftsum)) /\ exists fs_q_pfc_coefficient_shifted_leftsum_body_start. fs_u_pfc_coefficient_shifted_leftsum = fs_q_pfc_coefficient_shifted_leftsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_shifted_leftsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_shifted_leftsum_body_terminal. fs_h_pfc_coefficient_shifted_leftsum_body_terminal + S (pfc_natural_sum_coefficient_shifted_left) = S ((S (S (t+i))) * fs_v_pfc_coefficient_shifted_leftsum)) /\ exists fs_q_pfc_coefficient_shifted_leftsum_body_terminal. fs_u_pfc_coefficient_shifted_leftsum = fs_q_pfc_coefficient_shifted_leftsum_body_terminal * S ((S (S (t+i))) * fs_v_pfc_coefficient_shifted_leftsum) + (pfc_natural_sum_coefficient_shifted_left))) /\ forall fs_i_pfc_coefficient_shifted_leftsum_body_steps. (exists fs_lt_pfc_coefficient_shifted_leftsum_body_steps_bound. fs_lt_pfc_coefficient_shifted_leftsum_body_steps_bound + S fs_i_pfc_coefficient_shifted_leftsum_body_steps = S (t+i)) -> exists fs_a_pfc_coefficient_shifted_leftsum_body_steps fs_r_pfc_coefficient_shifted_leftsum_body_steps fs_s_pfc_coefficient_shifted_leftsum_body_steps. ((((exists fs_h_pfc_coefficient_shifted_leftsum_body_steps_summand. fs_h_pfc_coefficient_shifted_leftsum_body_steps_summand + S (fs_a_pfc_coefficient_shifted_leftsum_body_steps) = S ((S (fs_i_pfc_coefficient_shifted_leftsum_body_steps)) * pfc_terms_scale_coefficient_shifted_left)) /\ exists fs_q_pfc_coefficient_shifted_leftsum_body_steps_summand. pfc_terms_code_coefficient_shifted_left = fs_q_pfc_coefficient_shifted_leftsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_shifted_leftsum_body_steps)) * pfc_terms_scale_coefficient_shifted_left) + (fs_a_pfc_coefficient_shifted_leftsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_shifted_leftsum_body_steps_partial. fs_h_pfc_coefficient_shifted_leftsum_body_steps_partial + S (fs_r_pfc_coefficient_shifted_leftsum_body_steps) = S ((S (fs_i_pfc_coefficient_shifted_leftsum_body_steps)) * fs_v_pfc_coefficient_shifted_leftsum)) /\ exists fs_q_pfc_coefficient_shifted_leftsum_body_steps_partial. fs_u_pfc_coefficient_shifted_leftsum = fs_q_pfc_coefficient_shifted_leftsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_shifted_leftsum_body_steps)) * fs_v_pfc_coefficient_shifted_leftsum) + (fs_r_pfc_coefficient_shifted_leftsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_shifted_leftsum_body_steps_successor. fs_h_pfc_coefficient_shifted_leftsum_body_steps_successor + S (fs_s_pfc_coefficient_shifted_leftsum_body_steps) = S ((S (S fs_i_pfc_coefficient_shifted_leftsum_body_steps)) * fs_v_pfc_coefficient_shifted_leftsum)) /\ exists fs_q_pfc_coefficient_shifted_leftsum_body_steps_successor. fs_u_pfc_coefficient_shifted_leftsum = fs_q_pfc_coefficient_shifted_leftsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_shifted_leftsum_body_steps)) * fs_v_pfc_coefficient_shifted_leftsum) + (fs_s_pfc_coefficient_shifted_leftsum_body_steps))) /\ fs_s_pfc_coefficient_shifted_leftsum_body_steps = fs_r_pfc_coefficient_shifted_leftsum_body_steps + fs_a_pfc_coefficient_shifted_leftsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_shifted_leftresiduebound. pfa_gap_coefficient_shifted_leftresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_coefficient_shifted_leftresiduecongruence pfa_offset_right_coefficient_shifted_leftresiduecongruence. (pfc_natural_sum_coefficient_shifted_left) + (p) * pfa_offset_left_coefficient_shifted_leftresiduecongruence = (r) + (p) * pfa_offset_right_coefficient_shifted_leftresiduecongruence)))))))))

Complete tactic proof in conservative notation

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

83 script commands · 18 reading checkpoints · 5 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 (2)
polynomial diagonal left padding leftpolynomial left pad natural sum invariant
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 bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro AB
  9. L9
    intro AC
  10. L10
    intro t
02Fix variables and assumptionsL11–14

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

  1. L11
    intro i
  2. L12
    intro r
  3. L13
    intro hpad
  4. L14
    intro hc
03Separate the logical casesL15–19

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

  1. L15
    cases hc
  2. L16
    cases hc_witness
  3. L17
    cases hc_witness_witness
  4. L18
    cases hc_witness_witness_witness
  5. L19
    cases hc_witness_witness_witness_right
04Establish hdL20–28

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

  1. L20
    have hd : ∃ eb. ∃ ec. PolynomialDiagonalPrefix(AB,AC,t + L,bb,bc,M,t + i,eb,ec,S (t + i))Definitions: PolynomialDiagonalPrefix(AB,AC,t + L,bb,bc,M,t + i,eb,ec,S (t + i))Original native command in the exact edition
  2. L21
    specialize polynomial_diagonal_prefix_exists (AB)
  3. L22
    specialize polynomial_diagonal_prefix_exists (AC)
  4. L23
    specialize polynomial_diagonal_prefix_exists (t+L)
  5. L24
    specialize polynomial_diagonal_prefix_exists (bb)
  6. L25
    specialize polynomial_diagonal_prefix_exists (bc)
  7. L26
    specialize polynomial_diagonal_prefix_exists (M)
  8. L27
    specialize polynomial_diagonal_prefix_exists (t+i)
  9. L28
    apply polynomial_diagonal_prefix_exists
05Separate the logical casesL29–30

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

  1. L29
    cases hd
  2. L30
    cases hd_witness
06Establish hsL31–35

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

  1. L31
    have hs : ∃ n. Sum(x3,x4,S (t + i),n)Definitions: Sum(x3,x4,S (t + i),n)Original native command in the exact edition
  2. L32
    specialize beta_sum_exists (x3)
  3. L33
    specialize beta_sum_exists (x4)
  4. L34
    specialize beta_sum_exists (S (t+i))
  5. L35
    apply beta_sum_exists
07Separate the logical casesL36–36

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

  1. L36
    cases hs
08Establish hdataL37–46

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

  1. L37
    have hdata : PolynomialLeftPad(x,x1,S i,t,x3,x4)Definitions: PolynomialLeftPad(x,x1,S i,t,x3,x4)Original native command in the exact edition
  2. L38
    specialize polynomial_diagonal_left_padding_left (ab)
  3. L39
    specialize polynomial_diagonal_left_padding_left (ac)
  4. L40
    specialize polynomial_diagonal_left_padding_left (L)
  5. L41
    specialize polynomial_diagonal_left_padding_left (bb)
  6. L42
    specialize polynomial_diagonal_left_padding_left (bc)
  7. L43
    specialize polynomial_diagonal_left_padding_left (M)
  8. L44
    specialize polynomial_diagonal_left_padding_left (AB)
  9. L45
    specialize polynomial_diagonal_left_padding_left (AC)
  10. L46
    specialize polynomial_diagonal_left_padding_left (t)
09Use earlier factsL47–55

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

  1. L47
    specialize polynomial_diagonal_left_padding_left (i)
  2. L48
    specialize polynomial_diagonal_left_padding_left (x)
  3. L49
    specialize polynomial_diagonal_left_padding_left (x1)
  4. L50
    specialize polynomial_diagonal_left_padding_left (x3)
  5. L51
    specialize polynomial_diagonal_left_padding_left (x4)
  6. L52
    apply polynomial_diagonal_left_padding_left
  7. L53
    exact hpad
  8. L54
    exact hc_witness_witness_witness_left
  9. L55
    exact hd_witness_witness
10Establish heqL56–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial left pad natural sum invariant.

  1. L56
    have heq : x5=x2
  2. L57
    specialize polynomial_left_pad_natural_sum_invariant (x)
  3. L58
    specialize polynomial_left_pad_natural_sum_invariant (x1)
  4. L59
    specialize polynomial_left_pad_natural_sum_invariant (x3)
  5. L60
    specialize polynomial_left_pad_natural_sum_invariant (x4)
  6. L61
    specialize polynomial_left_pad_natural_sum_invariant (t)
  7. L62
    specialize polynomial_left_pad_natural_sum_invariant (S i)
  8. L63
    specialize polynomial_left_pad_natural_sum_invariant (x2)
  9. L64
    specialize polynomial_left_pad_natural_sum_invariant (x5)
  10. L65
    apply polynomial_left_pad_natural_sum_invariant
11Use earlier factsL66–67

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

  1. L66
    exact hdata
  2. L67
    exact hc_witness_witness_witness_right_left
12Establish hlengthL68–73

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

  1. L68
    have hlength : t+S i=S (t+i)
  2. L69
    simp
  3. L70
    rewrite hlength
  4. L71
    rewrite hlength
  5. L72
    rewrite hlength
  6. L73
    exact hs_witness
13Construct an explicit witnessL74–76

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

  1. L74
    exists x3
  2. L75
    exists x4
  3. L76
    exists x2
14Separate the logical casesL77–77

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

  1. L77
    split
15Use earlier factsL78–78

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

  1. L78
    exact hd_witness_witness
16Separate the logical casesL79–79

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

  1. L79
    split
17Calculate and transport equalitiesL80–81

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

  1. L80
    rewrite heq at hs_witness
  2. L81
    rewrite heq at hs_witness
18Use earlier factsL82–83

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

  1. L82
    exact hs_witness
  2. L83
    exact hc_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 83 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro AB
  9. 0009intro AC
  10. 0010intro t
  11. 0011intro i
  12. 0012intro r
  13. 0013intro hpad
  14. 0014intro hc
  15. 0015cases hc
  16. 0016cases hc_witness
  17. 0017cases hc_witness_witness
  18. 0018cases hc_witness_witness_witness
  19. 0019cases hc_witness_witness_witness_right
  20. 0020have hd : ∃ eb. ∃ ec. PolynomialDiagonalPrefix(AB,AC,t + L,bb,bc,M,t + i,eb,ec,S (t + i))
  21. 0021specialize polynomial_diagonal_prefix_exists (AB)
  22. 0022specialize polynomial_diagonal_prefix_exists (AC)
  23. 0023specialize polynomial_diagonal_prefix_exists (t+L)
  24. 0024specialize polynomial_diagonal_prefix_exists (bb)
  25. 0025specialize polynomial_diagonal_prefix_exists (bc)
  26. 0026specialize polynomial_diagonal_prefix_exists (M)
  27. 0027specialize polynomial_diagonal_prefix_exists (t+i)
  28. 0028apply polynomial_diagonal_prefix_exists
  29. 0029cases hd
  30. 0030cases hd_witness
  31. 0031have hs : ∃ n. Sum(x3,x4,S (t + i),n)
  32. 0032specialize beta_sum_exists (x3)
  33. 0033specialize beta_sum_exists (x4)
  34. 0034specialize beta_sum_exists (S (t+i))
  35. 0035apply beta_sum_exists
  36. 0036cases hs
  37. 0037have hdata : PolynomialLeftPad(x,x1,S i,t,x3,x4)
  38. 0038specialize polynomial_diagonal_left_padding_left (ab)
  39. 0039specialize polynomial_diagonal_left_padding_left (ac)
  40. 0040specialize polynomial_diagonal_left_padding_left (L)
  41. 0041specialize polynomial_diagonal_left_padding_left (bb)
  42. 0042specialize polynomial_diagonal_left_padding_left (bc)
  43. 0043specialize polynomial_diagonal_left_padding_left (M)
  44. 0044specialize polynomial_diagonal_left_padding_left (AB)
  45. 0045specialize polynomial_diagonal_left_padding_left (AC)
  46. 0046specialize polynomial_diagonal_left_padding_left (t)
  47. 0047specialize polynomial_diagonal_left_padding_left (i)
  48. 0048specialize polynomial_diagonal_left_padding_left (x)
  49. 0049specialize polynomial_diagonal_left_padding_left (x1)
  50. 0050specialize polynomial_diagonal_left_padding_left (x3)
  51. 0051specialize polynomial_diagonal_left_padding_left (x4)
  52. 0052apply polynomial_diagonal_left_padding_left
  53. 0053exact hpad
  54. 0054exact hc_witness_witness_witness_left
  55. 0055exact hd_witness_witness
  56. 0056have heq : x5=x2
  57. 0057specialize polynomial_left_pad_natural_sum_invariant (x)
  58. 0058specialize polynomial_left_pad_natural_sum_invariant (x1)
  59. 0059specialize polynomial_left_pad_natural_sum_invariant (x3)
  60. 0060specialize polynomial_left_pad_natural_sum_invariant (x4)
  61. 0061specialize polynomial_left_pad_natural_sum_invariant (t)
  62. 0062specialize polynomial_left_pad_natural_sum_invariant (S i)
  63. 0063specialize polynomial_left_pad_natural_sum_invariant (x2)
  64. 0064specialize polynomial_left_pad_natural_sum_invariant (x5)
  65. 0065apply polynomial_left_pad_natural_sum_invariant
  66. 0066exact hdata
  67. 0067exact hc_witness_witness_witness_right_left
  68. 0068have hlength : t+S i=S (t+i)
  69. 0069simp
  70. 0070rewrite hlength
  71. 0071rewrite hlength
  72. 0072rewrite hlength
  73. 0073exact hs_witness
  74. 0074exists x3
  75. 0075exists x4
  76. 0076exists x2
  77. 0077split
  78. 0078exact hd_witness_witness
  79. 0079split
  80. 0080rewrite heq at hs_witness
  81. 0081rewrite heq at hs_witness
  82. 0082exact hs_witness
  83. 0083exact hc_witness_witness_witness_right_right