PX0067

prime_field_convolution_coefficient_left_padding_right

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

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1PolynomialDiagonalPrefix(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) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 1Sum(b,c,l,z) · 1

Actual proof prerequisites

polynomial_diagonal_prefix_exists · checked external prerequisitebeta_sum_exists · checked external prerequisitepolynomial_diagonal_left_padding_rightpolynomial_zero_tail_natural_sum_invariantadd_succ_left · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall p ab ac L bb bc M BB BC t i r. (((forall pfp_repeat_index_coefficient_padding_rightzeros. (exists pfa_gap_coefficient_padding_rightzerosindex. pfa_gap_coefficient_padding_rightzerosindex + S (pfp_repeat_index_coefficient_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_coefficient_padding_rightzerosentry. ff_h_pfp_coefficient_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_coefficient_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_coefficient_padding_rightzerosentry. BB = ff_q_pfp_coefficient_padding_rightzerosentry * S ((S (pfp_repeat_index_coefficient_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_coefficient_padding_right pfrep_value_coefficient_padding_right. (exists pfa_gap_coefficient_padding_rightbound. pfa_gap_coefficient_padding_rightbound + S (pfrep_index_coefficient_padding_right) = (M)) -> (((exists ff_h_pfp_coefficient_padding_rightinput. ff_h_pfp_coefficient_padding_rightinput + S (pfrep_value_coefficient_padding_right) = S ((S (pfrep_index_coefficient_padding_right)) * bc)) /\ exists ff_q_pfp_coefficient_padding_rightinput. bb = ff_q_pfp_coefficient_padding_rightinput * S ((S (pfrep_index_coefficient_padding_right)) * bc) + (pfrep_value_coefficient_padding_right))) -> (((exists ff_h_pfp_coefficient_padding_rightoutput. ff_h_pfp_coefficient_padding_rightoutput + S (pfrep_value_coefficient_padding_right) = S ((S ((t)+pfrep_index_coefficient_padding_right)) * BC)) /\ exists ff_q_pfp_coefficient_padding_rightoutput. BB = ff_q_pfp_coefficient_padding_rightoutput * S ((S ((t)+pfrep_index_coefficient_padding_right)) * BC) + (pfrep_value_coefficient_padding_right))))))) -> (exists pfc_terms_code_coefficient_original_right pfc_terms_scale_coefficient_original_right pfc_natural_sum_coefficient_original_right. ((forall pfc_index_coefficient_original_rightdiagonal. (exists pfa_gap_coefficient_original_rightdiagonalbound. pfa_gap_coefficient_original_rightdiagonalbound + S (pfc_index_coefficient_original_rightdiagonal) = (S (i))) -> exists pfc_value_coefficient_original_rightdiagonal. ((((exists ff_h_pfp_coefficient_original_rightdiagonalentry. ff_h_pfp_coefficient_original_rightdiagonalentry + S (pfc_value_coefficient_original_rightdiagonal) = S ((S (pfc_index_coefficient_original_rightdiagonal)) * pfc_terms_scale_coefficient_original_right)) /\ exists ff_q_pfp_coefficient_original_rightdiagonalentry. pfc_terms_code_coefficient_original_right = ff_q_pfp_coefficient_original_rightdiagonalentry * S ((S (pfc_index_coefficient_original_rightdiagonal)) * pfc_terms_scale_coefficient_original_right) + (pfc_value_coefficient_original_rightdiagonal))) /\ ((exists pfc_complement_coefficient_original_rightdiagonalterm pfc_left_coefficient_original_rightdiagonalterm pfc_right_coefficient_original_rightdiagonalterm. (((pfc_index_coefficient_original_rightdiagonal)+pfc_complement_coefficient_original_rightdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_original_rightdiagonaltermleftinside. pfa_gap_coefficient_original_rightdiagonaltermleftinside + S (pfc_index_coefficient_original_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_coefficient_original_rightdiagonaltermleftentry. ff_h_pfp_coefficient_original_rightdiagonaltermleftentry + S (pfc_left_coefficient_original_rightdiagonalterm) = S ((S (pfc_index_coefficient_original_rightdiagonal)) * ac)) /\ exists ff_q_pfp_coefficient_original_rightdiagonaltermleftentry. ab = ff_q_pfp_coefficient_original_rightdiagonaltermleftentry * S ((S (pfc_index_coefficient_original_rightdiagonal)) * ac) + (pfc_left_coefficient_original_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_original_rightdiagonaltermleftoutside. pfc_gap_coefficient_original_rightdiagonaltermleftoutside+(L)=(pfc_index_coefficient_original_rightdiagonal)) /\ (((pfc_left_coefficient_original_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_original_rightdiagonaltermrightinside. pfa_gap_coefficient_original_rightdiagonaltermrightinside + S (pfc_complement_coefficient_original_rightdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_coefficient_original_rightdiagonaltermrightentry. ff_h_pfp_coefficient_original_rightdiagonaltermrightentry + S (pfc_right_coefficient_original_rightdiagonalterm) = S ((S (pfc_complement_coefficient_original_rightdiagonalterm)) * bc)) /\ exists ff_q_pfp_coefficient_original_rightdiagonaltermrightentry. bb = ff_q_pfp_coefficient_original_rightdiagonaltermrightentry * S ((S (pfc_complement_coefficient_original_rightdiagonalterm)) * bc) + (pfc_right_coefficient_original_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_original_rightdiagonaltermrightoutside. pfc_gap_coefficient_original_rightdiagonaltermrightoutside+(M)=(pfc_complement_coefficient_original_rightdiagonalterm)) /\ (((pfc_right_coefficient_original_rightdiagonalterm)=0))))) /\ (((pfc_value_coefficient_original_rightdiagonal)=pfc_left_coefficient_original_rightdiagonalterm*pfc_right_coefficient_original_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_original_rightsum fs_v_pfc_coefficient_original_rightsum. ((((exists fs_h_pfc_coefficient_original_rightsum_body_start. fs_h_pfc_coefficient_original_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_start. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_original_rightsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_original_rightsum_body_terminal. fs_h_pfc_coefficient_original_rightsum_body_terminal + S (pfc_natural_sum_coefficient_original_right) = S ((S (S (i))) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_terminal. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_original_rightsum) + (pfc_natural_sum_coefficient_original_right))) /\ forall fs_i_pfc_coefficient_original_rightsum_body_steps. (exists fs_lt_pfc_coefficient_original_rightsum_body_steps_bound. fs_lt_pfc_coefficient_original_rightsum_body_steps_bound + S fs_i_pfc_coefficient_original_rightsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_original_rightsum_body_steps fs_r_pfc_coefficient_original_rightsum_body_steps fs_s_pfc_coefficient_original_rightsum_body_steps. ((((exists fs_h_pfc_coefficient_original_rightsum_body_steps_summand. fs_h_pfc_coefficient_original_rightsum_body_steps_summand + S (fs_a_pfc_coefficient_original_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * pfc_terms_scale_coefficient_original_right)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_steps_summand. pfc_terms_code_coefficient_original_right = fs_q_pfc_coefficient_original_rightsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * pfc_terms_scale_coefficient_original_right) + (fs_a_pfc_coefficient_original_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_original_rightsum_body_steps_partial. fs_h_pfc_coefficient_original_rightsum_body_steps_partial + S (fs_r_pfc_coefficient_original_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_steps_partial. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum) + (fs_r_pfc_coefficient_original_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_original_rightsum_body_steps_successor. fs_h_pfc_coefficient_original_rightsum_body_steps_successor + S (fs_s_pfc_coefficient_original_rightsum_body_steps) = S ((S (S fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_steps_successor. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum) + (fs_s_pfc_coefficient_original_rightsum_body_steps))) /\ fs_s_pfc_coefficient_original_rightsum_body_steps = fs_r_pfc_coefficient_original_rightsum_body_steps + fs_a_pfc_coefficient_original_rightsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_original_rightresiduebound. pfa_gap_coefficient_original_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_coefficient_original_rightresiduecongruence pfa_offset_right_coefficient_original_rightresiduecongruence. (pfc_natural_sum_coefficient_original_right) + (p) * pfa_offset_left_coefficient_original_rightresiduecongruence = (r) + (p) * pfa_offset_right_coefficient_original_rightresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_shifted_right pfc_terms_scale_coefficient_shifted_right pfc_natural_sum_coefficient_shifted_right. ((forall pfc_index_coefficient_shifted_rightdiagonal. (exists pfa_gap_coefficient_shifted_rightdiagonalbound. pfa_gap_coefficient_shifted_rightdiagonalbound + S (pfc_index_coefficient_shifted_rightdiagonal) = (S (t+i))) -> exists pfc_value_coefficient_shifted_rightdiagonal. ((((exists ff_h_pfp_coefficient_shifted_rightdiagonalentry. ff_h_pfp_coefficient_shifted_rightdiagonalentry + S (pfc_value_coefficient_shifted_rightdiagonal) = S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * pfc_terms_scale_coefficient_shifted_right)) /\ exists ff_q_pfp_coefficient_shifted_rightdiagonalentry. pfc_terms_code_coefficient_shifted_right = ff_q_pfp_coefficient_shifted_rightdiagonalentry * S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * pfc_terms_scale_coefficient_shifted_right) + (pfc_value_coefficient_shifted_rightdiagonal))) /\ ((exists pfc_complement_coefficient_shifted_rightdiagonalterm pfc_left_coefficient_shifted_rightdiagonalterm pfc_right_coefficient_shifted_rightdiagonalterm. (((pfc_index_coefficient_shifted_rightdiagonal)+pfc_complement_coefficient_shifted_rightdiagonalterm=(t+i)) /\ ((((((exists pfa_gap_coefficient_shifted_rightdiagonaltermleftinside. pfa_gap_coefficient_shifted_rightdiagonaltermleftinside + S (pfc_index_coefficient_shifted_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_coefficient_shifted_rightdiagonaltermleftentry. ff_h_pfp_coefficient_shifted_rightdiagonaltermleftentry + S (pfc_left_coefficient_shifted_rightdiagonalterm) = S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * ac)) /\ exists ff_q_pfp_coefficient_shifted_rightdiagonaltermleftentry. ab = ff_q_pfp_coefficient_shifted_rightdiagonaltermleftentry * S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * ac) + (pfc_left_coefficient_shifted_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_shifted_rightdiagonaltermleftoutside. pfc_gap_coefficient_shifted_rightdiagonaltermleftoutside+(L)=(pfc_index_coefficient_shifted_rightdiagonal)) /\ (((pfc_left_coefficient_shifted_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_shifted_rightdiagonaltermrightinside. pfa_gap_coefficient_shifted_rightdiagonaltermrightinside + S (pfc_complement_coefficient_shifted_rightdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_coefficient_shifted_rightdiagonaltermrightentry. ff_h_pfp_coefficient_shifted_rightdiagonaltermrightentry + S (pfc_right_coefficient_shifted_rightdiagonalterm) = S ((S (pfc_complement_coefficient_shifted_rightdiagonalterm)) * BC)) /\ exists ff_q_pfp_coefficient_shifted_rightdiagonaltermrightentry. BB = ff_q_pfp_coefficient_shifted_rightdiagonaltermrightentry * S ((S (pfc_complement_coefficient_shifted_rightdiagonalterm)) * BC) + (pfc_right_coefficient_shifted_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_shifted_rightdiagonaltermrightoutside. pfc_gap_coefficient_shifted_rightdiagonaltermrightoutside+(t+M)=(pfc_complement_coefficient_shifted_rightdiagonalterm)) /\ (((pfc_right_coefficient_shifted_rightdiagonalterm)=0))))) /\ (((pfc_value_coefficient_shifted_rightdiagonal)=pfc_left_coefficient_shifted_rightdiagonalterm*pfc_right_coefficient_shifted_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_shifted_rightsum fs_v_pfc_coefficient_shifted_rightsum. ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_start. fs_h_pfc_coefficient_shifted_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_start. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_shifted_rightsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_terminal. fs_h_pfc_coefficient_shifted_rightsum_body_terminal + S (pfc_natural_sum_coefficient_shifted_right) = S ((S (S (t+i))) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_terminal. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_terminal * S ((S (S (t+i))) * fs_v_pfc_coefficient_shifted_rightsum) + (pfc_natural_sum_coefficient_shifted_right))) /\ forall fs_i_pfc_coefficient_shifted_rightsum_body_steps. (exists fs_lt_pfc_coefficient_shifted_rightsum_body_steps_bound. fs_lt_pfc_coefficient_shifted_rightsum_body_steps_bound + S fs_i_pfc_coefficient_shifted_rightsum_body_steps = S (t+i)) -> exists fs_a_pfc_coefficient_shifted_rightsum_body_steps fs_r_pfc_coefficient_shifted_rightsum_body_steps fs_s_pfc_coefficient_shifted_rightsum_body_steps. ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_steps_summand. fs_h_pfc_coefficient_shifted_rightsum_body_steps_summand + S (fs_a_pfc_coefficient_shifted_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * pfc_terms_scale_coefficient_shifted_right)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_steps_summand. pfc_terms_code_coefficient_shifted_right = fs_q_pfc_coefficient_shifted_rightsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * pfc_terms_scale_coefficient_shifted_right) + (fs_a_pfc_coefficient_shifted_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_steps_partial. fs_h_pfc_coefficient_shifted_rightsum_body_steps_partial + S (fs_r_pfc_coefficient_shifted_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_steps_partial. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum) + (fs_r_pfc_coefficient_shifted_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_steps_successor. fs_h_pfc_coefficient_shifted_rightsum_body_steps_successor + S (fs_s_pfc_coefficient_shifted_rightsum_body_steps) = S ((S (S fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_steps_successor. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum) + (fs_s_pfc_coefficient_shifted_rightsum_body_steps))) /\ fs_s_pfc_coefficient_shifted_rightsum_body_steps = fs_r_pfc_coefficient_shifted_rightsum_body_steps + fs_a_pfc_coefficient_shifted_rightsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_shifted_rightresiduebound. pfa_gap_coefficient_shifted_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_coefficient_shifted_rightresiduecongruence pfa_offset_right_coefficient_shifted_rightresiduecongruence. (pfc_natural_sum_coefficient_shifted_right) + (p) * pfa_offset_left_coefficient_shifted_rightresiduecongruence = (r) + (p) * pfa_offset_right_coefficient_shifted_rightresiduecongruence)))))))))

Complete tactic proof in conservative notation

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

85 script commands · 20 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 rightpolynomial zero tail 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 BB
  9. L9
    intro BC
  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,L,BB,BC,t + M,t + i,eb,ec,S (t + i))Definitions: PolynomialDiagonalPrefix(ab,ac,L,BB,BC,t + 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 (L)
  5. L24
    specialize polynomial_diagonal_prefix_exists (BB)
  6. L25
    specialize polynomial_diagonal_prefix_exists (BC)
  7. L26
    specialize polynomial_diagonal_prefix_exists (t+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 : BetaPrefixEqual(x,x1,x3,x4,S i) ∧ (∀ y. Lt(y,t) → BetaAt(x3,x4,S i + y,0))Definitions: BetaPrefixEqual(x,x1,x3,x4,S i)Lt(y,t)BetaAt(x3,x4,S i + y,0)Original native command in the exact edition
  2. L38
    specialize polynomial_diagonal_left_padding_right (ab)
  3. L39
    specialize polynomial_diagonal_left_padding_right (ac)
  4. L40
    specialize polynomial_diagonal_left_padding_right (L)
  5. L41
    specialize polynomial_diagonal_left_padding_right (bb)
  6. L42
    specialize polynomial_diagonal_left_padding_right (bc)
  7. L43
    specialize polynomial_diagonal_left_padding_right (M)
  8. L44
    specialize polynomial_diagonal_left_padding_right (BB)
  9. L45
    specialize polynomial_diagonal_left_padding_right (BC)
  10. L46
    specialize polynomial_diagonal_left_padding_right (t)
09Use earlier factsL47–55

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

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

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

  1. L56
    have heq : x5=x2
11Separate the logical casesL57–57

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

  1. L57
    cases hdata
12Use earlier factsL58–67

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

  1. L58
    specialize polynomial_zero_tail_natural_sum_invariant (x)
  2. L59
    specialize polynomial_zero_tail_natural_sum_invariant (x1)
  3. L60
    specialize polynomial_zero_tail_natural_sum_invariant (x3)
  4. L61
    specialize polynomial_zero_tail_natural_sum_invariant (x4)
  5. L62
    specialize polynomial_zero_tail_natural_sum_invariant (S i)
  6. L63
    specialize polynomial_zero_tail_natural_sum_invariant (t)
  7. L64
    specialize polynomial_zero_tail_natural_sum_invariant (x2)
  8. L65
    specialize polynomial_zero_tail_natural_sum_invariant (x5)
  9. L66
    apply polynomial_zero_tail_natural_sum_invariant
  10. L67
    exact hdata_left
13Use earlier factsL68–69

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

  1. L68
    exact hdata_right
  2. L69
    exact hc_witness_witness_witness_right_left
14Establish hlengthL70–75

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

  1. L70
    have hlength : S i+t=S (t+i)
  2. L71
    simp [add_succ_left,add_comm]
  3. L72
    rewrite hlength
  4. L73
    rewrite hlength
  5. L74
    rewrite hlength
  6. L75
    exact hs_witness
15Construct an explicit witnessL76–78

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

  1. L76
    exists x3
  2. L77
    exists x4
  3. L78
    exists x2
16Separate the logical casesL79–79

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

  1. L79
    split
17Use earlier factsL80–80

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

  1. L80
    exact hd_witness_witness
18Separate the logical casesL81–81

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

  1. L81
    split
19Calculate and transport equalitiesL82–83

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

  1. L82
    rewrite heq at hs_witness
  2. L83
    rewrite heq at hs_witness
20Use earlier factsL84–85

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

  1. L84
    exact hs_witness
  2. L85
    exact hc_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 85 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro BB
  9. 0009intro BC
  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,L,BB,BC,t + 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 (L)
  24. 0024specialize polynomial_diagonal_prefix_exists (BB)
  25. 0025specialize polynomial_diagonal_prefix_exists (BC)
  26. 0026specialize polynomial_diagonal_prefix_exists (t+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 : BetaPrefixEqual(x,x1,x3,x4,S i) ∧ (∀ y. Lt(y,t) → BetaAt(x3,x4,S i + y,0))
  38. 0038specialize polynomial_diagonal_left_padding_right (ab)
  39. 0039specialize polynomial_diagonal_left_padding_right (ac)
  40. 0040specialize polynomial_diagonal_left_padding_right (L)
  41. 0041specialize polynomial_diagonal_left_padding_right (bb)
  42. 0042specialize polynomial_diagonal_left_padding_right (bc)
  43. 0043specialize polynomial_diagonal_left_padding_right (M)
  44. 0044specialize polynomial_diagonal_left_padding_right (BB)
  45. 0045specialize polynomial_diagonal_left_padding_right (BC)
  46. 0046specialize polynomial_diagonal_left_padding_right (t)
  47. 0047specialize polynomial_diagonal_left_padding_right (i)
  48. 0048specialize polynomial_diagonal_left_padding_right (x)
  49. 0049specialize polynomial_diagonal_left_padding_right (x1)
  50. 0050specialize polynomial_diagonal_left_padding_right (x3)
  51. 0051specialize polynomial_diagonal_left_padding_right (x4)
  52. 0052apply polynomial_diagonal_left_padding_right
  53. 0053exact hpad
  54. 0054exact hc_witness_witness_witness_left
  55. 0055exact hd_witness_witness
  56. 0056have heq : x5=x2
  57. 0057cases hdata
  58. 0058specialize polynomial_zero_tail_natural_sum_invariant (x)
  59. 0059specialize polynomial_zero_tail_natural_sum_invariant (x1)
  60. 0060specialize polynomial_zero_tail_natural_sum_invariant (x3)
  61. 0061specialize polynomial_zero_tail_natural_sum_invariant (x4)
  62. 0062specialize polynomial_zero_tail_natural_sum_invariant (S i)
  63. 0063specialize polynomial_zero_tail_natural_sum_invariant (t)
  64. 0064specialize polynomial_zero_tail_natural_sum_invariant (x2)
  65. 0065specialize polynomial_zero_tail_natural_sum_invariant (x5)
  66. 0066apply polynomial_zero_tail_natural_sum_invariant
  67. 0067exact hdata_left
  68. 0068exact hdata_right
  69. 0069exact hc_witness_witness_witness_right_left
  70. 0070have hlength : S i+t=S (t+i)
  71. 0071simp [add_succ_left,add_comm]
  72. 0072rewrite hlength
  73. 0073rewrite hlength
  74. 0074rewrite hlength
  75. 0075exact hs_witness
  76. 0076exists x3
  77. 0077exists x4
  78. 0078exists x2
  79. 0079split
  80. 0080exact hd_witness_witness
  81. 0081split
  82. 0082rewrite heq at hs_witness
  83. 0083rewrite heq at hs_witness
  84. 0084exact hs_witness
  85. 0085exact hc_witness_witness_witness_right_right