MK000C

multinomial_binomial_prefix_nonzero

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

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

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 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))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized choose_positive Alpha theorem; checked-use authorized le_add_right Stable theorem; checked-use authorized

Direct dependents

MK000F multinomial_nonzero MK0011 multinomial_kummer_carry_valuation

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

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.

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–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: BetaAtChoose
  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 exact 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 : exists mkm_value_binpositive_point mkm_partial_binpositive_point mkm_factor_binpositive_point. (((exists fs_h_mkm_binpositive_point_source. fs_h_mkm_binpositive_point_source + S (mkm_value_binpositive_point) = S ((S (i)) * c)) /\ exists fs_q_mkm_binpositive_point_source. b = fs_q_mkm_binpositive_point_source * S ((S (i)) * c) + (mkm_value_binpositive_point))) /\ ((((exists fs_h_mkm_binpositive_point_partial. fs_h_mkm_binpositive_point_partial + S (mkm_partial_binpositive_point) = S ((S (i)) * sc)) /\ exists fs_q_mkm_binpositive_point_partial. sb = fs_q_mkm_binpositive_point_partial * S ((S (i)) * sc) + (mkm_partial_binpositive_point))) /\ ((((exists bcf_lt_gap_mkm_binpositive_point_choose_out_of_range. bcf_lt_gap_mkm_binpositive_point_choose_out_of_range + S (mkm_partial_binpositive_point + mkm_value_binpositive_point) = mkm_partial_binpositive_point) /\ mkm_factor_binpositive_point = 0) \/ ((exists bcf_le_gap_mkm_binpositive_point_choose_in_range. bcf_le_gap_mkm_binpositive_point_choose_in_range + (mkm_partial_binpositive_point) = mkm_partial_binpositive_point + mkm_value_binpositive_point) /\ (exists bcf_row_code_code_mkm_binpositive_point_choose bcf_row_code_scale_mkm_binpositive_point_choose bcf_row_scale_code_mkm_binpositive_point_choose bcf_row_scale_scale_mkm_binpositive_point_choose bcf_row_code_mkm_binpositive_point_choose bcf_row_scale_mkm_binpositive_point_choose. ((forall bcf_row_index_mkm_binpositive_point_choose_table. (exists bcf_lt_gap_mkm_binpositive_point_choose_table_row_bound. bcf_lt_gap_mkm_binpositive_point_choose_table_row_bound + S (bcf_row_index_mkm_binpositive_point_choose_table) = S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) -> exists bcf_row_code_mkm_binpositive_point_choose_table bcf_row_scale_mkm_binpositive_point_choose_table. ((((exists bcf_height_mkm_binpositive_point_choose_table_decoded_row_code. bcf_height_mkm_binpositive_point_choose_table_decoded_row_code + S (bcf_row_code_mkm_binpositive_point_choose_table) = S ((S (bcf_row_index_mkm_binpositive_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_decoded_row_code. bcf_row_code_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_table_decoded_row_code * S ((S (bcf_row_index_mkm_binpositive_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_point_choose) + (bcf_row_code_mkm_binpositive_point_choose_table))) /\ ((((exists bcf_height_mkm_binpositive_point_choose_table_decoded_row_scale. bcf_height_mkm_binpositive_point_choose_table_decoded_row_scale + S (bcf_row_scale_mkm_binpositive_point_choose_table) = S ((S (bcf_row_index_mkm_binpositive_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_decoded_row_scale. bcf_row_scale_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_table_decoded_row_scale * S ((S (bcf_row_index_mkm_binpositive_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_point_choose) + (bcf_row_scale_mkm_binpositive_point_choose_table))) /\ ((bcf_row_index_mkm_binpositive_point_choose_table = 0 /\ (forall bcf_index_mkm_binpositive_point_choose_table_zero_row. (exists bcf_lt_gap_mkm_binpositive_point_choose_table_zero_row_bound. bcf_lt_gap_mkm_binpositive_point_choose_table_zero_row_bound + S (bcf_index_mkm_binpositive_point_choose_table_zero_row) = S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) -> exists bcf_value_mkm_binpositive_point_choose_table_zero_row. ((((exists bcf_height_mkm_binpositive_point_choose_table_zero_row_entry. bcf_height_mkm_binpositive_point_choose_table_zero_row_entry + S (bcf_value_mkm_binpositive_point_choose_table_zero_row) = S ((S (bcf_index_mkm_binpositive_point_choose_table_zero_row)) * bcf_row_scale_mkm_binpositive_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_zero_row_entry. bcf_row_code_mkm_binpositive_point_choose_table = bcf_quotient_mkm_binpositive_point_choose_table_zero_row_entry * S ((S (bcf_index_mkm_binpositive_point_choose_table_zero_row)) * bcf_row_scale_mkm_binpositive_point_choose_table) + (bcf_value_mkm_binpositive_point_choose_table_zero_row))) /\ ((bcf_index_mkm_binpositive_point_choose_table_zero_row = 0 /\ bcf_value_mkm_binpositive_point_choose_table_zero_row = 1) \/ exists bcf_predecessor_mkm_binpositive_point_choose_table_zero_row. bcf_index_mkm_binpositive_point_choose_table_zero_row = S bcf_predecessor_mkm_binpositive_point_choose_table_zero_row /\ bcf_value_mkm_binpositive_point_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_mkm_binpositive_point_choose_table bcf_previous_code_mkm_binpositive_point_choose_table bcf_previous_scale_mkm_binpositive_point_choose_table. bcf_row_index_mkm_binpositive_point_choose_table = S bcf_predecessor_mkm_binpositive_point_choose_table /\ ((((exists bcf_height_mkm_binpositive_point_choose_table_decoded_previous_code. bcf_height_mkm_binpositive_point_choose_table_decoded_previous_code + S (bcf_previous_code_mkm_binpositive_point_choose_table) = S ((S (bcf_predecessor_mkm_binpositive_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_decoded_previous_code. bcf_row_code_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_table_decoded_previous_code * S ((S (bcf_predecessor_mkm_binpositive_point_choose_table)) * bcf_row_code_scale_mkm_binpositive_point_choose) + (bcf_previous_code_mkm_binpositive_point_choose_table))) /\ ((((exists bcf_height_mkm_binpositive_point_choose_table_decoded_previous_scale. bcf_height_mkm_binpositive_point_choose_table_decoded_previous_scale + S (bcf_previous_scale_mkm_binpositive_point_choose_table) = S ((S (bcf_predecessor_mkm_binpositive_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_decoded_previous_scale. bcf_row_scale_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_mkm_binpositive_point_choose_table)) * bcf_row_scale_scale_mkm_binpositive_point_choose) + (bcf_previous_scale_mkm_binpositive_point_choose_table))) /\ (forall bcf_index_mkm_binpositive_point_choose_table_row_step. (exists bcf_lt_gap_mkm_binpositive_point_choose_table_row_step_bound. bcf_lt_gap_mkm_binpositive_point_choose_table_row_step_bound + S (bcf_index_mkm_binpositive_point_choose_table_row_step) = S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) -> exists bcf_value_mkm_binpositive_point_choose_table_row_step. ((((exists bcf_height_mkm_binpositive_point_choose_table_row_step_entry. bcf_height_mkm_binpositive_point_choose_table_row_step_entry + S (bcf_value_mkm_binpositive_point_choose_table_row_step) = S ((S (bcf_index_mkm_binpositive_point_choose_table_row_step)) * bcf_row_scale_mkm_binpositive_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_row_step_entry. bcf_row_code_mkm_binpositive_point_choose_table = bcf_quotient_mkm_binpositive_point_choose_table_row_step_entry * S ((S (bcf_index_mkm_binpositive_point_choose_table_row_step)) * bcf_row_scale_mkm_binpositive_point_choose_table) + (bcf_value_mkm_binpositive_point_choose_table_row_step))) /\ ((bcf_index_mkm_binpositive_point_choose_table_row_step = 0 /\ bcf_value_mkm_binpositive_point_choose_table_row_step = 1) \/ exists bcf_predecessor_mkm_binpositive_point_choose_table_row_step bcf_left_mkm_binpositive_point_choose_table_row_step bcf_right_mkm_binpositive_point_choose_table_row_step. bcf_index_mkm_binpositive_point_choose_table_row_step = S bcf_predecessor_mkm_binpositive_point_choose_table_row_step /\ ((((exists bcf_height_mkm_binpositive_point_choose_table_row_step_previous_left. bcf_height_mkm_binpositive_point_choose_table_row_step_previous_left + S (bcf_left_mkm_binpositive_point_choose_table_row_step) = S ((S (bcf_predecessor_mkm_binpositive_point_choose_table_row_step)) * bcf_previous_scale_mkm_binpositive_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_row_step_previous_left. bcf_previous_code_mkm_binpositive_point_choose_table = bcf_quotient_mkm_binpositive_point_choose_table_row_step_previous_left * S ((S (bcf_predecessor_mkm_binpositive_point_choose_table_row_step)) * bcf_previous_scale_mkm_binpositive_point_choose_table) + (bcf_left_mkm_binpositive_point_choose_table_row_step))) /\ ((((exists bcf_height_mkm_binpositive_point_choose_table_row_step_previous_right. bcf_height_mkm_binpositive_point_choose_table_row_step_previous_right + S (bcf_right_mkm_binpositive_point_choose_table_row_step) = S ((S (S (bcf_predecessor_mkm_binpositive_point_choose_table_row_step))) * bcf_previous_scale_mkm_binpositive_point_choose_table)) /\ exists bcf_quotient_mkm_binpositive_point_choose_table_row_step_previous_right. bcf_previous_code_mkm_binpositive_point_choose_table = bcf_quotient_mkm_binpositive_point_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_mkm_binpositive_point_choose_table_row_step))) * bcf_previous_scale_mkm_binpositive_point_choose_table) + (bcf_right_mkm_binpositive_point_choose_table_row_step))) /\ bcf_value_mkm_binpositive_point_choose_table_row_step = bcf_left_mkm_binpositive_point_choose_table_row_step + bcf_right_mkm_binpositive_point_choose_table_row_step))))))))))) /\ ((((exists bcf_height_mkm_binpositive_point_choose_decoded_row_code. bcf_height_mkm_binpositive_point_choose_decoded_row_code + S (bcf_row_code_mkm_binpositive_point_choose) = S ((S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) * bcf_row_code_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_decoded_row_code. bcf_row_code_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_decoded_row_code * S ((S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) * bcf_row_code_scale_mkm_binpositive_point_choose) + (bcf_row_code_mkm_binpositive_point_choose))) /\ ((((exists bcf_height_mkm_binpositive_point_choose_decoded_row_scale. bcf_height_mkm_binpositive_point_choose_decoded_row_scale + S (bcf_row_scale_mkm_binpositive_point_choose) = S ((S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) * bcf_row_scale_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_decoded_row_scale. bcf_row_scale_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_decoded_row_scale * S ((S (mkm_partial_binpositive_point + mkm_value_binpositive_point)) * bcf_row_scale_scale_mkm_binpositive_point_choose) + (bcf_row_scale_mkm_binpositive_point_choose))) /\ (((exists bcf_height_mkm_binpositive_point_choose_decoded_value. bcf_height_mkm_binpositive_point_choose_decoded_value + S (mkm_factor_binpositive_point) = S ((S (mkm_partial_binpositive_point)) * bcf_row_scale_mkm_binpositive_point_choose)) /\ exists bcf_quotient_mkm_binpositive_point_choose_decoded_value. bcf_row_code_mkm_binpositive_point_choose = bcf_quotient_mkm_binpositive_point_choose_decoded_value * S ((S (mkm_partial_binpositive_point)) * bcf_row_scale_mkm_binpositive_point_choose) + (mkm_factor_binpositive_point))))))))) /\ (((exists fs_h_mkm_binpositive_point_factor. fs_h_mkm_binpositive_point_factor + S (mkm_factor_binpositive_point) = S ((S (i)) * cc)) /\ exists fs_q_mkm_binpositive_point_factor. cb = fs_q_mkm_binpositive_point_factor * S ((S (i)) * cc) + (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