HL0014

beta_horner_coefficient_blend_exists

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

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

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.

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

beta_repeat_exists Stable theorem; checked-use authorized beta_pointwise_mul_prefix_exists Alpha theorem; checked-use authorized beta_pointwise_add_prefix_exists Alpha theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized

Direct dependents

HL001F beta_signed_horner_hensel_iterated_exists_unique

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

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.

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–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 : exists rb rc. (forall ff_i_sph_repeat. (exists ff_lt_sph_repeat_bound. ff_lt_sph_repeat_bound + S ff_i_sph_repeat = l) -> (((exists ff_h_sph_repeat_decoded. ff_h_sph_repeat_decoded + S (h) = S ((S (ff_i_sph_repeat)) * rc)) /\ exists ff_q_sph_repeat_decoded. rb = ff_q_sph_repeat_decoded * S ((S (ff_i_sph_repeat)) * rc) + (h))))
  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: BetaLt
  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: BetaLt
  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 : exists w. (((exists fs_h_sph_entry. fs_h_sph_entry + S (w) = S ((S (i)) * x3)) /\ exists fs_q_sph_entry. x2 = fs_q_sph_entry * S ((S (i)) * x3) + (w)))
  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 exact 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 : exists rb rc. (forall ff_i_sph_repeat. (exists ff_lt_sph_repeat_bound. ff_lt_sph_repeat_bound + S ff_i_sph_repeat = l) -> (((exists ff_h_sph_repeat_decoded. ff_h_sph_repeat_decoded + S (h) = S ((S (ff_i_sph_repeat)) * rc)) /\ exists ff_q_sph_repeat_decoded. rb = ff_q_sph_repeat_decoded * S ((S (ff_i_sph_repeat)) * rc) + (h))))
  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 : exists sb sc. (forall fpmp_index_sph_scale fpmp_left_sph_scale fpmp_right_sph_scale fpmp_target_sph_scale. (exists fpmp_gap_sph_scale. fpmp_gap_sph_scale + S fpmp_index_sph_scale = l) -> (((exists ff_h_fpmp_sph_scale_left. ff_h_fpmp_sph_scale_left + S (fpmp_left_sph_scale) = S ((S (fpmp_index_sph_scale)) * x1)) /\ exists ff_q_fpmp_sph_scale_left. x = ff_q_fpmp_sph_scale_left * S ((S (fpmp_index_sph_scale)) * x1) + (fpmp_left_sph_scale))) -> (((exists ff_h_fpmp_sph_scale_right. ff_h_fpmp_sph_scale_right + S (fpmp_right_sph_scale) = S ((S (fpmp_index_sph_scale)) * nc)) /\ exists ff_q_fpmp_sph_scale_right. nb = ff_q_fpmp_sph_scale_right * S ((S (fpmp_index_sph_scale)) * nc) + (fpmp_right_sph_scale))) -> (((exists ff_h_fpmp_sph_scale_target. ff_h_fpmp_sph_scale_target + S (fpmp_target_sph_scale) = S ((S (fpmp_index_sph_scale)) * sc)) /\ exists ff_q_fpmp_sph_scale_target. sb = ff_q_fpmp_sph_scale_target * S ((S (fpmp_index_sph_scale)) * sc) + (fpmp_target_sph_scale))) -> fpmp_target_sph_scale = fpmp_left_sph_scale * fpmp_right_sph_scale)
  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 : exists gb gc. (forall ff_index_mcp_add_sph_add ff_left_mcp_add_sph_add ff_right_mcp_add_sph_add ff_target_mcp_add_sph_add. (exists mcp_gap_sph_add_bound. mcp_gap_sph_add_bound + S (ff_index_mcp_add_sph_add) = (l)) -> (((exists fs_h_mcp_sph_add_left. fs_h_mcp_sph_add_left + S (ff_left_mcp_add_sph_add) = S ((S (ff_index_mcp_add_sph_add)) * pc)) /\ exists fs_q_mcp_sph_add_left. pb = fs_q_mcp_sph_add_left * S ((S (ff_index_mcp_add_sph_add)) * pc) + (ff_left_mcp_add_sph_add))) -> (((exists fs_h_mcp_sph_add_right. fs_h_mcp_sph_add_right + S (ff_right_mcp_add_sph_add) = S ((S (ff_index_mcp_add_sph_add)) * x3)) /\ exists fs_q_mcp_sph_add_right. x2 = fs_q_mcp_sph_add_right * S ((S (ff_index_mcp_add_sph_add)) * x3) + (ff_right_mcp_add_sph_add))) -> (((exists fs_h_mcp_sph_add_target. fs_h_mcp_sph_add_target + S (ff_target_mcp_add_sph_add) = S ((S (ff_index_mcp_add_sph_add)) * gc)) /\ exists fs_q_mcp_sph_add_target. gb = fs_q_mcp_sph_add_target * S ((S (ff_index_mcp_add_sph_add)) * gc) + (ff_target_mcp_add_sph_add))) -> ff_target_mcp_add_sph_add = ff_left_mcp_add_sph_add + ff_right_mcp_add_sph_add)
  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 : exists w. (((exists fs_h_sph_entry. fs_h_sph_entry + S (w) = S ((S (i)) * x3)) /\ exists fs_q_sph_entry. x2 = fs_q_sph_entry * S ((S (i)) * x3) + (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