MK000C

multinomial_binomial_prefix_nonzero

Every actual multinomial binomial factor is strictly nonzero, including zero-valued input parts.

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. ∀ cb. ∀ cc. ∀ l. MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l) → ∀ x. ∀ y. Lt(x,l) → BetaAt(cb,cc,x,y) → ¬y = 0

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

Definition DAG

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

Actual proof prerequisites

beta_at_unique · checked external prerequisitechoose_positive · checked external prerequisitele_add_right · checked external prerequisite
Original expanded first-order statement 
forall b c sb sc cb cc l. (forall mkm_index_binpositive_source. (exists mkm_lt_binpositive_source_bound. mkm_lt_binpositive_source_bound + S (mkm_index_binpositive_source) = (l)) -> (exists mkm_value_binpositive_source_point mkm_partial_binpositive_source_point mkm_factor_binpositive_source_point. (((exists fs_h_mkm_binpositive_source_point_source. fs_h_mkm_binpositive_source_point_source + S (mkm_value_binpositive_source_point) = S ((S (mkm_index_binpositive_source)) * c)) /\ exists fs_q_mkm_binpositive_source_point_source. b = fs_q_mkm_binpositive_source_point_source * S ((S (mkm_index_binpositive_source)) * c) + (mkm_value_binpositive_source_point))) /\ ((((exists fs_h_mkm_binpositive_source_point_partial. fs_h_mkm_binpositive_source_point_partial + S (mkm_partial_binpositive_source_point) = S ((S (mkm_index_binpositive_source)) * sc)) /\ exists fs_q_mkm_binpositive_source_point_partial. sb = fs_q_mkm_binpositive_source_point_partial * S ((S (mkm_index_binpositive_source)) * sc) + (mkm_partial_binpositive_source_point))) /\ ((((exists bcf_lt_gap_mkm_binpositive_source_point_choose_out_of_range. bcf_lt_gap_mkm_binpositive_source_point_choose_out_of_range + S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point) = mkm_partial_binpositive_source_point) /\ mkm_factor_binpositive_source_point = 0) \/ ((exists bcf_le_gap_mkm_binpositive_source_point_choose_in_range. bcf_le_gap_mkm_binpositive_source_point_choose_in_range + (mkm_partial_binpositive_source_point) = mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point) /\ (exists bcf_row_code_code_mkm_binpositive_source_point_choose bcf_row_code_scale_mkm_binpositive_source_point_choose bcf_row_scale_code_mkm_binpositive_source_point_choose bcf_row_scale_scale_mkm_binpositive_source_point_choose bcf_row_code_mkm_binpositive_source_point_choose bcf_row_scale_mkm_binpositive_source_point_choose. ((forall bcf_row_index_mkm_binpositive_source_point_choose_table. (exists bcf_lt_gap_mkm_binpositive_source_point_choose_table_row_bound. bcf_lt_gap_mkm_binpositive_source_point_choose_table_row_bound + S (bcf_row_index_mkm_binpositive_source_point_choose_table) = S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) -> exists bcf_row_code_mkm_binpositive_source_point_choose_table bcf_row_scale_mkm_binpositive_source_point_choose_table. ((((exists bcf_height_mkm_binpositive_source_point_choose_table_decoded_row_code. bcf_height_mkm_binpositive_source_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binpositive_source_point_choose_table) = S ((S (bcf_row_index_mkm_binpositive_source_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binpositive_source_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_source_point_choose) + (bcf_row_code_mkm_binpositive_source_point_choose_table))) /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_table_decoded_row_scale. bcf_height_mkm_binpositive_source_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binpositive_source_point_choose_table) = S ((S (bcf_row_index_mkm_binpositive_source_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binpositive_source_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_source_point_choose) + (bcf_row_scale_mkm_binpositive_source_point_choose_table))) /\ ((bcf_row_index_mkm_binpositive_source_point_choose_table = 0 /\ (forall bcf_index_mkm_binpositive_source_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binpositive_source_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binpositive_source_point_choose_table_zero_row_bound + S (bcf_index_mkm_binpositive_source_point_choose_table_zero_row) = S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) -> exists bcf_value_mkm_binpositive_source_point_choose_table_zero_row. ((((exists bcf_height_mkm_binpositive_source_point_choose_table_zero_row_entry. bcf_height_mkm_binpositive_source_point_choose_table_zero_row_entry + S (bcf_value_mkm_binpositive_source_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binpositive_source_point_choose_table_zero_row)) * bcf_row_scale_mkm_binpositive_source_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_zero_row_entry. bcf_row_code_mkm_binpositive_source_point_choose_table = bcf_quotient_mkm_binpositive_source_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binpositive_source_point_choose_table_zero_row)) * bcf_row_scale_mkm_binpositive_source_point_choose_table) + (bcf_value_mkm_binpositive_source_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binpositive_source_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binpositive_source_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binpositive_source_point_choose_table_zero_row. bcf_index_mkm_binpositive_source_point_choose_table_zero_row = S bcf_predecessor_mkm_binpositive_source_point_choose_table_zero_row /\ bcf_value_mkm_binpositive_source_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binpositive_source_point_choose_table bcf_previous_code_mkm_binpositive_source_point_choose_table bcf_previous_scale_mkm_binpositive_source_point_choose_table. bcf_row_index_mkm_binpositive_source_point_choose_table = S bcf_predecessor_mkm_binpositive_source_point_choose_table /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_table_decoded_previous_code. bcf_height_mkm_binpositive_source_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binpositive_source_point_choose_table) = S ((S (bcf_predecessor_mkm_binpositive_source_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binpositive_source_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_source_point_choose) + (bcf_previous_code_mkm_binpositive_source_point_choose_table))) /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_table_decoded_previous_scale. bcf_height_mkm_binpositive_source_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binpositive_source_point_choose_table) = S ((S (bcf_predecessor_mkm_binpositive_source_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binpositive_source_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_source_point_choose) + (bcf_previous_scale_mkm_binpositive_source_point_choose_table))) /\ (forall bcf_index_mkm_binpositive_source_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binpositive_source_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binpositive_source_point_choose_table_row_step_bound + S (bcf_index_mkm_binpositive_source_point_choose_table_row_step) = S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) -> exists bcf_value_mkm_binpositive_source_point_choose_table_row_step. ((((exists bcf_height_mkm_binpositive_source_point_choose_table_row_step_entry. bcf_height_mkm_binpositive_source_point_choose_table_row_step_entry + S (bcf_value_mkm_binpositive_source_point_choose_table_row_step) = S ((S (bcf_index_mkm_binpositive_source_point_choose_table_row_step)) * bcf_row_scale_mkm_binpositive_source_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_row_step_entry. bcf_row_code_mkm_binpositive_source_point_choose_table = bcf_quotient_mkm_binpositive_source_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binpositive_source_point_choose_table_row_step)) * bcf_row_scale_mkm_binpositive_source_point_choose_table) + (bcf_value_mkm_binpositive_source_point_choose_table_row_step))) /\ ((bcf_index_mkm_binpositive_source_point_choose_table_row_step = 0 /\ bcf_value_mkm_binpositive_source_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binpositive_source_point_choose_table_row_step bcf_left_mkm_binpositive_source_point_choose_table_row_step bcf_right_mkm_binpositive_source_point_choose_table_row_step. bcf_index_mkm_binpositive_source_point_choose_table_row_step = S bcf_predecessor_mkm_binpositive_source_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_table_row_step_previous_left. bcf_height_mkm_binpositive_source_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binpositive_source_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binpositive_source_point_choose_table_row_step)) * bcf_previous_scale_mkm_binpositive_source_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binpositive_source_point_choose_table = bcf_quotient_mkm_binpositive_source_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binpositive_source_point_choose_table_row_step)) * bcf_previous_scale_mkm_binpositive_source_point_choose_table) + (bcf_left_mkm_binpositive_source_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_table_row_step_previous_right. bcf_height_mkm_binpositive_source_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binpositive_source_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binpositive_source_point_choose_table_row_step))) * bcf_previous_scale_mkm_binpositive_source_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binpositive_source_point_choose_table = bcf_quotient_mkm_binpositive_source_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binpositive_source_point_choose_table_row_step))) * bcf_previous_scale_mkm_binpositive_source_point_choose_table) + (bcf_right_mkm_binpositive_source_point_choose_table_row_step))) /\ bcf_value_mkm_binpositive_source_point_choose_table_row_step = bcf_left_mkm_binpositive_source_point_choose_table_row_step + bcf_right_mkm_binpositive_source_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_decoded_row_code. bcf_height_mkm_binpositive_source_point_choose_decoded_row_code + S (bcf_row_code_mkm_binpositive_source_point_choose) = S ((S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) * bcf_row_code_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_decoded_row_code. bcf_row_code_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_decoded_row_code * S ((S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) * bcf_row_code_scale_mkm_binpositive_source_point_choose) + (bcf_row_code_mkm_binpositive_source_point_choose))) /\ ((((exists bcf_height_mkm_binpositive_source_point_choose_decoded_row_scale. bcf_height_mkm_binpositive_source_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binpositive_source_point_choose) = S ((S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) * bcf_row_scale_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_decoded_row_scale * S ((S (mkm_partial_binpositive_source_point + mkm_value_binpositive_source_point)) * bcf_row_scale_scale_mkm_binpositive_source_point_choose) + (bcf_row_scale_mkm_binpositive_source_point_choose))) /\ (((exists bcf_height_mkm_binpositive_source_point_choose_decoded_value. bcf_height_mkm_binpositive_source_point_choose_decoded_value + S (mkm_factor_binpositive_source_point) = S ((S (mkm_partial_binpositive_source_point)) * bcf_row_scale_mkm_binpositive_source_point_choose)) /\ exists bcf_quotient_mkm_binpositive_source_point_choose_decoded_value. bcf_row_code_mkm_binpositive_source_point_choose = bcf_quotient_mkm_binpositive_source_point_choose_decoded_value * S ((S (mkm_partial_binpositive_source_point)) * bcf_row_scale_mkm_binpositive_source_point_choose) + (mkm_factor_binpositive_source_point))))))))) /\ (((exists fs_h_mkm_binpositive_source_point_factor. fs_h_mkm_binpositive_source_point_factor + S (mkm_factor_binpositive_source_point) = S ((S (mkm_index_binpositive_source)) * cc)) /\ exists fs_q_mkm_binpositive_source_point_factor. cb = fs_q_mkm_binpositive_source_point_factor * S ((S (mkm_index_binpositive_source)) * cc) + (mkm_factor_binpositive_source_point))))))) -> (forall gcrt_positive_index_mkm_binpositive_target gcrt_positive_value_mkm_binpositive_target. (exists ff_lt_gcrt_mkm_binpositive_target_bound. ff_lt_gcrt_mkm_binpositive_target_bound + S gcrt_positive_index_mkm_binpositive_target = l) -> (((exists ff_h_gcrt_mkm_binpositive_target_entry. ff_h_gcrt_mkm_binpositive_target_entry + S (gcrt_positive_value_mkm_binpositive_target) = S ((S (gcrt_positive_index_mkm_binpositive_target)) * cc)) /\ exists ff_q_gcrt_mkm_binpositive_target_entry. cb = ff_q_gcrt_mkm_binpositive_target_entry * S ((S (gcrt_positive_index_mkm_binpositive_target)) * cc) + (gcrt_positive_value_mkm_binpositive_target))) -> ~(gcrt_positive_value_mkm_binpositive_target = 0))

