BD0008

binary_length_upper_power_bound

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

Every actual BitLen witness supplies the exact beta-coded upper power 2^l and the strict inequality n < 2^l, including zero.

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 n l. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_upper_length ff_lower_bl_bd_upper_length ff_upper_bl_bd_upper_length. (((l) = S ff_exponent_bl_bd_upper_length) /\ ((exists ff_positive_bl_bd_upper_length. ff_positive_bl_bd_upper_length + 1 = (n)) /\ ((exists pa_b_bl_bd_upper_length_lower pa_c_bl_bd_upper_length_lower. ((forall pa_i_bl_bd_upper_length_lower_repeat. (exists pa_lt_bl_bd_upper_length_lower_repeat_bound. pa_lt_bl_bd_upper_length_lower_repeat_bound + S pa_i_bl_bd_upper_length_lower_repeat = ff_exponent_bl_bd_upper_length) -> (((exists pa_h_bl_bd_upper_length_lower_repeat_decoded. pa_h_bl_bd_upper_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_upper_length_lower_repeat)) * pa_c_bl_bd_upper_length_lower)) /\ exists pa_q_bl_bd_upper_length_lower_repeat_decoded. pa_b_bl_bd_upper_length_lower = pa_q_bl_bd_upper_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_upper_length_lower_repeat)) * pa_c_bl_bd_upper_length_lower) + (2)))) /\ (exists pa_u_bl_bd_upper_length_lower_product pa_v_bl_bd_upper_length_lower_product. ((((exists pa_h_bl_bd_upper_length_lower_product_start. pa_h_bl_bd_upper_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_start. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_upper_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_upper_length_lower_product_terminal. pa_h_bl_bd_upper_length_lower_product_terminal + S (ff_lower_bl_bd_upper_length) = S ((S (ff_exponent_bl_bd_upper_length)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_terminal. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_upper_length)) * pa_v_bl_bd_upper_length_lower_product) + (ff_lower_bl_bd_upper_length))) /\ forall pa_i_bl_bd_upper_length_lower_product. (exists pa_lt_bl_bd_upper_length_lower_product_bound. pa_lt_bl_bd_upper_length_lower_product_bound + S pa_i_bl_bd_upper_length_lower_product = ff_exponent_bl_bd_upper_length) -> exists pa_p_bl_bd_upper_length_lower_product pa_r_bl_bd_upper_length_lower_product pa_s_bl_bd_upper_length_lower_product. ((((exists pa_h_bl_bd_upper_length_lower_product_factor. pa_h_bl_bd_upper_length_lower_product_factor + S (pa_p_bl_bd_upper_length_lower_product) = S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_c_bl_bd_upper_length_lower)) /\ exists pa_q_bl_bd_upper_length_lower_product_factor. pa_b_bl_bd_upper_length_lower = pa_q_bl_bd_upper_length_lower_product_factor * S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_c_bl_bd_upper_length_lower) + (pa_p_bl_bd_upper_length_lower_product))) /\ ((((exists pa_h_bl_bd_upper_length_lower_product_partial. pa_h_bl_bd_upper_length_lower_product_partial + S (pa_r_bl_bd_upper_length_lower_product) = S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_partial. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_partial * S ((S (pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product) + (pa_r_bl_bd_upper_length_lower_product))) /\ ((((exists pa_h_bl_bd_upper_length_lower_product_successor. pa_h_bl_bd_upper_length_lower_product_successor + S (pa_s_bl_bd_upper_length_lower_product) = S ((S (S pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product)) /\ exists pa_q_bl_bd_upper_length_lower_product_successor. pa_u_bl_bd_upper_length_lower_product = pa_q_bl_bd_upper_length_lower_product_successor * S ((S (S pa_i_bl_bd_upper_length_lower_product)) * pa_v_bl_bd_upper_length_lower_product) + (pa_s_bl_bd_upper_length_lower_product))) /\ pa_s_bl_bd_upper_length_lower_product = pa_r_bl_bd_upper_length_lower_product * pa_p_bl_bd_upper_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_upper_length_upper pa_c_bl_bd_upper_length_upper. ((forall pa_i_bl_bd_upper_length_upper_repeat. (exists pa_lt_bl_bd_upper_length_upper_repeat_bound. pa_lt_bl_bd_upper_length_upper_repeat_bound + S pa_i_bl_bd_upper_length_upper_repeat = l) -> (((exists pa_h_bl_bd_upper_length_upper_repeat_decoded. pa_h_bl_bd_upper_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_upper_length_upper_repeat)) * pa_c_bl_bd_upper_length_upper)) /\ exists pa_q_bl_bd_upper_length_upper_repeat_decoded. pa_b_bl_bd_upper_length_upper = pa_q_bl_bd_upper_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_upper_length_upper_repeat)) * pa_c_bl_bd_upper_length_upper) + (2)))) /\ (exists pa_u_bl_bd_upper_length_upper_product pa_v_bl_bd_upper_length_upper_product. ((((exists pa_h_bl_bd_upper_length_upper_product_start. pa_h_bl_bd_upper_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_start. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_upper_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_upper_length_upper_product_terminal. pa_h_bl_bd_upper_length_upper_product_terminal + S (ff_upper_bl_bd_upper_length) = S ((S (l)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_terminal. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_upper_length_upper_product) + (ff_upper_bl_bd_upper_length))) /\ forall pa_i_bl_bd_upper_length_upper_product. (exists pa_lt_bl_bd_upper_length_upper_product_bound. pa_lt_bl_bd_upper_length_upper_product_bound + S pa_i_bl_bd_upper_length_upper_product = l) -> exists pa_p_bl_bd_upper_length_upper_product pa_r_bl_bd_upper_length_upper_product pa_s_bl_bd_upper_length_upper_product. ((((exists pa_h_bl_bd_upper_length_upper_product_factor. pa_h_bl_bd_upper_length_upper_product_factor + S (pa_p_bl_bd_upper_length_upper_product) = S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_c_bl_bd_upper_length_upper)) /\ exists pa_q_bl_bd_upper_length_upper_product_factor. pa_b_bl_bd_upper_length_upper = pa_q_bl_bd_upper_length_upper_product_factor * S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_c_bl_bd_upper_length_upper) + (pa_p_bl_bd_upper_length_upper_product))) /\ ((((exists pa_h_bl_bd_upper_length_upper_product_partial. pa_h_bl_bd_upper_length_upper_product_partial + S (pa_r_bl_bd_upper_length_upper_product) = S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_partial. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_partial * S ((S (pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product) + (pa_r_bl_bd_upper_length_upper_product))) /\ ((((exists pa_h_bl_bd_upper_length_upper_product_successor. pa_h_bl_bd_upper_length_upper_product_successor + S (pa_s_bl_bd_upper_length_upper_product) = S ((S (S pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product)) /\ exists pa_q_bl_bd_upper_length_upper_product_successor. pa_u_bl_bd_upper_length_upper_product = pa_q_bl_bd_upper_length_upper_product_successor * S ((S (S pa_i_bl_bd_upper_length_upper_product)) * pa_v_bl_bd_upper_length_upper_product) + (pa_s_bl_bd_upper_length_upper_product))) /\ pa_s_bl_bd_upper_length_upper_product = pa_r_bl_bd_upper_length_upper_product * pa_p_bl_bd_upper_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_upper_length. ff_lower_gap_bl_bd_upper_length + (ff_lower_bl_bd_upper_length) = (n)) /\ (exists ff_upper_gap_bl_bd_upper_length. ff_upper_gap_bl_bd_upper_length + S (n) = (ff_upper_bl_bd_upper_length))))))))) -> exists p. ((exists pa_b_bl_bd_upper_power pa_c_bl_bd_upper_power. ((forall pa_i_bl_bd_upper_power_repeat. (exists pa_lt_bl_bd_upper_power_repeat_bound. pa_lt_bl_bd_upper_power_repeat_bound + S pa_i_bl_bd_upper_power_repeat = l) -> (((exists pa_h_bl_bd_upper_power_repeat_decoded. pa_h_bl_bd_upper_power_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_upper_power_repeat)) * pa_c_bl_bd_upper_power)) /\ exists pa_q_bl_bd_upper_power_repeat_decoded. pa_b_bl_bd_upper_power = pa_q_bl_bd_upper_power_repeat_decoded * S ((S (pa_i_bl_bd_upper_power_repeat)) * pa_c_bl_bd_upper_power) + (2)))) /\ (exists pa_u_bl_bd_upper_power_product pa_v_bl_bd_upper_power_product. ((((exists pa_h_bl_bd_upper_power_product_start. pa_h_bl_bd_upper_power_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_start. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_start * S ((S (0)) * pa_v_bl_bd_upper_power_product) + (1))) /\ ((((exists pa_h_bl_bd_upper_power_product_terminal. pa_h_bl_bd_upper_power_product_terminal + S (p) = S ((S (l)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_terminal. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_terminal * S ((S (l)) * pa_v_bl_bd_upper_power_product) + (p))) /\ forall pa_i_bl_bd_upper_power_product. (exists pa_lt_bl_bd_upper_power_product_bound. pa_lt_bl_bd_upper_power_product_bound + S pa_i_bl_bd_upper_power_product = l) -> exists pa_p_bl_bd_upper_power_product pa_r_bl_bd_upper_power_product pa_s_bl_bd_upper_power_product. ((((exists pa_h_bl_bd_upper_power_product_factor. pa_h_bl_bd_upper_power_product_factor + S (pa_p_bl_bd_upper_power_product) = S ((S (pa_i_bl_bd_upper_power_product)) * pa_c_bl_bd_upper_power)) /\ exists pa_q_bl_bd_upper_power_product_factor. pa_b_bl_bd_upper_power = pa_q_bl_bd_upper_power_product_factor * S ((S (pa_i_bl_bd_upper_power_product)) * pa_c_bl_bd_upper_power) + (pa_p_bl_bd_upper_power_product))) /\ ((((exists pa_h_bl_bd_upper_power_product_partial. pa_h_bl_bd_upper_power_product_partial + S (pa_r_bl_bd_upper_power_product) = S ((S (pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_partial. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_partial * S ((S (pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product) + (pa_r_bl_bd_upper_power_product))) /\ ((((exists pa_h_bl_bd_upper_power_product_successor. pa_h_bl_bd_upper_power_product_successor + S (pa_s_bl_bd_upper_power_product) = S ((S (S pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product)) /\ exists pa_q_bl_bd_upper_power_product_successor. pa_u_bl_bd_upper_power_product = pa_q_bl_bd_upper_power_product_successor * S ((S (S pa_i_bl_bd_upper_power_product)) * pa_v_bl_bd_upper_power_product) + (pa_s_bl_bd_upper_power_product))) /\ pa_s_bl_bd_upper_power_product = pa_r_bl_bd_upper_power_product * pa_p_bl_bd_upper_power_product)))))))) /\ (exists gap. gap + S n = p))

Constructive proof overview

Generated structural guide

Every actual BitLen witness supplies the exact beta-coded upper power 2^l and the strict inequality n < 2^l, including zero.

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

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

Proof neighborhood

Direct dependencies

binary_power_two_exists Alpha theorem; checked-use authorized binary_power_two_nonzero Alpha theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized

Direct dependents

BD0009 binary_exponent_digit_prefix_at_length

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

35 script commands · 13 reading checkpoints · 2 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–3

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

  1. L1
    intro n
  2. L2
    intro l
  3. L3
    intro hlength
02Separate the logical casesL4–5

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

  1. L4
    cases hlength
  2. L5
    cases hlength_left
03Establish hpowerL6–8

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

  1. L6
    have hpower : ∃ value. PowTwo(l,value)Definitions: PowTwo
  2. L7
    specialize binary_power_two_exists l
  3. L8
    exact binary_power_two_exists
04Separate the logical casesL9–9

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

  1. L9
    cases hpower
05Construct an explicit witnessL10–10

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

  1. L10
    exists x
06Separate the logical casesL11–11

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

  1. L11
    split
07Use earlier factsL12–12

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

  1. L12
    exact hpower_witness
08Establish hnonzeroL13–22

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

  1. L13
    have hnonzero : ~(x = 0)
  2. L14
    intro hzero
  3. L15
    specialize binary_power_two_nonzero l
  4. L16
    specialize binary_power_two_nonzero x
  5. L17
    apply binary_power_two_nonzero
  6. L18
    exact hpower_witness
  7. L19
    exact hzero
  8. L20
    rewrite hlength_left_left
  9. L21
    specialize one_le_of_ne_zero x
  10. L22
    apply one_le_of_ne_zero
09Use earlier factsL23–23

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

  1. L23
    exact hnonzero
10Separate the logical casesL24–31

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

  1. L24
    cases hlength_right
  2. L25
    cases hlength_right_witness
  3. L26
    cases hlength_right_witness_witness
  4. L27
    cases hlength_right_witness_witness_witness
  5. L28
    cases hlength_right_witness_witness_witness_right
  6. L29
    cases hlength_right_witness_witness_witness_right_right
  7. L30
    cases hlength_right_witness_witness_witness_right_right_right
  8. L31
    cases hlength_right_witness_witness_witness_right_right_right_right
11Construct an explicit witnessL32–32

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

  1. L32
    exists x2
12Separate the logical casesL33–33

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

  1. L33
    split
13Use earlier factsL34–35

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

  1. L34
    exact hlength_right_witness_witness_witness_right_right_right_left
  2. L35
    exact hlength_right_witness_witness_witness_right_right_right_right_right

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003intro hlength
  4. 0004cases hlength
  5. 0005cases hlength_left
  6. 0006have hpower : exists value. (exists pa_b_bl_bd_zero_upper pa_c_bl_bd_zero_upper. ((forall pa_i_bl_bd_zero_upper_repeat. (exists pa_lt_bl_bd_zero_upper_repeat_bound. pa_lt_bl_bd_zero_upper_repeat_bound + S pa_i_bl_bd_zero_upper_repeat = l) -> (((exists pa_h_bl_bd_zero_upper_repeat_decoded. pa_h_bl_bd_zero_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_zero_upper_repeat)) * pa_c_bl_bd_zero_upper)) /\ exists pa_q_bl_bd_zero_upper_repeat_decoded. pa_b_bl_bd_zero_upper = pa_q_bl_bd_zero_upper_repeat_decoded * S ((S (pa_i_bl_bd_zero_upper_repeat)) * pa_c_bl_bd_zero_upper) + (2)))) /\ (exists pa_u_bl_bd_zero_upper_product pa_v_bl_bd_zero_upper_product. ((((exists pa_h_bl_bd_zero_upper_product_start. pa_h_bl_bd_zero_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_start. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_start * S ((S (0)) * pa_v_bl_bd_zero_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_zero_upper_product_terminal. pa_h_bl_bd_zero_upper_product_terminal + S (value) = S ((S (l)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_terminal. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_zero_upper_product) + (value))) /\ forall pa_i_bl_bd_zero_upper_product. (exists pa_lt_bl_bd_zero_upper_product_bound. pa_lt_bl_bd_zero_upper_product_bound + S pa_i_bl_bd_zero_upper_product = l) -> exists pa_p_bl_bd_zero_upper_product pa_r_bl_bd_zero_upper_product pa_s_bl_bd_zero_upper_product. ((((exists pa_h_bl_bd_zero_upper_product_factor. pa_h_bl_bd_zero_upper_product_factor + S (pa_p_bl_bd_zero_upper_product) = S ((S (pa_i_bl_bd_zero_upper_product)) * pa_c_bl_bd_zero_upper)) /\ exists pa_q_bl_bd_zero_upper_product_factor. pa_b_bl_bd_zero_upper = pa_q_bl_bd_zero_upper_product_factor * S ((S (pa_i_bl_bd_zero_upper_product)) * pa_c_bl_bd_zero_upper) + (pa_p_bl_bd_zero_upper_product))) /\ ((((exists pa_h_bl_bd_zero_upper_product_partial. pa_h_bl_bd_zero_upper_product_partial + S (pa_r_bl_bd_zero_upper_product) = S ((S (pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_partial. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_partial * S ((S (pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product) + (pa_r_bl_bd_zero_upper_product))) /\ ((((exists pa_h_bl_bd_zero_upper_product_successor. pa_h_bl_bd_zero_upper_product_successor + S (pa_s_bl_bd_zero_upper_product) = S ((S (S pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product)) /\ exists pa_q_bl_bd_zero_upper_product_successor. pa_u_bl_bd_zero_upper_product = pa_q_bl_bd_zero_upper_product_successor * S ((S (S pa_i_bl_bd_zero_upper_product)) * pa_v_bl_bd_zero_upper_product) + (pa_s_bl_bd_zero_upper_product))) /\ pa_s_bl_bd_zero_upper_product = pa_r_bl_bd_zero_upper_product * pa_p_bl_bd_zero_upper_product))))))))
  7. 0007specialize binary_power_two_exists l
  8. 0008exact binary_power_two_exists
  9. 0009cases hpower
  10. 0010exists x
  11. 0011split
  12. 0012exact hpower_witness
  13. 0013have hnonzero : ~(x = 0)
  14. 0014intro hzero
  15. 0015specialize binary_power_two_nonzero l
  16. 0016specialize binary_power_two_nonzero x
  17. 0017apply binary_power_two_nonzero
  18. 0018exact hpower_witness
  19. 0019exact hzero
  20. 0020rewrite hlength_left_left
  21. 0021specialize one_le_of_ne_zero x
  22. 0022apply one_le_of_ne_zero
  23. 0023exact hnonzero
  24. 0024cases hlength_right
  25. 0025cases hlength_right_witness
  26. 0026cases hlength_right_witness_witness
  27. 0027cases hlength_right_witness_witness_witness
  28. 0028cases hlength_right_witness_witness_witness_right
  29. 0029cases hlength_right_witness_witness_witness_right_right
  30. 0030cases hlength_right_witness_witness_witness_right_right_right
  31. 0031cases hlength_right_witness_witness_witness_right_right_right_right
  32. 0032exists x2
  33. 0033split
  34. 0034exact hlength_right_witness_witness_witness_right_right_right_left
  35. 0035exact hlength_right_witness_witness_witness_right_right_right_right_right

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