MD0005

beta_dot_product_functional

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

The exact finite dot-product value is independent of its coding witness.

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 mb mc sb sc l n m. (exists ff_code_dot_value ff_scale_dot_value. ((forall fpmp_index_dot_value_pointwise fpmp_left_dot_value_pointwise fpmp_right_dot_value_pointwise fpmp_target_dot_value_pointwise. (exists fpmp_gap_dot_value_pointwise. fpmp_gap_dot_value_pointwise + S fpmp_index_dot_value_pointwise = l) -> (((exists ff_h_fpmp_dot_value_pointwise_left. ff_h_fpmp_dot_value_pointwise_left + S (fpmp_left_dot_value_pointwise) = S ((S (fpmp_index_dot_value_pointwise)) * mc)) /\ exists ff_q_fpmp_dot_value_pointwise_left. mb = ff_q_fpmp_dot_value_pointwise_left * S ((S (fpmp_index_dot_value_pointwise)) * mc) + (fpmp_left_dot_value_pointwise))) -> (((exists ff_h_fpmp_dot_value_pointwise_right. ff_h_fpmp_dot_value_pointwise_right + S (fpmp_right_dot_value_pointwise) = S ((S (fpmp_index_dot_value_pointwise)) * sc)) /\ exists ff_q_fpmp_dot_value_pointwise_right. sb = ff_q_fpmp_dot_value_pointwise_right * S ((S (fpmp_index_dot_value_pointwise)) * sc) + (fpmp_right_dot_value_pointwise))) -> (((exists ff_h_fpmp_dot_value_pointwise_target. ff_h_fpmp_dot_value_pointwise_target + S (fpmp_target_dot_value_pointwise) = S ((S (fpmp_index_dot_value_pointwise)) * ff_scale_dot_value)) /\ exists ff_q_fpmp_dot_value_pointwise_target. ff_code_dot_value = ff_q_fpmp_dot_value_pointwise_target * S ((S (fpmp_index_dot_value_pointwise)) * ff_scale_dot_value) + (fpmp_target_dot_value_pointwise))) -> fpmp_target_dot_value_pointwise = fpmp_left_dot_value_pointwise * fpmp_right_dot_value_pointwise) /\ (exists ff_u_dot_value_sum ff_v_dot_value_sum. ((((exists ff_h_dot_value_sum_start. ff_h_dot_value_sum_start + S (0) = S ((S (0)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_start. ff_u_dot_value_sum = ff_q_dot_value_sum_start * S ((S (0)) * ff_v_dot_value_sum) + (0))) /\ ((((exists ff_h_dot_value_sum_terminal. ff_h_dot_value_sum_terminal + S (n) = S ((S (l)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_terminal. ff_u_dot_value_sum = ff_q_dot_value_sum_terminal * S ((S (l)) * ff_v_dot_value_sum) + (n))) /\ forall ff_i_dot_value_sum. (exists ff_lt_dot_value_sum_bound. ff_lt_dot_value_sum_bound + S ff_i_dot_value_sum = l) -> exists ff_a_dot_value_sum ff_r_dot_value_sum ff_s_dot_value_sum. ((((exists ff_h_dot_value_sum_summand. ff_h_dot_value_sum_summand + S (ff_a_dot_value_sum) = S ((S (ff_i_dot_value_sum)) * ff_scale_dot_value)) /\ exists ff_q_dot_value_sum_summand. ff_code_dot_value = ff_q_dot_value_sum_summand * S ((S (ff_i_dot_value_sum)) * ff_scale_dot_value) + (ff_a_dot_value_sum))) /\ ((((exists ff_h_dot_value_sum_partial. ff_h_dot_value_sum_partial + S (ff_r_dot_value_sum) = S ((S (ff_i_dot_value_sum)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_partial. ff_u_dot_value_sum = ff_q_dot_value_sum_partial * S ((S (ff_i_dot_value_sum)) * ff_v_dot_value_sum) + (ff_r_dot_value_sum))) /\ ((((exists ff_h_dot_value_sum_successor. ff_h_dot_value_sum_successor + S (ff_s_dot_value_sum) = S ((S (S ff_i_dot_value_sum)) * ff_v_dot_value_sum)) /\ exists ff_q_dot_value_sum_successor. ff_u_dot_value_sum = ff_q_dot_value_sum_successor * S ((S (S ff_i_dot_value_sum)) * ff_v_dot_value_sum) + (ff_s_dot_value_sum))) /\ ff_s_dot_value_sum = ff_r_dot_value_sum + ff_a_dot_value_sum)))))))) -> (exists ff_code_dot_other ff_scale_dot_other. ((forall fpmp_index_dot_other_pointwise fpmp_left_dot_other_pointwise fpmp_right_dot_other_pointwise fpmp_target_dot_other_pointwise. (exists fpmp_gap_dot_other_pointwise. fpmp_gap_dot_other_pointwise + S fpmp_index_dot_other_pointwise = l) -> (((exists ff_h_fpmp_dot_other_pointwise_left. ff_h_fpmp_dot_other_pointwise_left + S (fpmp_left_dot_other_pointwise) = S ((S (fpmp_index_dot_other_pointwise)) * mc)) /\ exists ff_q_fpmp_dot_other_pointwise_left. mb = ff_q_fpmp_dot_other_pointwise_left * S ((S (fpmp_index_dot_other_pointwise)) * mc) + (fpmp_left_dot_other_pointwise))) -> (((exists ff_h_fpmp_dot_other_pointwise_right. ff_h_fpmp_dot_other_pointwise_right + S (fpmp_right_dot_other_pointwise) = S ((S (fpmp_index_dot_other_pointwise)) * sc)) /\ exists ff_q_fpmp_dot_other_pointwise_right. sb = ff_q_fpmp_dot_other_pointwise_right * S ((S (fpmp_index_dot_other_pointwise)) * sc) + (fpmp_right_dot_other_pointwise))) -> (((exists ff_h_fpmp_dot_other_pointwise_target. ff_h_fpmp_dot_other_pointwise_target + S (fpmp_target_dot_other_pointwise) = S ((S (fpmp_index_dot_other_pointwise)) * ff_scale_dot_other)) /\ exists ff_q_fpmp_dot_other_pointwise_target. ff_code_dot_other = ff_q_fpmp_dot_other_pointwise_target * S ((S (fpmp_index_dot_other_pointwise)) * ff_scale_dot_other) + (fpmp_target_dot_other_pointwise))) -> fpmp_target_dot_other_pointwise = fpmp_left_dot_other_pointwise * fpmp_right_dot_other_pointwise) /\ (exists ff_u_dot_other_sum ff_v_dot_other_sum. ((((exists ff_h_dot_other_sum_start. ff_h_dot_other_sum_start + S (0) = S ((S (0)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_start. ff_u_dot_other_sum = ff_q_dot_other_sum_start * S ((S (0)) * ff_v_dot_other_sum) + (0))) /\ ((((exists ff_h_dot_other_sum_terminal. ff_h_dot_other_sum_terminal + S (m) = S ((S (l)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_terminal. ff_u_dot_other_sum = ff_q_dot_other_sum_terminal * S ((S (l)) * ff_v_dot_other_sum) + (m))) /\ forall ff_i_dot_other_sum. (exists ff_lt_dot_other_sum_bound. ff_lt_dot_other_sum_bound + S ff_i_dot_other_sum = l) -> exists ff_a_dot_other_sum ff_r_dot_other_sum ff_s_dot_other_sum. ((((exists ff_h_dot_other_sum_summand. ff_h_dot_other_sum_summand + S (ff_a_dot_other_sum) = S ((S (ff_i_dot_other_sum)) * ff_scale_dot_other)) /\ exists ff_q_dot_other_sum_summand. ff_code_dot_other = ff_q_dot_other_sum_summand * S ((S (ff_i_dot_other_sum)) * ff_scale_dot_other) + (ff_a_dot_other_sum))) /\ ((((exists ff_h_dot_other_sum_partial. ff_h_dot_other_sum_partial + S (ff_r_dot_other_sum) = S ((S (ff_i_dot_other_sum)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_partial. ff_u_dot_other_sum = ff_q_dot_other_sum_partial * S ((S (ff_i_dot_other_sum)) * ff_v_dot_other_sum) + (ff_r_dot_other_sum))) /\ ((((exists ff_h_dot_other_sum_successor. ff_h_dot_other_sum_successor + S (ff_s_dot_other_sum) = S ((S (S ff_i_dot_other_sum)) * ff_v_dot_other_sum)) /\ exists ff_q_dot_other_sum_successor. ff_u_dot_other_sum = ff_q_dot_other_sum_successor * S ((S (S ff_i_dot_other_sum)) * ff_v_dot_other_sum) + (ff_s_dot_other_sum))) /\ ff_s_dot_other_sum = ff_r_dot_other_sum + ff_a_dot_other_sum)))))))) -> n = m

Constructive proof overview

Generated structural guide

The exact finite dot-product value is independent of its coding witness.

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

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized beta_sum_transport_prefix Alpha theorem; checked-use authorized beta_sum_functional Stable theorem; checked-use authorized

Direct dependents

MD0006 beta_dot_product_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

82 script commands · 14 reading checkpoints · 7 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–9

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

  1. L1
    intro mb
  2. L2
    intro mc
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro m
  8. L8
    intro hn
  9. L9
    intro hm
02Separate the logical casesL10–15

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

  1. L10
    cases hn
  2. L11
    cases hn_witness
  3. L12
    cases hn_witness_witness
  4. L13
    cases hm
  5. L14
    cases hm_witness
  6. L15
    cases hm_witness_witness
03Establish htransportL16–25

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

  1. L16
    have htransport : Sum(x2,x3,l,n)Definitions: Sum
  2. L17
    specialize beta_sum_transport_prefix x
  3. L18
    specialize beta_sum_transport_prefix x1
  4. L19
    specialize beta_sum_transport_prefix x2
  5. L20
    specialize beta_sum_transport_prefix x3
  6. L21
    specialize beta_sum_transport_prefix l
  7. L22
    specialize beta_sum_transport_prefix n
  8. L23
    apply beta_sum_transport_prefix
  9. L24
    exact hn_witness_witness_right
  10. L25
    intro i
04Fix variables and assumptionsL26–28

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

  1. L26
    intro a
  2. L27
    intro hi
  3. L28
    intro ha
05Establish hleftL29–33

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

  1. L29
    have hleft : exists z. ((exists fs_h_dot_left. fs_h_dot_left + S (z) = S ((S (i)) * mc)) /\ exists fs_q_dot_left. mb = fs_q_dot_left * S ((S (i)) * mc) + (z))
  2. L30
    specialize beta_at_exists mb
  3. L31
    specialize beta_at_exists mc
  4. L32
    specialize beta_at_exists i
  5. L33
    exact beta_at_exists
06Separate the logical casesL34–34

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

  1. L34
    cases hleft
07Establish hrightL35–39

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

  1. L35
    have hright : exists z. ((exists fs_h_dot_right. fs_h_dot_right + S (z) = S ((S (i)) * sc)) /\ exists fs_q_dot_right. sb = fs_q_dot_right * S ((S (i)) * sc) + (z))
  2. L36
    specialize beta_at_exists sb
  3. L37
    specialize beta_at_exists sc
  4. L38
    specialize beta_at_exists i
  5. L39
    exact beta_at_exists
08Separate the logical casesL40–40

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

  1. L40
    cases hright
09Establish htargetL41–45

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

  1. L41
    have htarget : exists z. ((exists fs_h_dot_target. fs_h_dot_target + S (z) = S ((S (i)) * x3)) /\ exists fs_q_dot_target. x2 = fs_q_dot_target * S ((S (i)) * x3) + (z))
  2. L42
    specialize beta_at_exists x2
  3. L43
    specialize beta_at_exists x3
  4. L44
    specialize beta_at_exists i
  5. L45
    exact beta_at_exists
10Separate the logical casesL46–46

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

  1. L46
    cases htarget
11Establish hfirstL47–56

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

  1. L47
    have hfirst : a = x4 * x5
  2. L48
    specialize hn_witness_witness_left i
  3. L49
    specialize hn_witness_witness_left x4
  4. L50
    specialize hn_witness_witness_left x5
  5. L51
    specialize hn_witness_witness_left a
  6. L52
    apply hn_witness_witness_left
  7. L53
    exact hi
  8. L54
    exact hleft_witness
  9. L55
    exact hright_witness
  10. L56
    exact ha
12Establish hsecondL57–66

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

  1. L57
    have hsecond : x6 = x4 * x5
  2. L58
    specialize hm_witness_witness_left i
  3. L59
    specialize hm_witness_witness_left x4
  4. L60
    specialize hm_witness_witness_left x5
  5. L61
    specialize hm_witness_witness_left x6
  6. L62
    apply hm_witness_witness_left
  7. L63
    exact hi
  8. L64
    exact hleft_witness
  9. L65
    exact hright_witness
  10. L66
    exact htarget_witness
13Establish heqL67–76

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

  1. L67
    have heq : a = x6
  2. L68
    trans x4 * x5
  3. L69
    exact hfirst
  4. L70
    symm
  5. L71
    exact hsecond
  6. L72
    rewrite heq
  7. L73
    rewrite heq
  8. L74
    exact htarget_witness
  9. L75
    specialize beta_sum_functional x2
  10. L76
    specialize beta_sum_functional x3
14Use earlier factsL77–82

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

  1. L77
    specialize beta_sum_functional l
  2. L78
    specialize beta_sum_functional n
  3. L79
    specialize beta_sum_functional m
  4. L80
    apply beta_sum_functional
  5. L81
    exact htransport
  6. L82
    exact hm_witness_witness_right

Library-wide reading audit

Original exact command ledger · 82 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hn
  9. 0009intro hm
  10. 0010cases hn
  11. 0011cases hn_witness
  12. 0012cases hn_witness_witness
  13. 0013cases hm
  14. 0014cases hm_witness
  15. 0015cases hm_witness_witness
  16. 0016have htransport : exists ff_u_dot_transport ff_v_dot_transport. ((((exists ff_h_dot_transport_start. ff_h_dot_transport_start + S (0) = S ((S (0)) * ff_v_dot_transport)) /\ exists ff_q_dot_transport_start. ff_u_dot_transport = ff_q_dot_transport_start * S ((S (0)) * ff_v_dot_transport) + (0))) /\ ((((exists ff_h_dot_transport_terminal. ff_h_dot_transport_terminal + S (n) = S ((S (l)) * ff_v_dot_transport)) /\ exists ff_q_dot_transport_terminal. ff_u_dot_transport = ff_q_dot_transport_terminal * S ((S (l)) * ff_v_dot_transport) + (n))) /\ forall ff_i_dot_transport. (exists ff_lt_dot_transport_bound. ff_lt_dot_transport_bound + S ff_i_dot_transport = l) -> exists ff_a_dot_transport ff_r_dot_transport ff_s_dot_transport. ((((exists ff_h_dot_transport_summand. ff_h_dot_transport_summand + S (ff_a_dot_transport) = S ((S (ff_i_dot_transport)) * x3)) /\ exists ff_q_dot_transport_summand. x2 = ff_q_dot_transport_summand * S ((S (ff_i_dot_transport)) * x3) + (ff_a_dot_transport))) /\ ((((exists ff_h_dot_transport_partial. ff_h_dot_transport_partial + S (ff_r_dot_transport) = S ((S (ff_i_dot_transport)) * ff_v_dot_transport)) /\ exists ff_q_dot_transport_partial. ff_u_dot_transport = ff_q_dot_transport_partial * S ((S (ff_i_dot_transport)) * ff_v_dot_transport) + (ff_r_dot_transport))) /\ ((((exists ff_h_dot_transport_successor. ff_h_dot_transport_successor + S (ff_s_dot_transport) = S ((S (S ff_i_dot_transport)) * ff_v_dot_transport)) /\ exists ff_q_dot_transport_successor. ff_u_dot_transport = ff_q_dot_transport_successor * S ((S (S ff_i_dot_transport)) * ff_v_dot_transport) + (ff_s_dot_transport))) /\ ff_s_dot_transport = ff_r_dot_transport + ff_a_dot_transport)))))
  17. 0017specialize beta_sum_transport_prefix x
  18. 0018specialize beta_sum_transport_prefix x1
  19. 0019specialize beta_sum_transport_prefix x2
  20. 0020specialize beta_sum_transport_prefix x3
  21. 0021specialize beta_sum_transport_prefix l
  22. 0022specialize beta_sum_transport_prefix n
  23. 0023apply beta_sum_transport_prefix
  24. 0024exact hn_witness_witness_right
  25. 0025intro i
  26. 0026intro a
  27. 0027intro hi
  28. 0028intro ha
  29. 0029have hleft : exists z. ((exists fs_h_dot_left. fs_h_dot_left + S (z) = S ((S (i)) * mc)) /\ exists fs_q_dot_left. mb = fs_q_dot_left * S ((S (i)) * mc) + (z))
  30. 0030specialize beta_at_exists mb
  31. 0031specialize beta_at_exists mc
  32. 0032specialize beta_at_exists i
  33. 0033exact beta_at_exists
  34. 0034cases hleft
  35. 0035have hright : exists z. ((exists fs_h_dot_right. fs_h_dot_right + S (z) = S ((S (i)) * sc)) /\ exists fs_q_dot_right. sb = fs_q_dot_right * S ((S (i)) * sc) + (z))
  36. 0036specialize beta_at_exists sb
  37. 0037specialize beta_at_exists sc
  38. 0038specialize beta_at_exists i
  39. 0039exact beta_at_exists
  40. 0040cases hright
  41. 0041have htarget : exists z. ((exists fs_h_dot_target. fs_h_dot_target + S (z) = S ((S (i)) * x3)) /\ exists fs_q_dot_target. x2 = fs_q_dot_target * S ((S (i)) * x3) + (z))
  42. 0042specialize beta_at_exists x2
  43. 0043specialize beta_at_exists x3
  44. 0044specialize beta_at_exists i
  45. 0045exact beta_at_exists
  46. 0046cases htarget
  47. 0047have hfirst : a = x4 * x5
  48. 0048specialize hn_witness_witness_left i
  49. 0049specialize hn_witness_witness_left x4
  50. 0050specialize hn_witness_witness_left x5
  51. 0051specialize hn_witness_witness_left a
  52. 0052apply hn_witness_witness_left
  53. 0053exact hi
  54. 0054exact hleft_witness
  55. 0055exact hright_witness
  56. 0056exact ha
  57. 0057have hsecond : x6 = x4 * x5
  58. 0058specialize hm_witness_witness_left i
  59. 0059specialize hm_witness_witness_left x4
  60. 0060specialize hm_witness_witness_left x5
  61. 0061specialize hm_witness_witness_left x6
  62. 0062apply hm_witness_witness_left
  63. 0063exact hi
  64. 0064exact hleft_witness
  65. 0065exact hright_witness
  66. 0066exact htarget_witness
  67. 0067have heq : a = x6
  68. 0068trans x4 * x5
  69. 0069exact hfirst
  70. 0070symm
  71. 0071exact hsecond
  72. 0072rewrite heq
  73. 0073rewrite heq
  74. 0074exact htarget_witness
  75. 0075specialize beta_sum_functional x2
  76. 0076specialize beta_sum_functional x3
  77. 0077specialize beta_sum_functional l
  78. 0078specialize beta_sum_functional n
  79. 0079specialize beta_sum_functional m
  80. 0080apply beta_sum_functional
  81. 0081exact htransport
  82. 0082exact hm_witness_witness_right

Separate complete second-wave branches: Full T13 proof · Alpha v27.