PG0011

polynomial_zero_extended_scale_congruent

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.

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

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ k. ∀ bb. ∀ bc. ∀ sb. ∀ sc. ∀ M. ∀ i. ∀ b. ∀ s. FpPolyScale(p,k,bb,bc,sb,sc,M) → BetaZeroExtend(bb,bc,M,i,b) → BetaZeroExtend(sb,sc,M,i,s) → ModEq(p,k · b,s)

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

Definition DAG

FpMul(p,a,b,c) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 1BetaZeroExtend(b,c,L,i,a) · 2ModEq(m,a,b) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

polynomial_zero_extended_entry_inside · checked external prerequisiteprime_field_polynomial_scale_entry · checked external prerequisitepolynomial_zero_extended_entry_functional · checked external prerequisite
Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : BetaAt(sb,sc,i,s)Definitions: BetaAt(sb,sc,i,s)Original native command in the exact edition
  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
  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 defined 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 : BetaAt(sb,sc,i,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 : FpMul(p,k,b,s)
  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