PG001B

prime_field_polynomial_append_shift_constant_decomposition_exists

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

Construct the shifted old prefix, a canonical singleton constant and its genuine leading padding, then prove their actual aligned sum is the given appended prefix.

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 p bb bc M c db dc. (~((p) = 1) /\ forall pfa_factor_left_append_decomposition_prime pfa_factor_right_append_decomposition_prime. (p) = pfa_factor_left_append_decomposition_prime * pfa_factor_right_append_decomposition_prime -> pfa_factor_left_append_decomposition_prime = 1 \/ pfa_factor_right_append_decomposition_prime = 1) -> (forall fom_index_pfp_append_decomposition_old_coefficients. (exists fom_gap_pfp_append_decomposition_old_coefficients_index_bound. fom_gap_pfp_append_decomposition_old_coefficients_index_bound + S (fom_index_pfp_append_decomposition_old_coefficients) = M) -> exists fom_value_pfp_append_decomposition_old_coefficients. ((((exists fom_beta_height_pfp_append_decomposition_old_coefficients_entry. fom_beta_height_pfp_append_decomposition_old_coefficients_entry + S (fom_value_pfp_append_decomposition_old_coefficients) = S ((S (fom_index_pfp_append_decomposition_old_coefficients)) * bc)) /\ exists fom_beta_quotient_pfp_append_decomposition_old_coefficients_entry. bb = fom_beta_quotient_pfp_append_decomposition_old_coefficients_entry * S ((S (fom_index_pfp_append_decomposition_old_coefficients)) * bc) + (fom_value_pfp_append_decomposition_old_coefficients))) /\ (exists fom_gap_pfp_append_decomposition_old_coefficients_value_bound. fom_gap_pfp_append_decomposition_old_coefficients_value_bound + S (fom_value_pfp_append_decomposition_old_coefficients) = p))) -> (exists pfa_gap_append_decomposition_scalar. pfa_gap_append_decomposition_scalar + S (c) = (p)) -> (forall mdr_i_pfp_append_decomposition_preserve mdr_a_pfp_append_decomposition_preserve. (exists mdr_gap_pfp_append_decomposition_preserveb. mdr_gap_pfp_append_decomposition_preserveb + S (mdr_i_pfp_append_decomposition_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_decomposition_preserveo. ff_h_mdr_pfp_append_decomposition_preserveo + S (mdr_a_pfp_append_decomposition_preserve) = S ((S (mdr_i_pfp_append_decomposition_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_decomposition_preserveo. bb = ff_q_mdr_pfp_append_decomposition_preserveo * S ((S (mdr_i_pfp_append_decomposition_preserve)) * bc) + (mdr_a_pfp_append_decomposition_preserve))) -> (((exists ff_h_mdr_pfp_append_decomposition_preserven. ff_h_mdr_pfp_append_decomposition_preserven + S (mdr_a_pfp_append_decomposition_preserve) = S ((S (mdr_i_pfp_append_decomposition_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_decomposition_preserven. db = ff_q_mdr_pfp_append_decomposition_preserven * S ((S (mdr_i_pfp_append_decomposition_preserve)) * dc) + (mdr_a_pfp_append_decomposition_preserve)))) -> (((exists ff_h_pfp_append_decomposition_actual_last. ff_h_pfp_append_decomposition_actual_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_decomposition_actual_last. db = ff_q_pfp_append_decomposition_actual_last * S ((S (M)) * dc) + (c))) -> (exists sb sc kb kc tb tc. ((((forall mdr_i_pfp_append_decomposition_shiftprefix mdr_a_pfp_append_decomposition_shiftprefix. (exists mdr_gap_pfp_append_decomposition_shiftprefixb. mdr_gap_pfp_append_decomposition_shiftprefixb + S (mdr_i_pfp_append_decomposition_shiftprefix) = (M)) -> (((exists ff_h_mdr_pfp_append_decomposition_shiftprefixo. ff_h_mdr_pfp_append_decomposition_shiftprefixo + S (mdr_a_pfp_append_decomposition_shiftprefix) = S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * bc)) /\ exists ff_q_mdr_pfp_append_decomposition_shiftprefixo. bb = ff_q_mdr_pfp_append_decomposition_shiftprefixo * S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * bc) + (mdr_a_pfp_append_decomposition_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_decomposition_shiftprefixn. ff_h_mdr_pfp_append_decomposition_shiftprefixn + S (mdr_a_pfp_append_decomposition_shiftprefix) = S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * sc)) /\ exists ff_q_mdr_pfp_append_decomposition_shiftprefixn. sb = ff_q_mdr_pfp_append_decomposition_shiftprefixn * S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * sc) + (mdr_a_pfp_append_decomposition_shiftprefix)))) /\ ((((exists ff_h_pfp_append_decomposition_shiftlast. ff_h_pfp_append_decomposition_shiftlast + S (0) = S ((S (M)) * sc)) /\ exists ff_q_pfp_append_decomposition_shiftlast. sb = ff_q_pfp_append_decomposition_shiftlast * S ((S (M)) * sc) + (0)))))) /\ (((forall fom_index_pfp_append_decomposition_constant_bound. (exists fom_gap_pfp_append_decomposition_constant_bound_index_bound. fom_gap_pfp_append_decomposition_constant_bound_index_bound + S (fom_index_pfp_append_decomposition_constant_bound) = 1) -> exists fom_value_pfp_append_decomposition_constant_bound. ((((exists fom_beta_height_pfp_append_decomposition_constant_bound_entry. fom_beta_height_pfp_append_decomposition_constant_bound_entry + S (fom_value_pfp_append_decomposition_constant_bound) = S ((S (fom_index_pfp_append_decomposition_constant_bound)) * kc)) /\ exists fom_beta_quotient_pfp_append_decomposition_constant_bound_entry. kb = fom_beta_quotient_pfp_append_decomposition_constant_bound_entry * S ((S (fom_index_pfp_append_decomposition_constant_bound)) * kc) + (fom_value_pfp_append_decomposition_constant_bound))) /\ (exists fom_gap_pfp_append_decomposition_constant_bound_value_bound. fom_gap_pfp_append_decomposition_constant_bound_value_bound + S (fom_value_pfp_append_decomposition_constant_bound) = p))) /\ (((((exists ff_h_pfp_append_decomposition_constant. ff_h_pfp_append_decomposition_constant + S (c) = S ((S (0)) * kc)) /\ exists ff_q_pfp_append_decomposition_constant. kb = ff_q_pfp_append_decomposition_constant * S ((S (0)) * kc) + (c))) /\ (((((forall pfp_repeat_index_append_decomposition_padzeros. (exists pfa_gap_append_decomposition_padzerosindex. pfa_gap_append_decomposition_padzerosindex + S (pfp_repeat_index_append_decomposition_padzeros) = (M)) -> (((exists ff_h_pfp_append_decomposition_padzerosentry. ff_h_pfp_append_decomposition_padzerosentry + S (0) = S ((S (pfp_repeat_index_append_decomposition_padzeros)) * tc)) /\ exists ff_q_pfp_append_decomposition_padzerosentry. tb = ff_q_pfp_append_decomposition_padzerosentry * S ((S (pfp_repeat_index_append_decomposition_padzeros)) * tc) + (0)))) /\ ((forall pfrep_index_append_decomposition_pad pfrep_value_append_decomposition_pad. (exists pfa_gap_append_decomposition_padbound. pfa_gap_append_decomposition_padbound + S (pfrep_index_append_decomposition_pad) = (1)) -> (((exists ff_h_pfp_append_decomposition_padinput. ff_h_pfp_append_decomposition_padinput + S (pfrep_value_append_decomposition_pad) = S ((S (pfrep_index_append_decomposition_pad)) * kc)) /\ exists ff_q_pfp_append_decomposition_padinput. kb = ff_q_pfp_append_decomposition_padinput * S ((S (pfrep_index_append_decomposition_pad)) * kc) + (pfrep_value_append_decomposition_pad))) -> (((exists ff_h_pfp_append_decomposition_padoutput. ff_h_pfp_append_decomposition_padoutput + S (pfrep_value_append_decomposition_pad) = S ((S ((M)+pfrep_index_append_decomposition_pad)) * tc)) /\ exists ff_q_pfp_append_decomposition_padoutput. tb = ff_q_pfp_append_decomposition_padoutput * S ((S ((M)+pfrep_index_append_decomposition_pad)) * tc) + (pfrep_value_append_decomposition_pad))))))) /\ ((forall pfp_index_append_decomposition_add. (exists pfa_gap_append_decomposition_addindex. pfa_gap_append_decomposition_addindex + S (pfp_index_append_decomposition_add) = (S M)) -> exists pfp_left_append_decomposition_add pfp_right_append_decomposition_add pfp_value_append_decomposition_add. ((((exists ff_h_pfp_append_decomposition_addleft. ff_h_pfp_append_decomposition_addleft + S (pfp_left_append_decomposition_add) = S ((S (pfp_index_append_decomposition_add)) * sc)) /\ exists ff_q_pfp_append_decomposition_addleft. sb = ff_q_pfp_append_decomposition_addleft * S ((S (pfp_index_append_decomposition_add)) * sc) + (pfp_left_append_decomposition_add))) /\ (((((exists ff_h_pfp_append_decomposition_addright. ff_h_pfp_append_decomposition_addright + S (pfp_right_append_decomposition_add) = S ((S (pfp_index_append_decomposition_add)) * tc)) /\ exists ff_q_pfp_append_decomposition_addright. tb = ff_q_pfp_append_decomposition_addright * S ((S (pfp_index_append_decomposition_add)) * tc) + (pfp_right_append_decomposition_add))) /\ (((((exists ff_h_pfp_append_decomposition_addtarget. ff_h_pfp_append_decomposition_addtarget + S (pfp_value_append_decomposition_add) = S ((S (pfp_index_append_decomposition_add)) * dc)) /\ exists ff_q_pfp_append_decomposition_addtarget. db = ff_q_pfp_append_decomposition_addtarget * S ((S (pfp_index_append_decomposition_add)) * dc) + (pfp_value_append_decomposition_add))) /\ ((((exists pfa_gap_append_decomposition_addoperationleft. pfa_gap_append_decomposition_addoperationleft + S (pfp_left_append_decomposition_add) = (p)) /\ (((exists pfa_gap_append_decomposition_addoperationright. pfa_gap_append_decomposition_addoperationright + S (pfp_right_append_decomposition_add) = (p)) /\ ((((exists pfa_gap_append_decomposition_addoperationresultbound. pfa_gap_append_decomposition_addoperationresultbound + S (pfp_value_append_decomposition_add) = (p)) /\ ((exists pfa_offset_left_append_decomposition_addoperationresultcongruence pfa_offset_right_append_decomposition_addoperationresultcongruence. ((pfp_left_append_decomposition_add) + (pfp_right_append_decomposition_add)) + (p) * pfa_offset_left_append_decomposition_addoperationresultcongruence = (pfp_value_append_decomposition_add) + (p) * pfa_offset_right_append_decomposition_addoperationresultcongruence)))))))))))))))))))))))))

Constructive proof overview

Generated structural guide

Construct the shifted old prefix, a canonical singleton constant and its genuine leading padding, then prove their actual aligned sum is the given appended prefix.

The unchanged tactic script uses 4 declared prerequisites and contains 83 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG0001 prime_field_polynomial_shift_exists beta_repeat_exists Alpha theorem; checked-use authorized prime_field_polynomial_left_pad_exists Alpha theorem; checked-use authorized PG001A prime_field_polynomial_append_shift_constant_add

Direct dependents

PG001E prime_field_polynomial_convolution_right_append_equivalent

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

83 script commands · 26 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.

Named ingredients (2)
prime field polynomial shift existsprime field polynomial append shift constant add

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro bb
  3. L3
    intro bc
  4. L4
    intro M
  5. L5
    intro c
  6. L6
    intro db
  7. L7
    intro dc
  8. L8
    intro hp
  9. L9
    intro hb
  10. L10
    intro hc
02Fix variables and assumptionsL11–12

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

  1. L11
    intro he
  2. L12
    intro hlast
03Establish hsL13–17

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

  1. L13
    have hs : ∃ sb. ∃ sc. PolynomialShift(bb,bc,M,sb,sc)Definitions: PolynomialShift
  2. L14
    specialize prime_field_polynomial_shift_exists (bb)
  3. L15
    specialize prime_field_polynomial_shift_exists (bc)
  4. L16
    specialize prime_field_polynomial_shift_exists (M)
  5. L17
    apply prime_field_polynomial_shift_exists
04Separate the logical casesL18–19

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

  1. L18
    cases hs
  2. L19
    cases hs_witness
05Establish hkL20–23

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

  1. L20
    have hk : exists kb kc. forall pfp_repeat_index_append_decomposition_repeat. (exists pfa_gap_append_decomposition_repeatindex. pfa_gap_append_decomposition_repeatindex + S (pfp_repeat_index_append_decomposition_repeat) = (1)) -> (((exists ff_h_pfp_append_decomposition_repeatentry. ff_h_pfp_append_decomposition_repeatentry + S (c) = S ((S (pfp_repeat_index_append_decomposition_repeat)) * kc)) /\ exists ff_q_pfp_append_decomposition_repeatentry. kb = ff_q_pfp_append_decomposition_repeatentry * S ((S (pfp_repeat_index_append_decomposition_repeat)) * kc) + (c)))
  2. L21
    specialize beta_repeat_exists (c)
  3. L22
    specialize beta_repeat_exists (1)
  4. L23
    apply beta_repeat_exists
06Separate the logical casesL24–25

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

  1. L24
    cases hk
  2. L25
    cases hk_witness
07Establish hconstantL26–28

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

  1. L26
    have hconstant : ((exists ff_h_pfp_append_decomposition_chosen_constant. ff_h_pfp_append_decomposition_chosen_constant + S (c) = S ((S (0)) * x3)) /\ exists ff_q_pfp_append_decomposition_chosen_constant. x2 = ff_q_pfp_append_decomposition_chosen_constant * S ((S (0)) * x3) + (c))
  2. L27
    specialize hk_witness_witness (0)
  3. L28
    apply hk_witness_witness
08Construct an explicit witnessL29–29

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

  1. L29
    exists 0
09Calculate and transport equalitiesL30–30

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

  1. L30
    simp
10Establish hboundedL31–33

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

  1. L31
    have hbounded : BetaPrefixInto(x2,x3,1,p)Definitions: BetaPrefixInto
  2. L32
    intro i
  3. L33
    intro hi
11Construct an explicit witnessL34–34

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

  1. L34
    exists c
12Separate the logical casesL35–35

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

  1. L35
    split
13Use earlier factsL36–39

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

  1. L36
    specialize hk_witness_witness (i)
  2. L37
    apply hk_witness_witness
  3. L38
    exact hi
  4. L39
    exact hc
14Establish htL40–45

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

  1. L40
    have ht : ∃ tb. ∃ tc. PolynomialLeftPad(x2,x3,1,M,tb,tc)Definitions: PolynomialLeftPad
  2. L41
    specialize prime_field_polynomial_left_pad_exists (x2)
  3. L42
    specialize prime_field_polynomial_left_pad_exists (x3)
  4. L43
    specialize prime_field_polynomial_left_pad_exists (M)
  5. L44
    specialize prime_field_polynomial_left_pad_exists (1)
  6. L45
    apply prime_field_polynomial_left_pad_exists
15Separate the logical casesL46–47

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

  1. L46
    cases ht
  2. L47
    cases ht_witness
16Construct an explicit witnessL48–53

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

  1. L48
    exists x
  2. L49
    exists x1
  3. L50
    exists x2
  4. L51
    exists x3
  5. L52
    exists x4
  6. L53
    exists x5
17Separate the logical casesL54–54

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

  1. L54
    split
18Use earlier factsL55–55

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

  1. L55
    exact hs_witness_witness
19Separate the logical casesL56–56

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

  1. L56
    split
20Use earlier factsL57–57

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

  1. L57
    exact hbounded
21Separate the logical casesL58–58

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

  1. L58
    split
22Use earlier factsL59–59

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

  1. L59
    exact hconstant
23Separate the logical casesL60–60

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

  1. L60
    split
24Use earlier factsL61–70

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

  1. L61
    exact ht_witness_witness
  2. L62
    specialize prime_field_polynomial_append_shift_constant_add (p)
  3. L63
    specialize prime_field_polynomial_append_shift_constant_add (bb)
  4. L64
    specialize prime_field_polynomial_append_shift_constant_add (bc)
  5. L65
    specialize prime_field_polynomial_append_shift_constant_add (M)
  6. L66
    specialize prime_field_polynomial_append_shift_constant_add (c)
  7. L67
    specialize prime_field_polynomial_append_shift_constant_add (db)
  8. L68
    specialize prime_field_polynomial_append_shift_constant_add (dc)
  9. L69
    specialize prime_field_polynomial_append_shift_constant_add (x)
  10. L70
    specialize prime_field_polynomial_append_shift_constant_add (x1)
25Use earlier factsL71–80

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

  1. L71
    specialize prime_field_polynomial_append_shift_constant_add (x2)
  2. L72
    specialize prime_field_polynomial_append_shift_constant_add (x3)
  3. L73
    specialize prime_field_polynomial_append_shift_constant_add (x4)
  4. L74
    specialize prime_field_polynomial_append_shift_constant_add (x5)
  5. L75
    apply prime_field_polynomial_append_shift_constant_add
  6. L76
    exact hp
  7. L77
    exact hb
  8. L78
    exact hc
  9. L79
    exact he
  10. L80
    exact hlast
26Use earlier factsL81–83

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

  1. L81
    exact hs_witness_witness
  2. L82
    exact hconstant
  3. L83
    exact ht_witness_witness

Library-wide reading audit

Original exact command ledger · 83 lines
  1. 0001intro p
  2. 0002intro bb
  3. 0003intro bc
  4. 0004intro M
  5. 0005intro c
  6. 0006intro db
  7. 0007intro dc
  8. 0008intro hp
  9. 0009intro hb
  10. 0010intro hc
  11. 0011intro he
  12. 0012intro hlast
  13. 0013have hs : exists sb sc. ((forall mdr_i_pfp_append_decomposition_shiftprefix mdr_a_pfp_append_decomposition_shiftprefix. (exists mdr_gap_pfp_append_decomposition_shiftprefixb. mdr_gap_pfp_append_decomposition_shiftprefixb + S (mdr_i_pfp_append_decomposition_shiftprefix) = (M)) -> (((exists ff_h_mdr_pfp_append_decomposition_shiftprefixo. ff_h_mdr_pfp_append_decomposition_shiftprefixo + S (mdr_a_pfp_append_decomposition_shiftprefix) = S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * bc)) /\ exists ff_q_mdr_pfp_append_decomposition_shiftprefixo. bb = ff_q_mdr_pfp_append_decomposition_shiftprefixo * S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * bc) + (mdr_a_pfp_append_decomposition_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_decomposition_shiftprefixn. ff_h_mdr_pfp_append_decomposition_shiftprefixn + S (mdr_a_pfp_append_decomposition_shiftprefix) = S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * sc)) /\ exists ff_q_mdr_pfp_append_decomposition_shiftprefixn. sb = ff_q_mdr_pfp_append_decomposition_shiftprefixn * S ((S (mdr_i_pfp_append_decomposition_shiftprefix)) * sc) + (mdr_a_pfp_append_decomposition_shiftprefix)))) /\ ((((exists ff_h_pfp_append_decomposition_shiftlast. ff_h_pfp_append_decomposition_shiftlast + S (0) = S ((S (M)) * sc)) /\ exists ff_q_pfp_append_decomposition_shiftlast. sb = ff_q_pfp_append_decomposition_shiftlast * S ((S (M)) * sc) + (0)))))
  14. 0014specialize prime_field_polynomial_shift_exists (bb)
  15. 0015specialize prime_field_polynomial_shift_exists (bc)
  16. 0016specialize prime_field_polynomial_shift_exists (M)
  17. 0017apply prime_field_polynomial_shift_exists
  18. 0018cases hs
  19. 0019cases hs_witness
  20. 0020have hk : exists kb kc. forall pfp_repeat_index_append_decomposition_repeat. (exists pfa_gap_append_decomposition_repeatindex. pfa_gap_append_decomposition_repeatindex + S (pfp_repeat_index_append_decomposition_repeat) = (1)) -> (((exists ff_h_pfp_append_decomposition_repeatentry. ff_h_pfp_append_decomposition_repeatentry + S (c) = S ((S (pfp_repeat_index_append_decomposition_repeat)) * kc)) /\ exists ff_q_pfp_append_decomposition_repeatentry. kb = ff_q_pfp_append_decomposition_repeatentry * S ((S (pfp_repeat_index_append_decomposition_repeat)) * kc) + (c)))
  21. 0021specialize beta_repeat_exists (c)
  22. 0022specialize beta_repeat_exists (1)
  23. 0023apply beta_repeat_exists
  24. 0024cases hk
  25. 0025cases hk_witness
  26. 0026have hconstant : ((exists ff_h_pfp_append_decomposition_chosen_constant. ff_h_pfp_append_decomposition_chosen_constant + S (c) = S ((S (0)) * x3)) /\ exists ff_q_pfp_append_decomposition_chosen_constant. x2 = ff_q_pfp_append_decomposition_chosen_constant * S ((S (0)) * x3) + (c))
  27. 0027specialize hk_witness_witness (0)
  28. 0028apply hk_witness_witness
  29. 0029exists 0
  30. 0030simp
  31. 0031have hbounded : forall fom_index_pfp_append_decomposition_chosen_bound. (exists fom_gap_pfp_append_decomposition_chosen_bound_index_bound. fom_gap_pfp_append_decomposition_chosen_bound_index_bound + S (fom_index_pfp_append_decomposition_chosen_bound) = 1) -> exists fom_value_pfp_append_decomposition_chosen_bound. ((((exists fom_beta_height_pfp_append_decomposition_chosen_bound_entry. fom_beta_height_pfp_append_decomposition_chosen_bound_entry + S (fom_value_pfp_append_decomposition_chosen_bound) = S ((S (fom_index_pfp_append_decomposition_chosen_bound)) * x3)) /\ exists fom_beta_quotient_pfp_append_decomposition_chosen_bound_entry. x2 = fom_beta_quotient_pfp_append_decomposition_chosen_bound_entry * S ((S (fom_index_pfp_append_decomposition_chosen_bound)) * x3) + (fom_value_pfp_append_decomposition_chosen_bound))) /\ (exists fom_gap_pfp_append_decomposition_chosen_bound_value_bound. fom_gap_pfp_append_decomposition_chosen_bound_value_bound + S (fom_value_pfp_append_decomposition_chosen_bound) = p))
  32. 0032intro i
  33. 0033intro hi
  34. 0034exists c
  35. 0035split
  36. 0036specialize hk_witness_witness (i)
  37. 0037apply hk_witness_witness
  38. 0038exact hi
  39. 0039exact hc
  40. 0040have ht : exists tb tc. ((forall pfp_repeat_index_append_decomposition_chosen_padzeros. (exists pfa_gap_append_decomposition_chosen_padzerosindex. pfa_gap_append_decomposition_chosen_padzerosindex + S (pfp_repeat_index_append_decomposition_chosen_padzeros) = (M)) -> (((exists ff_h_pfp_append_decomposition_chosen_padzerosentry. ff_h_pfp_append_decomposition_chosen_padzerosentry + S (0) = S ((S (pfp_repeat_index_append_decomposition_chosen_padzeros)) * tc)) /\ exists ff_q_pfp_append_decomposition_chosen_padzerosentry. tb = ff_q_pfp_append_decomposition_chosen_padzerosentry * S ((S (pfp_repeat_index_append_decomposition_chosen_padzeros)) * tc) + (0)))) /\ ((forall pfrep_index_append_decomposition_chosen_pad pfrep_value_append_decomposition_chosen_pad. (exists pfa_gap_append_decomposition_chosen_padbound. pfa_gap_append_decomposition_chosen_padbound + S (pfrep_index_append_decomposition_chosen_pad) = (1)) -> (((exists ff_h_pfp_append_decomposition_chosen_padinput. ff_h_pfp_append_decomposition_chosen_padinput + S (pfrep_value_append_decomposition_chosen_pad) = S ((S (pfrep_index_append_decomposition_chosen_pad)) * x3)) /\ exists ff_q_pfp_append_decomposition_chosen_padinput. x2 = ff_q_pfp_append_decomposition_chosen_padinput * S ((S (pfrep_index_append_decomposition_chosen_pad)) * x3) + (pfrep_value_append_decomposition_chosen_pad))) -> (((exists ff_h_pfp_append_decomposition_chosen_padoutput. ff_h_pfp_append_decomposition_chosen_padoutput + S (pfrep_value_append_decomposition_chosen_pad) = S ((S ((M)+pfrep_index_append_decomposition_chosen_pad)) * tc)) /\ exists ff_q_pfp_append_decomposition_chosen_padoutput. tb = ff_q_pfp_append_decomposition_chosen_padoutput * S ((S ((M)+pfrep_index_append_decomposition_chosen_pad)) * tc) + (pfrep_value_append_decomposition_chosen_pad))))))
  41. 0041specialize prime_field_polynomial_left_pad_exists (x2)
  42. 0042specialize prime_field_polynomial_left_pad_exists (x3)
  43. 0043specialize prime_field_polynomial_left_pad_exists (M)
  44. 0044specialize prime_field_polynomial_left_pad_exists (1)
  45. 0045apply prime_field_polynomial_left_pad_exists
  46. 0046cases ht
  47. 0047cases ht_witness
  48. 0048exists x
  49. 0049exists x1
  50. 0050exists x2
  51. 0051exists x3
  52. 0052exists x4
  53. 0053exists x5
  54. 0054split
  55. 0055exact hs_witness_witness
  56. 0056split
  57. 0057exact hbounded
  58. 0058split
  59. 0059exact hconstant
  60. 0060split
  61. 0061exact ht_witness_witness
  62. 0062specialize prime_field_polynomial_append_shift_constant_add (p)
  63. 0063specialize prime_field_polynomial_append_shift_constant_add (bb)
  64. 0064specialize prime_field_polynomial_append_shift_constant_add (bc)
  65. 0065specialize prime_field_polynomial_append_shift_constant_add (M)
  66. 0066specialize prime_field_polynomial_append_shift_constant_add (c)
  67. 0067specialize prime_field_polynomial_append_shift_constant_add (db)
  68. 0068specialize prime_field_polynomial_append_shift_constant_add (dc)
  69. 0069specialize prime_field_polynomial_append_shift_constant_add (x)
  70. 0070specialize prime_field_polynomial_append_shift_constant_add (x1)
  71. 0071specialize prime_field_polynomial_append_shift_constant_add (x2)
  72. 0072specialize prime_field_polynomial_append_shift_constant_add (x3)
  73. 0073specialize prime_field_polynomial_append_shift_constant_add (x4)
  74. 0074specialize prime_field_polynomial_append_shift_constant_add (x5)
  75. 0075apply prime_field_polynomial_append_shift_constant_add
  76. 0076exact hp
  77. 0077exact hb
  78. 0078exact hc
  79. 0079exact he
  80. 0080exact hlast
  81. 0081exact hs_witness_witness
  82. 0082exact hconstant
  83. 0083exact ht_witness_witness