MK000B

multinomial_binomial_prefix_exists

Construct all actual binomial factors for any finite decoded part and partial-sum tables.

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 carry relation contains actual quotient columns and carry bits, not the desired valuation. The theorem includes all finite lists and zero parts. It uses sequential binary-column carries; a separate simultaneous-grid or permutation-invariance theorem is not asserted.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ sb. ∀ sc. ∀ l. ∃ cb. ∃ cc. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)

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

Definition DAG

MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l) · 2BetaAt(b,c,i,x) · 2Choose(n,k,z) · 1

Actual proof prerequisites

multinomial_binomial_prefix_emptybeta_at_exists · checked external prerequisitechoose_exists · checked external prerequisitemultinomial_binomial_prefix_extend
Original expanded first-order statement 
forall b c sb sc l. exists cb cc. (forall mkm_index_binexists_target. (exists mkm_lt_binexists_target_bound. mkm_lt_binexists_target_bound + S (mkm_index_binexists_target) = (l)) -> (exists mkm_value_binexists_target_point mkm_partial_binexists_target_point mkm_factor_binexists_target_point. (((exists fs_h_mkm_binexists_target_point_source. fs_h_mkm_binexists_target_point_source + S (mkm_value_binexists_target_point) = S ((S (mkm_index_binexists_target)) * c)) /\ exists fs_q_mkm_binexists_target_point_source. b = fs_q_mkm_binexists_target_point_source * S ((S (mkm_index_binexists_target)) * c) + (mkm_value_binexists_target_point))) /\ ((((exists fs_h_mkm_binexists_target_point_partial. fs_h_mkm_binexists_target_point_partial + S (mkm_partial_binexists_target_point) = S ((S (mkm_index_binexists_target)) * sc)) /\ exists fs_q_mkm_binexists_target_point_partial. sb = fs_q_mkm_binexists_target_point_partial * S ((S (mkm_index_binexists_target)) * sc) + (mkm_partial_binexists_target_point))) /\ ((((exists bcf_lt_gap_mkm_binexists_target_point_choose_out_of_range. bcf_lt_gap_mkm_binexists_target_point_choose_out_of_range + S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point) = mkm_partial_binexists_target_point) /\ mkm_factor_binexists_target_point = 0) \/ ((exists bcf_le_gap_mkm_binexists_target_point_choose_in_range. bcf_le_gap_mkm_binexists_target_point_choose_in_range + (mkm_partial_binexists_target_point) = mkm_partial_binexists_target_point + mkm_value_binexists_target_point) /\ (exists bcf_row_code_code_mkm_binexists_target_point_choose bcf_row_code_scale_mkm_binexists_target_point_choose bcf_row_scale_code_mkm_binexists_target_point_choose bcf_row_scale_scale_mkm_binexists_target_point_choose bcf_row_code_mkm_binexists_target_point_choose bcf_row_scale_mkm_binexists_target_point_choose. ((forall bcf_row_index_mkm_binexists_target_point_choose_table. (exists bcf_lt_gap_mkm_binexists_target_point_choose_table_row_bound. bcf_lt_gap_mkm_binexists_target_point_choose_table_row_bound + S (bcf_row_index_mkm_binexists_target_point_choose_table) = S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) -> exists bcf_row_code_mkm_binexists_target_point_choose_table bcf_row_scale_mkm_binexists_target_point_choose_table. ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_row_code. bcf_height_mkm_binexists_target_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binexists_target_point_choose_table) = S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose) + (bcf_row_code_mkm_binexists_target_point_choose_table))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_row_scale. bcf_height_mkm_binexists_target_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binexists_target_point_choose_table) = S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose) + (bcf_row_scale_mkm_binexists_target_point_choose_table))) /\ ((bcf_row_index_mkm_binexists_target_point_choose_table = 0 /\ (forall bcf_index_mkm_binexists_target_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binexists_target_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binexists_target_point_choose_table_zero_row_bound + S (bcf_index_mkm_binexists_target_point_choose_table_zero_row) = S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) -> exists bcf_value_mkm_binexists_target_point_choose_table_zero_row. ((((exists bcf_height_mkm_binexists_target_point_choose_table_zero_row_entry. bcf_height_mkm_binexists_target_point_choose_table_zero_row_entry + S (bcf_value_mkm_binexists_target_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binexists_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_zero_row_entry. bcf_row_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binexists_target_point_choose_table_zero_row)) * bcf_row_scale_mkm_binexists_target_point_choose_table) + (bcf_value_mkm_binexists_target_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binexists_target_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binexists_target_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binexists_target_point_choose_table_zero_row. bcf_index_mkm_binexists_target_point_choose_table_zero_row = S bcf_predecessor_mkm_binexists_target_point_choose_table_zero_row /\ bcf_value_mkm_binexists_target_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binexists_target_point_choose_table bcf_previous_code_mkm_binexists_target_point_choose_table bcf_previous_scale_mkm_binexists_target_point_choose_table. bcf_row_index_mkm_binexists_target_point_choose_table = S bcf_predecessor_mkm_binexists_target_point_choose_table /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_code. bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binexists_target_point_choose_table) = S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_code_scale_mkm_binexists_target_point_choose) + (bcf_previous_code_mkm_binexists_target_point_choose_table))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_scale. bcf_height_mkm_binexists_target_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binexists_target_point_choose_table) = S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table)) * bcf_row_scale_scale_mkm_binexists_target_point_choose) + (bcf_previous_scale_mkm_binexists_target_point_choose_table))) /\ (forall bcf_index_mkm_binexists_target_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binexists_target_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binexists_target_point_choose_table_row_step_bound + S (bcf_index_mkm_binexists_target_point_choose_table_row_step) = S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) -> exists bcf_value_mkm_binexists_target_point_choose_table_row_step. ((((exists bcf_height_mkm_binexists_target_point_choose_table_row_step_entry. bcf_height_mkm_binexists_target_point_choose_table_row_step_entry + S (bcf_value_mkm_binexists_target_point_choose_table_row_step) = S ((S (bcf_index_mkm_binexists_target_point_choose_table_row_step)) * bcf_row_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_row_step_entry. bcf_row_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binexists_target_point_choose_table_row_step)) * bcf_row_scale_mkm_binexists_target_point_choose_table) + (bcf_value_mkm_binexists_target_point_choose_table_row_step))) /\ ((bcf_index_mkm_binexists_target_point_choose_table_row_step = 0 /\ bcf_value_mkm_binexists_target_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binexists_target_point_choose_table_row_step bcf_left_mkm_binexists_target_point_choose_table_row_step bcf_right_mkm_binexists_target_point_choose_table_row_step. bcf_index_mkm_binexists_target_point_choose_table_row_step = S bcf_predecessor_mkm_binexists_target_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_left. bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binexists_target_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step)) * bcf_previous_scale_mkm_binexists_target_point_choose_table) + (bcf_left_mkm_binexists_target_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_right. bcf_height_mkm_binexists_target_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binexists_target_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_target_point_choose_table)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binexists_target_point_choose_table = bcf_quotient_mkm_binexists_target_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binexists_target_point_choose_table_row_step))) * bcf_previous_scale_mkm_binexists_target_point_choose_table) + (bcf_right_mkm_binexists_target_point_choose_table_row_step))) /\ bcf_value_mkm_binexists_target_point_choose_table_row_step = bcf_left_mkm_binexists_target_point_choose_table_row_step + bcf_right_mkm_binexists_target_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_decoded_row_code. bcf_height_mkm_binexists_target_point_choose_decoded_row_code + S (bcf_row_code_mkm_binexists_target_point_choose) = S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_code_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_decoded_row_code. bcf_row_code_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_decoded_row_code * S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_code_scale_mkm_binexists_target_point_choose) + (bcf_row_code_mkm_binexists_target_point_choose))) /\ ((((exists bcf_height_mkm_binexists_target_point_choose_decoded_row_scale. bcf_height_mkm_binexists_target_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binexists_target_point_choose) = S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_scale_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_decoded_row_scale * S ((S (mkm_partial_binexists_target_point + mkm_value_binexists_target_point)) * bcf_row_scale_scale_mkm_binexists_target_point_choose) + (bcf_row_scale_mkm_binexists_target_point_choose))) /\ (((exists bcf_height_mkm_binexists_target_point_choose_decoded_value. bcf_height_mkm_binexists_target_point_choose_decoded_value + S (mkm_factor_binexists_target_point) = S ((S (mkm_partial_binexists_target_point)) * bcf_row_scale_mkm_binexists_target_point_choose)) /\ exists bcf_quotient_mkm_binexists_target_point_choose_decoded_value. bcf_row_code_mkm_binexists_target_point_choose = bcf_quotient_mkm_binexists_target_point_choose_decoded_value * S ((S (mkm_partial_binexists_target_point)) * bcf_row_scale_mkm_binexists_target_point_choose) + (mkm_factor_binexists_target_point))))))))) /\ (((exists fs_h_mkm_binexists_target_point_factor. fs_h_mkm_binexists_target_point_factor + S (mkm_factor_binexists_target_point) = S ((S (mkm_index_binexists_target)) * cc)) /\ exists fs_q_mkm_binexists_target_point_factor. cb = fs_q_mkm_binexists_target_point_factor * S ((S (mkm_index_binexists_target)) * cc) + (mkm_factor_binexists_target_point)))))))