Complete tactic proof in conservative notation

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

51 script commands · 8 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.

01Fix variables and assumptionsL1–10

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
  5. L5
    intro cb
  6. L6
    intro cc
  7. L7
    intro l
  8. L8
    intro h
  9. L9
    intro i
  10. L10
    intro C
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hi
  2. L12
    intro hC
  3. L13
    intro hzero
03Establish hpointL14–17

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

  1. L14
    have hpoint : ∃ mkm_value_binpositive_point. ∃ mkm_partial_binpositive_point. ∃ mkm_factor_binpositive_point. BetaAt(b,c,i,mkm_value_binpositive_point) ∧ (BetaAt(sb,sc,i,mkm_partial_binpositive_point) ∧ (Choose(mkm_partial_binpositive_point + mkm_value_binpositive_point,mkm_partial_binpositive_point,mkm_factor_binpositive_point) ∧ BetaAt(cb,cc,i,mkm_factor_binpositive_point)))Definitions: BetaAt(b,c,i,mkm_value_binpositive_point)BetaAt(sb,sc,i,mkm_partial_binpositive_point)Choose(mkm_partial_binpositive_point + mkm_value_binpositive_point,mkm_partial_binpositive_point,mkm_factor_binpositive_point)BetaAt(cb,cc,i,mkm_factor_binpositive_point)Original native command in the exact edition
  2. L15
    specialize h i
  3. L16
    apply h
  4. L17
    exact hi
