BL0013

binary_length_functional

Two complete constructive binary-length witnesses for one input agree.

Alpha v34 checked-use · first admitted v22 · 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.

G101 and G102 were OPEN when these BitLen foundations were first admitted in Alpha v22. Both are now CLOSED in Alpha v23: complete canonical exponent digits and both exact logarithmic execution bounds are proved.

Exact theorem in conservative defined notation

∀ n. ∀ l. ∀ L. BitLen(n,l) → BitLen(n,L) → l = L

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

Definition DAG

BitLen(n,ell) · 2

Actual proof prerequisites

binary_length_zero_input_generalle_total · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisitebinary_power_two_exponent_monotonele_trans · checked external prerequisitelt_not_le · checked external prerequisite
Original expanded first-order statement 
forall n l L. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_length ff_lower_bl_length ff_upper_bl_length. (((l) = S ff_exponent_bl_length) /\ ((exists ff_positive_bl_length. ff_positive_bl_length + 1 = (n)) /\ ((exists pa_b_bl_length_lower pa_c_bl_length_lower. ((forall pa_i_bl_length_lower_repeat. (exists pa_lt_bl_length_lower_repeat_bound. pa_lt_bl_length_lower_repeat_bound + S pa_i_bl_length_lower_repeat = ff_exponent_bl_length) -> (((exists pa_h_bl_length_lower_repeat_decoded. pa_h_bl_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_length_lower_repeat)) * pa_c_bl_length_lower)) /\ exists pa_q_bl_length_lower_repeat_decoded. pa_b_bl_length_lower = pa_q_bl_length_lower_repeat_decoded * S ((S (pa_i_bl_length_lower_repeat)) * pa_c_bl_length_lower) + (2)))) /\ (exists pa_u_bl_length_lower_product pa_v_bl_length_lower_product. ((((exists pa_h_bl_length_lower_product_start. pa_h_bl_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_start. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_start * S ((S (0)) * pa_v_bl_length_lower_product) + (1))) /\ ((((exists pa_h_bl_length_lower_product_terminal. pa_h_bl_length_lower_product_terminal + S (ff_lower_bl_length) = S ((S (ff_exponent_bl_length)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_terminal. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_terminal * S ((S (ff_exponent_bl_length)) * pa_v_bl_length_lower_product) + (ff_lower_bl_length))) /\ forall pa_i_bl_length_lower_product. (exists pa_lt_bl_length_lower_product_bound. pa_lt_bl_length_lower_product_bound + S pa_i_bl_length_lower_product = ff_exponent_bl_length) -> exists pa_p_bl_length_lower_product pa_r_bl_length_lower_product pa_s_bl_length_lower_product. ((((exists pa_h_bl_length_lower_product_factor. pa_h_bl_length_lower_product_factor + S (pa_p_bl_length_lower_product) = S ((S (pa_i_bl_length_lower_product)) * pa_c_bl_length_lower)) /\ exists pa_q_bl_length_lower_product_factor. pa_b_bl_length_lower = pa_q_bl_length_lower_product_factor * S ((S (pa_i_bl_length_lower_product)) * pa_c_bl_length_lower) + (pa_p_bl_length_lower_product))) /\ ((((exists pa_h_bl_length_lower_product_partial. pa_h_bl_length_lower_product_partial + S (pa_r_bl_length_lower_product) = S ((S (pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_partial. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_partial * S ((S (pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product) + (pa_r_bl_length_lower_product))) /\ ((((exists pa_h_bl_length_lower_product_successor. pa_h_bl_length_lower_product_successor + S (pa_s_bl_length_lower_product) = S ((S (S pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_successor. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_successor * S ((S (S pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product) + (pa_s_bl_length_lower_product))) /\ pa_s_bl_length_lower_product = pa_r_bl_length_lower_product * pa_p_bl_length_lower_product)))))))) /\ ((exists pa_b_bl_length_upper pa_c_bl_length_upper. ((forall pa_i_bl_length_upper_repeat. (exists pa_lt_bl_length_upper_repeat_bound. pa_lt_bl_length_upper_repeat_bound + S pa_i_bl_length_upper_repeat = l) -> (((exists pa_h_bl_length_upper_repeat_decoded. pa_h_bl_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_length_upper_repeat)) * pa_c_bl_length_upper)) /\ exists pa_q_bl_length_upper_repeat_decoded. pa_b_bl_length_upper = pa_q_bl_length_upper_repeat_decoded * S ((S (pa_i_bl_length_upper_repeat)) * pa_c_bl_length_upper) + (2)))) /\ (exists pa_u_bl_length_upper_product pa_v_bl_length_upper_product. ((((exists pa_h_bl_length_upper_product_start. pa_h_bl_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_start. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_start * S ((S (0)) * pa_v_bl_length_upper_product) + (1))) /\ ((((exists pa_h_bl_length_upper_product_terminal. pa_h_bl_length_upper_product_terminal + S (ff_upper_bl_length) = S ((S (l)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_terminal. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_terminal * S ((S (l)) * pa_v_bl_length_upper_product) + (ff_upper_bl_length))) /\ forall pa_i_bl_length_upper_product. (exists pa_lt_bl_length_upper_product_bound. pa_lt_bl_length_upper_product_bound + S pa_i_bl_length_upper_product = l) -> exists pa_p_bl_length_upper_product pa_r_bl_length_upper_product pa_s_bl_length_upper_product. ((((exists pa_h_bl_length_upper_product_factor. pa_h_bl_length_upper_product_factor + S (pa_p_bl_length_upper_product) = S ((S (pa_i_bl_length_upper_product)) * pa_c_bl_length_upper)) /\ exists pa_q_bl_length_upper_product_factor. pa_b_bl_length_upper = pa_q_bl_length_upper_product_factor * S ((S (pa_i_bl_length_upper_product)) * pa_c_bl_length_upper) + (pa_p_bl_length_upper_product))) /\ ((((exists pa_h_bl_length_upper_product_partial. pa_h_bl_length_upper_product_partial + S (pa_r_bl_length_upper_product) = S ((S (pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_partial. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_partial * S ((S (pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product) + (pa_r_bl_length_upper_product))) /\ ((((exists pa_h_bl_length_upper_product_successor. pa_h_bl_length_upper_product_successor + S (pa_s_bl_length_upper_product) = S ((S (S pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_successor. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_successor * S ((S (S pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product) + (pa_s_bl_length_upper_product))) /\ pa_s_bl_length_upper_product = pa_r_bl_length_upper_product * pa_p_bl_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_length. ff_lower_gap_bl_length + (ff_lower_bl_length) = (n)) /\ (exists ff_upper_gap_bl_length. ff_upper_gap_bl_length + S (n) = (ff_upper_bl_length))))))))) -> ((((n) = 0 /\ (L) = 1) \/ exists ff_exponent_bl_other_length ff_lower_bl_other_length ff_upper_bl_other_length. (((L) = S ff_exponent_bl_other_length) /\ ((exists ff_positive_bl_other_length. ff_positive_bl_other_length + 1 = (n)) /\ ((exists pa_b_bl_other_length_lower pa_c_bl_other_length_lower. ((forall pa_i_bl_other_length_lower_repeat. (exists pa_lt_bl_other_length_lower_repeat_bound. pa_lt_bl_other_length_lower_repeat_bound + S pa_i_bl_other_length_lower_repeat = ff_exponent_bl_other_length) -> (((exists pa_h_bl_other_length_lower_repeat_decoded. pa_h_bl_other_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_other_length_lower_repeat)) * pa_c_bl_other_length_lower)) /\ exists pa_q_bl_other_length_lower_repeat_decoded. pa_b_bl_other_length_lower = pa_q_bl_other_length_lower_repeat_decoded * S ((S (pa_i_bl_other_length_lower_repeat)) * pa_c_bl_other_length_lower) + (2)))) /\ (exists pa_u_bl_other_length_lower_product pa_v_bl_other_length_lower_product. ((((exists pa_h_bl_other_length_lower_product_start. pa_h_bl_other_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_other_length_lower_product)) /\ exists pa_q_bl_other_length_lower_product_start. pa_u_bl_other_length_lower_product = pa_q_bl_other_length_lower_product_start * S ((S (0)) * pa_v_bl_other_length_lower_product) + (1))) /\ ((((exists pa_h_bl_other_length_lower_product_terminal. pa_h_bl_other_length_lower_product_terminal + S (ff_lower_bl_other_length) = S ((S (ff_exponent_bl_other_length)) * pa_v_bl_other_length_lower_product)) /\ exists pa_q_bl_other_length_lower_product_terminal. pa_u_bl_other_length_lower_product = pa_q_bl_other_length_lower_product_terminal * S ((S (ff_exponent_bl_other_length)) * pa_v_bl_other_length_lower_product) + (ff_lower_bl_other_length))) /\ forall pa_i_bl_other_length_lower_product. (exists pa_lt_bl_other_length_lower_product_bound. pa_lt_bl_other_length_lower_product_bound + S pa_i_bl_other_length_lower_product = ff_exponent_bl_other_length) -> exists pa_p_bl_other_length_lower_product pa_r_bl_other_length_lower_product pa_s_bl_other_length_lower_product. ((((exists pa_h_bl_other_length_lower_product_factor. pa_h_bl_other_length_lower_product_factor + S (pa_p_bl_other_length_lower_product) = S ((S (pa_i_bl_other_length_lower_product)) * pa_c_bl_other_length_lower)) /\ exists pa_q_bl_other_length_lower_product_factor. pa_b_bl_other_length_lower = pa_q_bl_other_length_lower_product_factor * S ((S (pa_i_bl_other_length_lower_product)) * pa_c_bl_other_length_lower) + (pa_p_bl_other_length_lower_product))) /\ ((((exists pa_h_bl_other_length_lower_product_partial. pa_h_bl_other_length_lower_product_partial + S (pa_r_bl_other_length_lower_product) = S ((S (pa_i_bl_other_length_lower_product)) * pa_v_bl_other_length_lower_product)) /\ exists pa_q_bl_other_length_lower_product_partial. pa_u_bl_other_length_lower_product = pa_q_bl_other_length_lower_product_partial * S ((S (pa_i_bl_other_length_lower_product)) * pa_v_bl_other_length_lower_product) + (pa_r_bl_other_length_lower_product))) /\ ((((exists pa_h_bl_other_length_lower_product_successor. pa_h_bl_other_length_lower_product_successor + S (pa_s_bl_other_length_lower_product) = S ((S (S pa_i_bl_other_length_lower_product)) * pa_v_bl_other_length_lower_product)) /\ exists pa_q_bl_other_length_lower_product_successor. pa_u_bl_other_length_lower_product = pa_q_bl_other_length_lower_product_successor * S ((S (S pa_i_bl_other_length_lower_product)) * pa_v_bl_other_length_lower_product) + (pa_s_bl_other_length_lower_product))) /\ pa_s_bl_other_length_lower_product = pa_r_bl_other_length_lower_product * pa_p_bl_other_length_lower_product)))))))) /\ ((exists pa_b_bl_other_length_upper pa_c_bl_other_length_upper. ((forall pa_i_bl_other_length_upper_repeat. (exists pa_lt_bl_other_length_upper_repeat_bound. pa_lt_bl_other_length_upper_repeat_bound + S pa_i_bl_other_length_upper_repeat = L) -> (((exists pa_h_bl_other_length_upper_repeat_decoded. pa_h_bl_other_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_other_length_upper_repeat)) * pa_c_bl_other_length_upper)) /\ exists pa_q_bl_other_length_upper_repeat_decoded. pa_b_bl_other_length_upper = pa_q_bl_other_length_upper_repeat_decoded * S ((S (pa_i_bl_other_length_upper_repeat)) * pa_c_bl_other_length_upper) + (2)))) /\ (exists pa_u_bl_other_length_upper_product pa_v_bl_other_length_upper_product. ((((exists pa_h_bl_other_length_upper_product_start. pa_h_bl_other_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_other_length_upper_product)) /\ exists pa_q_bl_other_length_upper_product_start. pa_u_bl_other_length_upper_product = pa_q_bl_other_length_upper_product_start * S ((S (0)) * pa_v_bl_other_length_upper_product) + (1))) /\ ((((exists pa_h_bl_other_length_upper_product_terminal. pa_h_bl_other_length_upper_product_terminal + S (ff_upper_bl_other_length) = S ((S (L)) * pa_v_bl_other_length_upper_product)) /\ exists pa_q_bl_other_length_upper_product_terminal. pa_u_bl_other_length_upper_product = pa_q_bl_other_length_upper_product_terminal * S ((S (L)) * pa_v_bl_other_length_upper_product) + (ff_upper_bl_other_length))) /\ forall pa_i_bl_other_length_upper_product. (exists pa_lt_bl_other_length_upper_product_bound. pa_lt_bl_other_length_upper_product_bound + S pa_i_bl_other_length_upper_product = L) -> exists pa_p_bl_other_length_upper_product pa_r_bl_other_length_upper_product pa_s_bl_other_length_upper_product. ((((exists pa_h_bl_other_length_upper_product_factor. pa_h_bl_other_length_upper_product_factor + S (pa_p_bl_other_length_upper_product) = S ((S (pa_i_bl_other_length_upper_product)) * pa_c_bl_other_length_upper)) /\ exists pa_q_bl_other_length_upper_product_factor. pa_b_bl_other_length_upper = pa_q_bl_other_length_upper_product_factor * S ((S (pa_i_bl_other_length_upper_product)) * pa_c_bl_other_length_upper) + (pa_p_bl_other_length_upper_product))) /\ ((((exists pa_h_bl_other_length_upper_product_partial. pa_h_bl_other_length_upper_product_partial + S (pa_r_bl_other_length_upper_product) = S ((S (pa_i_bl_other_length_upper_product)) * pa_v_bl_other_length_upper_product)) /\ exists pa_q_bl_other_length_upper_product_partial. pa_u_bl_other_length_upper_product = pa_q_bl_other_length_upper_product_partial * S ((S (pa_i_bl_other_length_upper_product)) * pa_v_bl_other_length_upper_product) + (pa_r_bl_other_length_upper_product))) /\ ((((exists pa_h_bl_other_length_upper_product_successor. pa_h_bl_other_length_upper_product_successor + S (pa_s_bl_other_length_upper_product) = S ((S (S pa_i_bl_other_length_upper_product)) * pa_v_bl_other_length_upper_product)) /\ exists pa_q_bl_other_length_upper_product_successor. pa_u_bl_other_length_upper_product = pa_q_bl_other_length_upper_product_successor * S ((S (S pa_i_bl_other_length_upper_product)) * pa_v_bl_other_length_upper_product) + (pa_s_bl_other_length_upper_product))) /\ pa_s_bl_other_length_upper_product = pa_r_bl_other_length_upper_product * pa_p_bl_other_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_other_length. ff_lower_gap_bl_other_length + (ff_lower_bl_other_length) = (n)) /\ (exists ff_upper_gap_bl_other_length. ff_upper_gap_bl_other_length + S (n) = (ff_upper_bl_other_length))))))))) -> l = L

Complete unchanged native tactic proof

All 120 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

120 script commands · 32 reading checkpoints · 10 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)
binary length zero input generalbinary power two exponent monotone
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro l
  3. L3
    intro L
  4. L4
    intro hfirst
  5. L5
    intro hsecond
02Separate the logical casesL6–7

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

  1. L6
    cases hfirst
  2. L7
    cases hfirst_left
03Establish hotherL8–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary length zero input general.

  1. L8
    have hother : L = 1
  2. L9
    specialize binary_length_zero_input_general n
  3. L10
    specialize binary_length_zero_input_general L
  4. L11
    apply binary_length_zero_input_general
  5. L12
    exact hfirst_left_left
  6. L13
    exact hsecond
  7. L14
    trans 1
  8. L15
    exact hfirst_left_right
  9. L16
    symm
  10. L17
    exact hother
04Separate the logical casesL18–19

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

  1. L18
    cases hsecond
  2. L19
    cases hsecond_left
05Establish hselfL20–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary length zero input general.

  1. L20
    have hself : l = 1
  2. L21
    specialize binary_length_zero_input_general n
  3. L22
    specialize binary_length_zero_input_general l
  4. L23
    apply binary_length_zero_input_general
  5. L24
    exact hsecond_left_left
06Separate the logical casesL25–25

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

  1. L25
    right
07Use earlier factsL26–26

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

  1. L26
    exact hfirst_right
08Calculate and transport equalitiesL27–27

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    trans 1
09Use earlier factsL28–28

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

  1. L28
    exact hself
10Calculate and transport equalitiesL29–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    symm
11Use earlier factsL30–30

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

  1. L30
    exact hsecond_left_right
12Separate the logical casesL31–40

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

  1. L31
    cases hfirst_right
  2. L32
    cases hfirst_right_witness
  3. L33
    cases hfirst_right_witness_witness
  4. L34
    cases hfirst_right_witness_witness_witness
  5. L35
    cases hfirst_right_witness_witness_witness_right
  6. L36
    cases hfirst_right_witness_witness_witness_right_right
  7. L37
    cases hfirst_right_witness_witness_witness_right_right_right
  8. L38
    cases hfirst_right_witness_witness_witness_right_right_right_right
  9. L39
    cases hsecond_right
  10. L40
    cases hsecond_right_witness
13Separate the logical casesL41–46

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

  1. L41
    cases hsecond_right_witness_witness
  2. L42
    cases hsecond_right_witness_witness_witness
  3. L43
    cases hsecond_right_witness_witness_witness_right
  4. L44
    cases hsecond_right_witness_witness_witness_right_right
  5. L45
    cases hsecond_right_witness_witness_witness_right_right_right
  6. L46
    cases hsecond_right_witness_witness_witness_right_right_right_right
14Use earlier factsL47–48

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

  1. L47
    specialize le_total l
  2. L48
    specialize le_total L
15Separate the logical casesL49–49

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

  1. L49
    cases le_total
16Establish hcasesL50–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L50
    have hcases : l = L \/ exists gap. gap + S l = L
  2. L51
    specialize le_eq_or_lt l
  3. L52
    specialize le_eq_or_lt L
  4. L53
    apply le_eq_or_lt
  5. L54
    exact le_total_left
17Separate the logical casesL55–55

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

  1. L55
    cases hcases
18Use earlier factsL56–56

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

  1. L56
    exact hcases_left
19Establish hexponentL57–62

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

  1. L57
    have hexponent : exists gap. gap + l = x3
  2. L58
    specialize le_of_succ_le_succ l
  3. L59
    specialize le_of_succ_le_succ x3
  4. L60
    apply le_of_succ_le_succ
  5. L61
    rewrite hsecond_right_witness_witness_witness_left at hcases_right
  6. L62
    exact hcases_right
20Establish hpowersL63–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two exponent monotone.

  1. L63
    have hpowers : exists gap. gap + x2 = x4
  2. L64
    specialize binary_power_two_exponent_monotone l
  3. L65
    specialize binary_power_two_exponent_monotone x3
  4. L66
    specialize binary_power_two_exponent_monotone x2
  5. L67
    specialize binary_power_two_exponent_monotone x4
  6. L68
    apply binary_power_two_exponent_monotone
  7. L69
    exact hexponent
  8. L70
    exact hfirst_right_witness_witness_witness_right_right_right_left
  9. L71
    exact hsecond_right_witness_witness_witness_right_right_left
21Establish hreverseL72–78

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

  1. L72
    have hreverse : exists gap. gap + x2 = n
  2. L73
    specialize le_trans x2
  3. L74
    specialize le_trans x4
  4. L75
    specialize le_trans n
  5. L76
    apply le_trans
  6. L77
    exact hpowers
  7. L78
    exact hsecond_right_witness_witness_witness_right_right_right_right_left
22Separate the logical casesL79–79

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

  1. L79
    exfalso
23Use earlier factsL80–84

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

  1. L80
    specialize lt_not_le n
  2. L81
    specialize lt_not_le x2
  3. L82
    apply lt_not_le
  4. L83
    exact hfirst_right_witness_witness_witness_right_right_right_right_right
  5. L84
    exact hreverse
24Establish hcasesL85–89

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L85
    have hcases : L = l \/ exists gap. gap + S L = l
  2. L86
    specialize le_eq_or_lt L
  3. L87
    specialize le_eq_or_lt l
  4. L88
    apply le_eq_or_lt
  5. L89
    exact le_total_right
25Separate the logical casesL90–90

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

  1. L90
    cases hcases
26Calculate and transport equalitiesL91–91

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L91
    symm
27Use earlier factsL92–92

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

  1. L92
    exact hcases_left
28Establish hexponentL93–98

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

  1. L93
    have hexponent : exists gap. gap + L = x
  2. L94
    specialize le_of_succ_le_succ L
  3. L95
    specialize le_of_succ_le_succ x
  4. L96
    apply le_of_succ_le_succ
  5. L97
    rewrite hfirst_right_witness_witness_witness_left at hcases_right
  6. L98
    exact hcases_right
29Establish hpowersL99–107

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two exponent monotone.

  1. L99
    have hpowers : exists gap. gap + x5 = x1
  2. L100
    specialize binary_power_two_exponent_monotone L
  3. L101
    specialize binary_power_two_exponent_monotone x
  4. L102
    specialize binary_power_two_exponent_monotone x5
  5. L103
    specialize binary_power_two_exponent_monotone x1
  6. L104
    apply binary_power_two_exponent_monotone
  7. L105
    exact hexponent
  8. L106
    exact hsecond_right_witness_witness_witness_right_right_right_left
  9. L107
    exact hfirst_right_witness_witness_witness_right_right_left
30Establish hreverseL108–114

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

  1. L108
    have hreverse : exists gap. gap + x5 = n
  2. L109
    specialize le_trans x5
  3. L110
    specialize le_trans x1
  4. L111
    specialize le_trans n
  5. L112
    apply le_trans
  6. L113
    exact hpowers
  7. L114
    exact hfirst_right_witness_witness_witness_right_right_right_right_left
31Separate the logical casesL115–115

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

  1. L115
    exfalso
32Use earlier factsL116–120

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

  1. L116
    specialize lt_not_le n
  2. L117
    specialize lt_not_le x5
  3. L118
    apply lt_not_le
  4. L119
    exact hsecond_right_witness_witness_witness_right_right_right_right_right
  5. L120
    exact hreverse

Library-wide reading audit

Original defined command ledger · 120 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003intro L
  4. 0004intro hfirst
  5. 0005intro hsecond
  6. 0006cases hfirst
  7. 0007cases hfirst_left
  8. 0008have hother : L = 1
  9. 0009specialize binary_length_zero_input_general n
  10. 0010specialize binary_length_zero_input_general L
  11. 0011apply binary_length_zero_input_general
  12. 0012exact hfirst_left_left
  13. 0013exact hsecond
  14. 0014trans 1
  15. 0015exact hfirst_left_right
  16. 0016symm
  17. 0017exact hother
  18. 0018cases hsecond
  19. 0019cases hsecond_left
  20. 0020have hself : l = 1
  21. 0021specialize binary_length_zero_input_general n
  22. 0022specialize binary_length_zero_input_general l
  23. 0023apply binary_length_zero_input_general
  24. 0024exact hsecond_left_left
  25. 0025right
  26. 0026exact hfirst_right
  27. 0027trans 1
  28. 0028exact hself
  29. 0029symm
  30. 0030exact hsecond_left_right
  31. 0031cases hfirst_right
  32. 0032cases hfirst_right_witness
  33. 0033cases hfirst_right_witness_witness
  34. 0034cases hfirst_right_witness_witness_witness
  35. 0035cases hfirst_right_witness_witness_witness_right
  36. 0036cases hfirst_right_witness_witness_witness_right_right
  37. 0037cases hfirst_right_witness_witness_witness_right_right_right
  38. 0038cases hfirst_right_witness_witness_witness_right_right_right_right
  39. 0039cases hsecond_right
  40. 0040cases hsecond_right_witness
  41. 0041cases hsecond_right_witness_witness
  42. 0042cases hsecond_right_witness_witness_witness
  43. 0043cases hsecond_right_witness_witness_witness_right
  44. 0044cases hsecond_right_witness_witness_witness_right_right
  45. 0045cases hsecond_right_witness_witness_witness_right_right_right
  46. 0046cases hsecond_right_witness_witness_witness_right_right_right_right
  47. 0047specialize le_total l
  48. 0048specialize le_total L
  49. 0049cases le_total
  50. 0050have hcases : l = L \/ exists gap. gap + S l = L
  51. 0051specialize le_eq_or_lt l
  52. 0052specialize le_eq_or_lt L
  53. 0053apply le_eq_or_lt
  54. 0054exact le_total_left
  55. 0055cases hcases
  56. 0056exact hcases_left
  57. 0057have hexponent : exists gap. gap + l = x3
  58. 0058specialize le_of_succ_le_succ l
  59. 0059specialize le_of_succ_le_succ x3
  60. 0060apply le_of_succ_le_succ
  61. 0061rewrite hsecond_right_witness_witness_witness_left at hcases_right
  62. 0062exact hcases_right
  63. 0063have hpowers : exists gap. gap + x2 = x4
  64. 0064specialize binary_power_two_exponent_monotone l
  65. 0065specialize binary_power_two_exponent_monotone x3
  66. 0066specialize binary_power_two_exponent_monotone x2
  67. 0067specialize binary_power_two_exponent_monotone x4
  68. 0068apply binary_power_two_exponent_monotone
  69. 0069exact hexponent
  70. 0070exact hfirst_right_witness_witness_witness_right_right_right_left
  71. 0071exact hsecond_right_witness_witness_witness_right_right_left
  72. 0072have hreverse : exists gap. gap + x2 = n
  73. 0073specialize le_trans x2
  74. 0074specialize le_trans x4
  75. 0075specialize le_trans n
  76. 0076apply le_trans
  77. 0077exact hpowers
  78. 0078exact hsecond_right_witness_witness_witness_right_right_right_right_left
  79. 0079exfalso
  80. 0080specialize lt_not_le n
  81. 0081specialize lt_not_le x2
  82. 0082apply lt_not_le
  83. 0083exact hfirst_right_witness_witness_witness_right_right_right_right_right
  84. 0084exact hreverse
  85. 0085have hcases : L = l \/ exists gap. gap + S L = l
  86. 0086specialize le_eq_or_lt L
  87. 0087specialize le_eq_or_lt l
  88. 0088apply le_eq_or_lt
  89. 0089exact le_total_right
  90. 0090cases hcases
  91. 0091symm
  92. 0092exact hcases_left
  93. 0093have hexponent : exists gap. gap + L = x
  94. 0094specialize le_of_succ_le_succ L
  95. 0095specialize le_of_succ_le_succ x
  96. 0096apply le_of_succ_le_succ
  97. 0097rewrite hfirst_right_witness_witness_witness_left at hcases_right
  98. 0098exact hcases_right
  99. 0099have hpowers : exists gap. gap + x5 = x1
  100. 0100specialize binary_power_two_exponent_monotone L
  101. 0101specialize binary_power_two_exponent_monotone x
  102. 0102specialize binary_power_two_exponent_monotone x5
  103. 0103specialize binary_power_two_exponent_monotone x1
  104. 0104apply binary_power_two_exponent_monotone
  105. 0105exact hexponent
  106. 0106exact hsecond_right_witness_witness_witness_right_right_right_left
  107. 0107exact hfirst_right_witness_witness_witness_right_right_left
  108. 0108have hreverse : exists gap. gap + x5 = n
  109. 0109specialize le_trans x5
  110. 0110specialize le_trans x1
  111. 0111specialize le_trans n
  112. 0112apply le_trans
  113. 0113exact hpowers
  114. 0114exact hfirst_right_witness_witness_witness_right_right_right_right_left
  115. 0115exfalso
  116. 0116specialize lt_not_le n
  117. 0117specialize lt_not_le x5
  118. 0118apply lt_not_le
  119. 0119exact hsecond_right_witness_witness_witness_right_right_right_right_right
  120. 0120exact hreverse