Complete tactic proof in conservative notation

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

50 script commands · 14 reading checkpoints · 4 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.

Named ingredients (2)
multinomial binomial prefix emptymultinomial binomial prefix extend
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro sb
  4. L4
    intro sc
02Induction on lL5–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction l
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Use earlier factsL8–14

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

  1. L8
    specialize multinomial_binomial_prefix_empty b
  2. L9
    specialize multinomial_binomial_prefix_empty c
  3. L10
    specialize multinomial_binomial_prefix_empty sb
  4. L11
    specialize multinomial_binomial_prefix_empty sc
  5. L12
    specialize multinomial_binomial_prefix_empty 0
  6. L13
    specialize multinomial_binomial_prefix_empty 0
  7. L14
    apply multinomial_binomial_prefix_empty
05Establish hprefixL15–16

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

  1. L15
    have hprefix : ∃ cb. ∃ cc. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)Definitions: MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)Original native command in the exact edition
  2. L16
    apply IH
06Separate the logical casesL17–18

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

  1. L17
    cases hprefix
  2. L18
    cases hprefix_witness
07Establish hpartL19–23

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

  1. L19
    have hpart : ∃ a. BetaAt(b,c,l,a)Definitions: BetaAt(b,c,l,a)Original native command in the exact edition
  2. L20
    specialize beta_at_exists b
  3. L21
    specialize beta_at_exists c
  4. L22
    specialize beta_at_exists l
  5. L23
    apply beta_at_exists
