PG0011

polynomial_zero_extended_scale_congruent

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

Actual coefficient scaling extends by genuine exterior zeros to a scalar congruence at every array index, with no condition on raw entries after the prefixes.

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 k bb bc sb sc M i b s. (((exists pfa_gap_scalar_pad_operationscalar. pfa_gap_scalar_pad_operationscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_pad_operation. (exists pfa_gap_scalar_pad_operationindex. pfa_gap_scalar_pad_operationindex + S (pfp_index_scalar_pad_operation) = (M)) -> exists pfp_source_scalar_pad_operation pfp_value_scalar_pad_operation. ((((exists ff_h_pfp_scalar_pad_operationsource. ff_h_pfp_scalar_pad_operationsource + S (pfp_source_scalar_pad_operation) = S ((S (pfp_index_scalar_pad_operation)) * bc)) /\ exists ff_q_pfp_scalar_pad_operationsource. bb = ff_q_pfp_scalar_pad_operationsource * S ((S (pfp_index_scalar_pad_operation)) * bc) + (pfp_source_scalar_pad_operation))) /\ (((((exists ff_h_pfp_scalar_pad_operationtarget. ff_h_pfp_scalar_pad_operationtarget + S (pfp_value_scalar_pad_operation) = S ((S (pfp_index_scalar_pad_operation)) * sc)) /\ exists ff_q_pfp_scalar_pad_operationtarget. sb = ff_q_pfp_scalar_pad_operationtarget * S ((S (pfp_index_scalar_pad_operation)) * sc) + (pfp_value_scalar_pad_operation))) /\ ((((exists pfa_gap_scalar_pad_operationoperationleft. pfa_gap_scalar_pad_operationoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_pad_operationoperationright. pfa_gap_scalar_pad_operationoperationright + S (pfp_source_scalar_pad_operation) = (p)) /\ ((((exists pfa_gap_scalar_pad_operationoperationresultbound. pfa_gap_scalar_pad_operationoperationresultbound + S (pfp_value_scalar_pad_operation) = (p)) /\ ((exists pfa_offset_left_scalar_pad_operationoperationresultcongruence pfa_offset_right_scalar_pad_operationoperationresultcongruence. ((k) * (pfp_source_scalar_pad_operation)) + (p) * pfa_offset_left_scalar_pad_operationoperationresultcongruence = (pfp_value_scalar_pad_operation) + (p) * pfa_offset_right_scalar_pad_operationoperationresultcongruence))))))))))))))))) -> ((((exists pfa_gap_scalar_pad_sourceinside. pfa_gap_scalar_pad_sourceinside + S (i) = (M)) /\ ((((exists ff_h_pfp_scalar_pad_sourceentry. ff_h_pfp_scalar_pad_sourceentry + S (b) = S ((S (i)) * bc)) /\ exists ff_q_pfp_scalar_pad_sourceentry. bb = ff_q_pfp_scalar_pad_sourceentry * S ((S (i)) * bc) + (b)))))) \/ (((exists pfc_gap_scalar_pad_sourceoutside. pfc_gap_scalar_pad_sourceoutside+(M)=(i)) /\ (((b)=0))))) -> ((((exists pfa_gap_scalar_pad_targetinside. pfa_gap_scalar_pad_targetinside + S (i) = (M)) /\ ((((exists ff_h_pfp_scalar_pad_targetentry. ff_h_pfp_scalar_pad_targetentry + S (s) = S ((S (i)) * sc)) /\ exists ff_q_pfp_scalar_pad_targetentry. sb = ff_q_pfp_scalar_pad_targetentry * S ((S (i)) * sc) + (s)))))) \/ (((exists pfc_gap_scalar_pad_targetoutside. pfc_gap_scalar_pad_targetoutside+(M)=(i)) /\ (((s)=0))))) -> (exists pfa_offset_left_scalar_pad_result pfa_offset_right_scalar_pad_result. (k*b) + (p) * pfa_offset_left_scalar_pad_result = (s) + (p) * pfa_offset_right_scalar_pad_result)

Constructive proof overview

Generated structural guide