04Separate the logical casesL18–23

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

  1. L18
    cases hpoint
  2. L19
    cases hpoint_witness
  3. L20
    cases hpoint_witness_witness
  4. L21
    cases hpoint_witness_witness_witness
  5. L22
    cases hpoint_witness_witness_witness_right
  6. L23
    cases hpoint_witness_witness_witness_right_right
05Establish hfactorL24–32

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

  1. L24
    have hfactor : x2 = C
  2. L25
    specialize beta_at_unique cb
  3. L26
    specialize beta_at_unique cc
  4. L27
    specialize beta_at_unique i
  5. L28
    specialize beta_at_unique x2
  6. L29
    specialize beta_at_unique C
  7. L30
    apply beta_at_unique
  8. L31
    exact hpoint_witness_witness_witness_right_right_right
  9. L32
    exact hC
06Establish hpositiveL33–41

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

  1. L33
    have hpositive : exists q. x2 = S q
  2. L34
    specialize choose_positive (x1 + x)
  3. L35
    specialize choose_positive x1
  4. L36
    specialize choose_positive x2
  5. L37
    apply choose_positive
  6. L38
    specialize le_add_right x1
  7. L39
    specialize le_add_right x
  8. L40
    apply le_add_right
  9. L41
    exact hpoint_witness_witness_witness_right_right_left