08Separate the logical casesL24–24

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

  1. L24
    cases hpart
09Establish hpartialL25–29

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

  1. L25
    have hpartial : ∃ u. BetaAt(sb,sc,l,u)Definitions: BetaAt(sb,sc,l,u)Original native command in the exact edition
  2. L26
    specialize beta_at_exists sb
  3. L27
    specialize beta_at_exists sc
  4. L28
    specialize beta_at_exists l
  5. L29
    apply beta_at_exists
10Separate the logical casesL30–30

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

  1. L30
    cases hpartial
11Establish hchooseL31–34

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

  1. L31
    have hchoose : ∃ C. Choose(x3 + x2,x3,C)Definitions: Choose(x3 + x2,x3,C)Original native command in the exact edition
  2. L32
    specialize choose_exists (x3 + x2)
  3. L33
    specialize choose_exists x3
  4. L34
    apply choose_exists
12Separate the logical casesL35–35

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

  1. L35
    cases hchoose
13Use earlier factsL36–45

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

  1. L36
    specialize multinomial_binomial_prefix_extend b
  2. L37
    specialize multinomial_binomial_prefix_extend c
  3. L38
    specialize multinomial_binomial_prefix_extend sb
  4. L39
    specialize multinomial_binomial_prefix_extend sc
  5. L40
    specialize multinomial_binomial_prefix_extend x
  6. L41
    specialize multinomial_binomial_prefix_extend x1
  7. L42
    specialize multinomial_binomial_prefix_extend l
  8. L43
    specialize multinomial_binomial_prefix_extend x2
  9. L44
    specialize multinomial_binomial_prefix_extend x3
  10. L45
    specialize multinomial_binomial_prefix_extend x4
14Use earlier factsL46–50

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

  1. L46
    apply multinomial_binomial_prefix_extend
  2. L47
    exact hprefix_witness_witness
  3. L48
    exact hpart_witness
  4. L49
    exact hpartial_witness
  5. L50
    exact hchoose_witness

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro sb
  4. 0004intro sc
  5. 0005induction l
  6. 0006exists 0
  7. 0007exists 0
  8. 0008specialize multinomial_binomial_prefix_empty b
  9. 0009specialize multinomial_binomial_prefix_empty c
  10. 0010specialize multinomial_binomial_prefix_empty sb
  11. 0011specialize multinomial_binomial_prefix_empty sc
  12. 0012specialize multinomial_binomial_prefix_empty 0
  13. 0013specialize multinomial_binomial_prefix_empty 0
  14. 0014apply multinomial_binomial_prefix_empty
  15. 0015have hprefix : ∃ cb. ∃ cc. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)
  16. 0016apply IH
  17. 0017cases hprefix
  18. 0018cases hprefix_witness
  19. 0019have hpart : ∃ a. BetaAt(b,c,l,a)
  20. 0020specialize beta_at_exists b
  21. 0021specialize beta_at_exists c
  22. 0022specialize beta_at_exists l
  23. 0023apply beta_at_exists
  24. 0024cases hpart
  25. 0025have hpartial : ∃ u. BetaAt(sb,sc,l,u)
  26. 0026specialize beta_at_exists sb
  27. 0027specialize beta_at_exists sc
  28. 0028specialize beta_at_exists l
  29. 0029apply beta_at_exists
  30. 0030cases hpartial
  31. 0031have hchoose : ∃ C. Choose(x3 + x2,x3,C)
  32. 0032specialize choose_exists (x3 + x2)
  33. 0033specialize choose_exists x3
  34. 0034apply choose_exists
  35. 0035cases hchoose
  36. 0036specialize multinomial_binomial_prefix_extend b
  37. 0037specialize multinomial_binomial_prefix_extend c
  38. 0038specialize multinomial_binomial_prefix_extend sb
  39. 0039specialize multinomial_binomial_prefix_extend sc
  40. 0040specialize multinomial_binomial_prefix_extend x
  41. 0041specialize multinomial_binomial_prefix_extend x1
  42. 0042specialize multinomial_binomial_prefix_extend l
  43. 0043specialize multinomial_binomial_prefix_extend x2
  44. 0044specialize multinomial_binomial_prefix_extend x3
  45. 0045specialize multinomial_binomial_prefix_extend x4
  46. 0046apply multinomial_binomial_prefix_extend
  47. 0047exact hprefix_witness_witness
  48. 0048exact hpart_witness
  49. 0049exact hpartial_witness
  50. 0050exact hchoose_witness