Actual coefficient scaling extends by genuine exterior zeros to a scalar congruence at every array index, with no condition on raw entries after the prefixes.

The unchanged tactic script uses 3 declared prerequisites and contains 63 exact native proof lines.

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

Proof neighborhood

Direct dependencies

polynomial_zero_extended_entry_inside Alpha theorem; checked-use authorized prime_field_polynomial_scale_entry Alpha theorem; checked-use authorized polynomial_zero_extended_entry_functional Alpha theorem; checked-use authorized

Direct dependents

PG0012 polynomial_diagonal_term_right_scale_congruent

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

63 script commands · 15 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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 k
  3. L3
    intro bb
  4. L4
    intro bc
  5. L5
    intro sb
  6. L6
    intro sc
  7. L7
    intro M
  8. L8
    intro i
  9. L9
    intro b
  10. L10
    intro s
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hs
  2. L12
    intro hb
  3. L13
    intro hr
03Separate the logical casesL14–15

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

  1. L14
    cases hb
  2. L15
    cases hb_left
04Establish htargetL16–24

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

  1. L16
    have htarget : ((exists ff_h_pfp_scalar_pad_inside_target. ff_h_pfp_scalar_pad_inside_target + S (s) = S ((S (i)) * sc)) /\ exists ff_q_pfp_scalar_pad_inside_target. sb = ff_q_pfp_scalar_pad_inside_target * S ((S (i)) * sc) + (s))
  2. L17
    specialize polynomial_zero_extended_entry_inside (sb)
  3. L18
    specialize polynomial_zero_extended_entry_inside (sc)
  4. L19
    specialize polynomial_zero_extended_entry_inside (M)
  5. L20
    specialize polynomial_zero_extended_entry_inside (i)
  6. L21
    specialize polynomial_zero_extended_entry_inside (s)
  7. L22
    apply polynomial_zero_extended_entry_inside
  8. L23
    exact hb_left_left
  9. L24
    exact hr
05Establish hmL25–34

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

  1. L25
    have hm : FpMul(p,k,b,s)Definitions: FpMul
  2. L26
    specialize prime_field_polynomial_scale_entry (p)
  3. L27
    specialize prime_field_polynomial_scale_entry (k)
  4. L28
    specialize prime_field_polynomial_scale_entry (bb)
  5. L29
    specialize prime_field_polynomial_scale_entry (bc)
  6. L30
    specialize prime_field_polynomial_scale_entry (sb)
  7. L31
    specialize prime_field_polynomial_scale_entry (sc)
  8. L32
    specialize prime_field_polynomial_scale_entry (M)
  9. L33
    specialize prime_field_polynomial_scale_entry (i)
  10. L34
    specialize prime_field_polynomial_scale_entry (b)
06Use earlier factsL35–40

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

  1. L35
    specialize prime_field_polynomial_scale_entry (s)
  2. L36
    apply prime_field_polynomial_scale_entry
  3. L37
    exact hs
  4. L38
    exact hb_left_left
  5. L39
    exact hb_left_right
  6. L40
    exact htarget
07Separate the logical casesL41–43

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

  1. L41
    cases hm
  2. L42
    cases hm_right
  3. L43
    cases hm_right_right
08Use earlier factsL44–44

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

  1. L44
    exact hm_right_right_right
09Separate the logical casesL45–45

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

  1. L45
    cases hb_right
10Establish hzL46–54

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

  1. L46
    have hz : s=0
  2. L47
    specialize polynomial_zero_extended_entry_functional (sb)
  3. L48
    specialize polynomial_zero_extended_entry_functional (sc)
  4. L49
    specialize polynomial_zero_extended_entry_functional (M)
  5. L50
    specialize polynomial_zero_extended_entry_functional (i)
  6. L51
    specialize polynomial_zero_extended_entry_functional (s)
  7. L52
    specialize polynomial_zero_extended_entry_functional (0)
  8. L53
    apply polynomial_zero_extended_entry_functional
  9. L54
    exact hr
11Separate the logical casesL55–56

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

  1. L55
    right
  2. L56
    split
12Use earlier factsL57–57

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

  1. L57
    exact hb_right_left
