HL0014

beta_horner_coefficient_blend_exists

Every pair of finite integer-coefficient component codes admits an actual natural positive+weight*negative coefficient code.

Alpha v34 checked-use · first admitted v27 · 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. Exact original first-admission records.

The derivative-nonzero criterion supplies no inverse or power witness: both are constructed. Roots may be arbitrary natural representatives of signed integer polynomials. Singular-root classification and p-adic completion are separate milestones.

Exact theorem in conservative defined notation

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ h. ∀ l. ∃ gb. ∃ gc. HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l)

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

Definition DAG

Beta(b,c,i,x) · 7HornerCoefficientBlend(pb,pc,nb,nc,gb,gc,h,l) · 1Lt(a,b) · 2Repeat(b,c,a,l) · 1

Actual proof prerequisites

beta_repeat_exists · checked external prerequisitebeta_pointwise_mul_prefix_exists · checked external prerequisitebeta_pointwise_add_prefix_exists · checked external prerequisitebeta_at_exists · checked external prerequisite
Original expanded first-order statement 
forall pb pc nb nc h l. exists gb gc. (forall sph_i_blend sph_A_blend sph_B_blend sph_C_blend. (exists hpl_gap_blend. hpl_gap_blend + S (sph_i_blend) = (l)) -> (((exists fs_h_sph_blend_positive. fs_h_sph_blend_positive + S (sph_A_blend) = S ((S (sph_i_blend)) * pc)) /\ exists fs_q_sph_blend_positive. pb = fs_q_sph_blend_positive * S ((S (sph_i_blend)) * pc) + (sph_A_blend))) -> (((exists fs_h_sph_blend_negative. fs_h_sph_blend_negative + S (sph_B_blend) = S ((S (sph_i_blend)) * nc)) /\ exists fs_q_sph_blend_negative. nb = fs_q_sph_blend_negative * S ((S (sph_i_blend)) * nc) + (sph_B_blend))) -> (((exists fs_h_sph_blend_combined. fs_h_sph_blend_combined + S (sph_C_blend) = S ((S (sph_i_blend)) * gc)) /\ exists fs_q_sph_blend_combined. gb = fs_q_sph_blend_combined * S ((S (sph_i_blend)) * gc) + (sph_C_blend))) -> sph_C_blend = sph_A_blend + h * sph_B_blend)

Complete tactic proof in conservative notation

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

70 script commands · 16 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro h
  6. L6
    intro l
02Establish hrepeatedL7–10

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

  1. L7
    have hrepeated : ∃ rb. ∃ rc. Repeat(rb,rc,h,l)Definitions: Repeat(rb,rc,h,l)Original native command in the exact edition
  2. L8
    specialize beta_repeat_exists h
  3. L9
    specialize beta_repeat_exists l
  4. L10
    apply beta_repeat_exists
03Separate the logical casesL11–12

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

  1. L11
    cases hrepeated
  2. L12
    cases hrepeated_witness
04Establish hscaledL13–19

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

  1. L13
    have hscaled : ∃ sb. ∃ sc. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,l) → Beta(x,x1,y,z) → Beta(nb,nc,y,n) → Beta(sb,sc,y,m) → m = z · nDefinitions: Lt(y,l)Beta(x,x1,y,z)Beta(nb,nc,y,n)Beta(sb,sc,y,m)Original native command in the exact edition
  2. L14
    specialize beta_pointwise_mul_prefix_exists x
  3. L15
    specialize beta_pointwise_mul_prefix_exists x1
  4. L16
    specialize beta_pointwise_mul_prefix_exists nb
  5. L17
    specialize beta_pointwise_mul_prefix_exists nc
  6. L18
    specialize beta_pointwise_mul_prefix_exists l
  7. L19
    apply beta_pointwise_mul_prefix_exists
05Separate the logical casesL20–21

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

  1. L20
    cases hscaled
  2. L21
    cases hscaled_witness
06Establish haddedL22–28

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

  1. L22
    have hadded : ∃ gb. ∃ gc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → Beta(pb,pc,x,y) → Beta(x2,x3,x,z) → Beta(gb,gc,x,n) → n = y + zDefinitions: Lt(x,l)Beta(pb,pc,x,y)Beta(x2,x3,x,z)Beta(gb,gc,x,n)Original native command in the exact edition
  2. L23
    specialize beta_pointwise_add_prefix_exists pb
  3. L24
    specialize beta_pointwise_add_prefix_exists pc
  4. L25
    specialize beta_pointwise_add_prefix_exists x2
  5. L26
    specialize beta_pointwise_add_prefix_exists x3
  6. L27
    specialize beta_pointwise_add_prefix_exists l
  7. L28
    apply beta_pointwise_add_prefix_exists
07Separate the logical casesL29–30

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

  1. L29
    cases hadded
  2. L30
    cases hadded_witness
08Construct an explicit witnessL31–32

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

  1. L31
    exists x4
  2. L32
    exists x5
09Fix variables and assumptionsL33–40

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

  1. L33
    intro i
  2. L34
    intro A
  3. L35
    intro B
  4. L36
    intro C
  5. L37
    intro hi
  6. L38
    intro hA
  7. L39
    intro hB
  8. L40
    intro hC