07Separate the logical casesL42–42

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

  1. L42
    cases hpositive
08Establish hsuccL43–51

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

  1. L43
    have hsucc : S x3 = 0
  2. L44
    trans x2
  3. L45
    symm
  4. L46
    exact hpositive_witness
  5. L47
    trans C
  6. L48
    exact hfactor
  7. L49
    exact hzero
  8. L50
    apply PA1
  9. L51
    exact hsucc

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro cb
  6. 0006intro cc
  7. 0007intro l
  8. 0008intro h
  9. 0009intro i
  10. 0010intro C
  11. 0011intro hi
  12. 0012intro hC
  13. 0013intro hzero
  14. 0014have hpoint : ∃ mkm_value_binpositive_point. ∃ mkm_partial_binpositive_point. ∃ mkm_factor_binpositive_point. BetaAt(b,c,i,mkm_value_binpositive_point) ∧ (BetaAt(sb,sc,i,mkm_partial_binpositive_point) ∧ (Choose(mkm_partial_binpositive_point + mkm_value_binpositive_point,mkm_partial_binpositive_point,mkm_factor_binpositive_point) ∧ BetaAt(cb,cc,i,mkm_factor_binpositive_point)))
  15. 0015specialize h i
  16. 0016apply h
  17. 0017exact hi
  18. 0018cases hpoint
  19. 0019cases hpoint_witness
  20. 0020cases hpoint_witness_witness
  21. 0021cases hpoint_witness_witness_witness
  22. 0022cases hpoint_witness_witness_witness_right
  23. 0023cases hpoint_witness_witness_witness_right_right
  24. 0024have hfactor : x2 = C
  25. 0025specialize beta_at_unique cb
  26. 0026specialize beta_at_unique cc
  27. 0027specialize beta_at_unique i
  28. 0028specialize beta_at_unique x2
  29. 0029specialize beta_at_unique C
  30. 0030apply beta_at_unique
  31. 0031exact hpoint_witness_witness_witness_right_right_right
  32. 0032exact hC
  33. 0033have hpositive : exists q. x2 = S q
  34. 0034specialize choose_positive (x1 + x)
  35. 0035specialize choose_positive x1
  36. 0036specialize choose_positive x2
  37. 0037apply choose_positive
  38. 0038specialize le_add_right x1
  39. 0039specialize le_add_right x
  40. 0040apply le_add_right
  41. 0041exact hpoint_witness_witness_witness_right_right_left
  42. 0042cases hpositive
  43. 0043have hsucc : S x3 = 0
  44. 0044trans x2
  45. 0045symm
  46. 0046exact hpositive_witness
  47. 0047trans C
  48. 0048exact hfactor
  49. 0049exact hzero
  50. 0050apply PA1
  51. 0051exact hsucc