13Calculate and transport equalitiesL58–60

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

  1. L58
    refl
  2. L59
    rewrite hb_right_right
  3. L60
    rewrite hz
14Construct an explicit witnessL61–62

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

  1. L61
    exists 0
  2. L62
    exists 0
15Calculate and transport equalitiesL63–63

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

  1. L63
    simp

Library-wide reading audit

Original exact command ledger · 63 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro sb
  6. 0006intro sc
  7. 0007intro M
  8. 0008intro i
  9. 0009intro b
  10. 0010intro s
  11. 0011intro hs
  12. 0012intro hb
  13. 0013intro hr
  14. 0014cases hb
  15. 0015cases hb_left
  16. 0016have htarget : ((exists ff_h_pfp_scalar_pad_inside_target. ff_h_pfp_scalar_pad_inside_target + S (s) = S ((S (i)) * sc)) /\ exists ff_q_pfp_scalar_pad_inside_target. sb = ff_q_pfp_scalar_pad_inside_target * S ((S (i)) * sc) + (s))
  17. 0017specialize polynomial_zero_extended_entry_inside (sb)
  18. 0018specialize polynomial_zero_extended_entry_inside (sc)
  19. 0019specialize polynomial_zero_extended_entry_inside (M)
  20. 0020specialize polynomial_zero_extended_entry_inside (i)
  21. 0021specialize polynomial_zero_extended_entry_inside (s)
  22. 0022apply polynomial_zero_extended_entry_inside
  23. 0023exact hb_left_left
  24. 0024exact hr
  25. 0025have hm : ((exists pfa_gap_scalar_pad_inside_productleft. pfa_gap_scalar_pad_inside_productleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_pad_inside_productright. pfa_gap_scalar_pad_inside_productright + S (b) = (p)) /\ ((((exists pfa_gap_scalar_pad_inside_productresultbound. pfa_gap_scalar_pad_inside_productresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_scalar_pad_inside_productresultcongruence pfa_offset_right_scalar_pad_inside_productresultcongruence. ((k) * (b)) + (p) * pfa_offset_left_scalar_pad_inside_productresultcongruence = (s) + (p) * pfa_offset_right_scalar_pad_inside_productresultcongruence))))))))
  26. 0026specialize prime_field_polynomial_scale_entry (p)
  27. 0027specialize prime_field_polynomial_scale_entry (k)
  28. 0028specialize prime_field_polynomial_scale_entry (bb)
  29. 0029specialize prime_field_polynomial_scale_entry (bc)
  30. 0030specialize prime_field_polynomial_scale_entry (sb)
  31. 0031specialize prime_field_polynomial_scale_entry (sc)
  32. 0032specialize prime_field_polynomial_scale_entry (M)
  33. 0033specialize prime_field_polynomial_scale_entry (i)
  34. 0034specialize prime_field_polynomial_scale_entry (b)
  35. 0035specialize prime_field_polynomial_scale_entry (s)
  36. 0036apply prime_field_polynomial_scale_entry
  37. 0037exact hs
  38. 0038exact hb_left_left
  39. 0039exact hb_left_right
  40. 0040exact htarget
  41. 0041cases hm
  42. 0042cases hm_right
  43. 0043cases hm_right_right
  44. 0044exact hm_right_right_right
  45. 0045cases hb_right
  46. 0046have hz : s=0
  47. 0047specialize polynomial_zero_extended_entry_functional (sb)
  48. 0048specialize polynomial_zero_extended_entry_functional (sc)
  49. 0049specialize polynomial_zero_extended_entry_functional (M)
  50. 0050specialize polynomial_zero_extended_entry_functional (i)
  51. 0051specialize polynomial_zero_extended_entry_functional (s)
  52. 0052specialize polynomial_zero_extended_entry_functional (0)
  53. 0053apply polynomial_zero_extended_entry_functional
  54. 0054exact hr
  55. 0055right
  56. 0056split
  57. 0057exact hb_right_left
  58. 0058refl
  59. 0059rewrite hb_right_right
  60. 0060rewrite hz
  61. 0061exists 0
  62. 0062exists 0
  63. 0063simp