10Establish hentryL41–45

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

  1. L41
    have hentry : ∃ w. Beta(x2,x3,i,w)Definitions: Beta(x2,x3,i,w)Original native command in the exact edition
  2. L42
    specialize beta_at_exists x2
  3. L43
    specialize beta_at_exists x3
  4. L44
    specialize beta_at_exists i
  5. L45
    apply beta_at_exists
11Separate the logical casesL46–46

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

  1. L46
    cases hentry
12Establish hscaleL47–56

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

  1. L47
    have hscale : x6 = h * B
  2. L48
    specialize hscaled_witness_witness i
  3. L49
    specialize hscaled_witness_witness h
  4. L50
    specialize hscaled_witness_witness B
  5. L51
    specialize hscaled_witness_witness x6
  6. L52
    apply hscaled_witness_witness
  7. L53
    exact hi
  8. L54
    specialize hrepeated_witness_witness i
  9. L55
    apply hrepeated_witness_witness
  10. L56
    exact hi
13Use earlier factsL57–58

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

  1. L57
    exact hB
  2. L58
    exact hentry_witness
14Calculate and transport equalitiesL59–59

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

  1. L59
    trans A + x6
15Use earlier factsL60–68

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

  1. L60
    specialize hadded_witness_witness i
  2. L61
    specialize hadded_witness_witness A
  3. L62
    specialize hadded_witness_witness x6
  4. L63
    specialize hadded_witness_witness C
  5. L64
    apply hadded_witness_witness
  6. L65
    exact hi
  7. L66
    exact hA
  8. L67
    exact hentry_witness
  9. L68
    exact hC
16Calculate and transport equalitiesL69–70

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

  1. L69
    rewrite hscale
  2. L70
    refl

Library-wide reading audit

Original defined command ledger · 70 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro h
  6. 0006intro l
  7. 0007have hrepeated : ∃ rb. ∃ rc. Repeat(rb,rc,h,l)
  8. 0008specialize beta_repeat_exists h
  9. 0009specialize beta_repeat_exists l
  10. 0010apply beta_repeat_exists
  11. 0011cases hrepeated
  12. 0012cases hrepeated_witness
  13. 0013have hscaled : ∃ sb. ∃ sc. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,l) → Beta(x,x1,y,z) → Beta(nb,nc,y,n) → Beta(sb,sc,y,m) → m = z · n
  14. 0014specialize beta_pointwise_mul_prefix_exists x
  15. 0015specialize beta_pointwise_mul_prefix_exists x1
  16. 0016specialize beta_pointwise_mul_prefix_exists nb
  17. 0017specialize beta_pointwise_mul_prefix_exists nc
  18. 0018specialize beta_pointwise_mul_prefix_exists l
  19. 0019apply beta_pointwise_mul_prefix_exists
  20. 0020cases hscaled
  21. 0021cases hscaled_witness
  22. 0022have hadded : ∃ gb. ∃ gc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → Beta(pb,pc,x,y) → Beta(x2,x3,x,z) → Beta(gb,gc,x,n) → n = y + z
  23. 0023specialize beta_pointwise_add_prefix_exists pb
  24. 0024specialize beta_pointwise_add_prefix_exists pc
  25. 0025specialize beta_pointwise_add_prefix_exists x2
  26. 0026specialize beta_pointwise_add_prefix_exists x3
  27. 0027specialize beta_pointwise_add_prefix_exists l
  28. 0028apply beta_pointwise_add_prefix_exists
  29. 0029cases hadded
  30. 0030cases hadded_witness
  31. 0031exists x4
  32. 0032exists x5
  33. 0033intro i
  34. 0034intro A
  35. 0035intro B
  36. 0036intro C
  37. 0037intro hi
  38. 0038intro hA
  39. 0039intro hB
  40. 0040intro hC
  41. 0041have hentry : ∃ w. Beta(x2,x3,i,w)
  42. 0042specialize beta_at_exists x2
  43. 0043specialize beta_at_exists x3
  44. 0044specialize beta_at_exists i
  45. 0045apply beta_at_exists
  46. 0046cases hentry
  47. 0047have hscale : x6 = h * B
  48. 0048specialize hscaled_witness_witness i
  49. 0049specialize hscaled_witness_witness h
  50. 0050specialize hscaled_witness_witness B
  51. 0051specialize hscaled_witness_witness x6
  52. 0052apply hscaled_witness_witness
  53. 0053exact hi
  54. 0054specialize hrepeated_witness_witness i
  55. 0055apply hrepeated_witness_witness
  56. 0056exact hi
  57. 0057exact hB
  58. 0058exact hentry_witness
  59. 0059trans A + x6
  60. 0060specialize hadded_witness_witness i
  61. 0061specialize hadded_witness_witness A
  62. 0062specialize hadded_witness_witness x6
  63. 0063specialize hadded_witness_witness C
  64. 0064apply hadded_witness_witness
  65. 0065exact hi
  66. 0066exact hA
  67. 0067exact hentry_witness
  68. 0068exact hC
  69. 0069rewrite hscale
  70. 0070refl