BD0009

binary_exponent_digit_prefix_at_length

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

Every canonical binary-length witness constructs a genuine beta-coded equally long zero-or-one prefix whose base-two Horner value is the original exponent.

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_exact_length ff_lower_bl_bd_exact_length ff_upper_bl_bd_exact_length. (((l) = S ff_exponent_bl_bd_exact_length) /\ ((exists ff_positive_bl_bd_exact_length. ff_positive_bl_bd_exact_length + 1 = (n)) /\ ((exists pa_b_bl_bd_exact_length_lower pa_c_bl_bd_exact_length_lower. ((forall pa_i_bl_bd_exact_length_lower_repeat. (exists pa_lt_bl_bd_exact_length_lower_repeat_bound. pa_lt_bl_bd_exact_length_lower_repeat_bound + S pa_i_bl_bd_exact_length_lower_repeat = ff_exponent_bl_bd_exact_length) -> (((exists pa_h_bl_bd_exact_length_lower_repeat_decoded. pa_h_bl_bd_exact_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_exact_length_lower_repeat)) * pa_c_bl_bd_exact_length_lower)) /\ exists pa_q_bl_bd_exact_length_lower_repeat_decoded. pa_b_bl_bd_exact_length_lower = pa_q_bl_bd_exact_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_exact_length_lower_repeat)) * pa_c_bl_bd_exact_length_lower) + (2)))) /\ (exists pa_u_bl_bd_exact_length_lower_product pa_v_bl_bd_exact_length_lower_product. ((((exists pa_h_bl_bd_exact_length_lower_product_start. pa_h_bl_bd_exact_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_start. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_exact_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_exact_length_lower_product_terminal. pa_h_bl_bd_exact_length_lower_product_terminal + S (ff_lower_bl_bd_exact_length) = S ((S (ff_exponent_bl_bd_exact_length)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_terminal. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_exact_length)) * pa_v_bl_bd_exact_length_lower_product) + (ff_lower_bl_bd_exact_length))) /\ forall pa_i_bl_bd_exact_length_lower_product. (exists pa_lt_bl_bd_exact_length_lower_product_bound. pa_lt_bl_bd_exact_length_lower_product_bound + S pa_i_bl_bd_exact_length_lower_product = ff_exponent_bl_bd_exact_length) -> exists pa_p_bl_bd_exact_length_lower_product pa_r_bl_bd_exact_length_lower_product pa_s_bl_bd_exact_length_lower_product. ((((exists pa_h_bl_bd_exact_length_lower_product_factor. pa_h_bl_bd_exact_length_lower_product_factor + S (pa_p_bl_bd_exact_length_lower_product) = S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_c_bl_bd_exact_length_lower)) /\ exists pa_q_bl_bd_exact_length_lower_product_factor. pa_b_bl_bd_exact_length_lower = pa_q_bl_bd_exact_length_lower_product_factor * S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_c_bl_bd_exact_length_lower) + (pa_p_bl_bd_exact_length_lower_product))) /\ ((((exists pa_h_bl_bd_exact_length_lower_product_partial. pa_h_bl_bd_exact_length_lower_product_partial + S (pa_r_bl_bd_exact_length_lower_product) = S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_partial. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_partial * S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product) + (pa_r_bl_bd_exact_length_lower_product))) /\ ((((exists pa_h_bl_bd_exact_length_lower_product_successor. pa_h_bl_bd_exact_length_lower_product_successor + S (pa_s_bl_bd_exact_length_lower_product) = S ((S (S pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_successor. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_successor * S ((S (S pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product) + (pa_s_bl_bd_exact_length_lower_product))) /\ pa_s_bl_bd_exact_length_lower_product = pa_r_bl_bd_exact_length_lower_product * pa_p_bl_bd_exact_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_exact_length_upper pa_c_bl_bd_exact_length_upper. ((forall pa_i_bl_bd_exact_length_upper_repeat. (exists pa_lt_bl_bd_exact_length_upper_repeat_bound. pa_lt_bl_bd_exact_length_upper_repeat_bound + S pa_i_bl_bd_exact_length_upper_repeat = l) -> (((exists pa_h_bl_bd_exact_length_upper_repeat_decoded. pa_h_bl_bd_exact_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_exact_length_upper_repeat)) * pa_c_bl_bd_exact_length_upper)) /\ exists pa_q_bl_bd_exact_length_upper_repeat_decoded. pa_b_bl_bd_exact_length_upper = pa_q_bl_bd_exact_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_exact_length_upper_repeat)) * pa_c_bl_bd_exact_length_upper) + (2)))) /\ (exists pa_u_bl_bd_exact_length_upper_product pa_v_bl_bd_exact_length_upper_product. ((((exists pa_h_bl_bd_exact_length_upper_product_start. pa_h_bl_bd_exact_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_start. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_exact_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_exact_length_upper_product_terminal. pa_h_bl_bd_exact_length_upper_product_terminal + S (ff_upper_bl_bd_exact_length) = S ((S (l)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_terminal. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_exact_length_upper_product) + (ff_upper_bl_bd_exact_length))) /\ forall pa_i_bl_bd_exact_length_upper_product. (exists pa_lt_bl_bd_exact_length_upper_product_bound. pa_lt_bl_bd_exact_length_upper_product_bound + S pa_i_bl_bd_exact_length_upper_product = l) -> exists pa_p_bl_bd_exact_length_upper_product pa_r_bl_bd_exact_length_upper_product pa_s_bl_bd_exact_length_upper_product. ((((exists pa_h_bl_bd_exact_length_upper_product_factor. pa_h_bl_bd_exact_length_upper_product_factor + S (pa_p_bl_bd_exact_length_upper_product) = S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_c_bl_bd_exact_length_upper)) /\ exists pa_q_bl_bd_exact_length_upper_product_factor. pa_b_bl_bd_exact_length_upper = pa_q_bl_bd_exact_length_upper_product_factor * S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_c_bl_bd_exact_length_upper) + (pa_p_bl_bd_exact_length_upper_product))) /\ ((((exists pa_h_bl_bd_exact_length_upper_product_partial. pa_h_bl_bd_exact_length_upper_product_partial + S (pa_r_bl_bd_exact_length_upper_product) = S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_partial. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_partial * S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product) + (pa_r_bl_bd_exact_length_upper_product))) /\ ((((exists pa_h_bl_bd_exact_length_upper_product_successor. pa_h_bl_bd_exact_length_upper_product_successor + S (pa_s_bl_bd_exact_length_upper_product) = S ((S (S pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_successor. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_successor * S ((S (S pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product) + (pa_s_bl_bd_exact_length_upper_product))) /\ pa_s_bl_bd_exact_length_upper_product = pa_r_bl_bd_exact_length_upper_product * pa_p_bl_bd_exact_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_exact_length. ff_lower_gap_bl_bd_exact_length + (ff_lower_bl_bd_exact_length) = (n)) /\ (exists ff_upper_gap_bl_bd_exact_length. ff_upper_gap_bl_bd_exact_length + S (n) = (ff_upper_bl_bd_exact_length))))))))) -> exists b c. (((forall ff_index_be_bd_exact_length_digits ff_digit_be_bd_exact_length_digits. (exists ff_lt_be_bd_exact_length_digits_bound. ff_lt_be_bd_exact_length_digits_bound + S ff_index_be_bd_exact_length_digits = l) -> (((exists ff_h_be_bd_exact_length_digits_digit. ff_h_be_bd_exact_length_digits_digit + S (ff_digit_be_bd_exact_length_digits) = S ((S (ff_index_be_bd_exact_length_digits)) * c)) /\ exists ff_q_be_bd_exact_length_digits_digit. b = ff_q_be_bd_exact_length_digits_digit * S ((S (ff_index_be_bd_exact_length_digits)) * c) + (ff_digit_be_bd_exact_length_digits))) -> (ff_digit_be_bd_exact_length_digits = 0 \/ ff_digit_be_bd_exact_length_digits = 1)) /\ (exists ff_u_ph_bd_exact_length_horner ff_v_ph_bd_exact_length_horner. ((((exists fs_h_ph_bd_exact_length_horner_body_start. fs_h_ph_bd_exact_length_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_start. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_start * S ((S (0)) * ff_v_ph_bd_exact_length_horner) + (0))) /\ ((((exists fs_h_ph_bd_exact_length_horner_body_terminal. fs_h_ph_bd_exact_length_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_terminal. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_exact_length_horner) + (n))) /\ forall ff_i_ph_bd_exact_length_horner_body_steps. (exists ph_bound_bd_exact_length_horner_body_steps. ph_bound_bd_exact_length_horner_body_steps + S ff_i_ph_bd_exact_length_horner_body_steps = l) -> exists ff_coefficient_ph_bd_exact_length_horner_body_steps ff_previous_ph_bd_exact_length_horner_body_steps ff_current_ph_bd_exact_length_horner_body_steps. ((((exists fs_h_ph_bd_exact_length_horner_body_steps_coefficient. fs_h_ph_bd_exact_length_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_exact_length_horner_body_steps) = S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_exact_length_horner_body_steps_coefficient. b = fs_q_ph_bd_exact_length_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * c) + (ff_coefficient_ph_bd_exact_length_horner_body_steps))) /\ ((((exists fs_h_ph_bd_exact_length_horner_body_steps_before. fs_h_ph_bd_exact_length_horner_body_steps_before + S (ff_previous_ph_bd_exact_length_horner_body_steps) = S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_steps_before. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_steps_before * S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner) + (ff_previous_ph_bd_exact_length_horner_body_steps))) /\ ((((exists fs_h_ph_bd_exact_length_horner_body_steps_after. fs_h_ph_bd_exact_length_horner_body_steps_after + S (ff_current_ph_bd_exact_length_horner_body_steps) = S ((S (S ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_steps_after. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_steps_after * S ((S (S ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner) + (ff_current_ph_bd_exact_length_horner_body_steps))) /\ ff_current_ph_bd_exact_length_horner_body_steps = ff_previous_ph_bd_exact_length_horner_body_steps * 2 + ff_coefficient_ph_bd_exact_length_horner_body_steps))))))))

Constructive proof overview

Generated structural guide

Every canonical binary-length witness constructs a genuine beta-coded equally long zero-or-one prefix whose base-two Horner value is the original exponent.

The unchanged tactic script uses 2 declared prerequisites and contains 16 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BD0008 binary_length_upper_power_bound BD0007 binary_digit_bounded_prefix_exists

Direct dependents

BD000A binary_exponent_digit_prefix_exists

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

16 script commands · 4 reading checkpoints · 1 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.

Named ingredients (2)
binary length upper power boundbinary digit bounded prefix exists

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
02Establish hupperL4–8

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

  1. L4
    have hupper : ∃ p. PowTwo(l,p) ∧ Lt(n,p)Definitions: PowTwoLt
  2. L5
    specialize binary_length_upper_power_bound n
  3. L6
    specialize binary_length_upper_power_bound l
  4. L7
    apply binary_length_upper_power_bound
  5. L8
    exact hlength
03Separate the logical casesL9–10

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

  1. L9
    cases hupper
  2. L10
    cases hupper_witness
04Use earlier factsL11–16

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

  1. L11
    specialize binary_digit_bounded_prefix_exists l
  2. L12
    specialize binary_digit_bounded_prefix_exists x
  3. L13
    specialize binary_digit_bounded_prefix_exists n
  4. L14
    apply binary_digit_bounded_prefix_exists
  5. L15
    exact hupper_witness_left
  6. L16
    exact hupper_witness_right

Library-wide reading audit

Original exact command ledger · 16 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003intro hlength
  4. 0004have hupper : exists p. ((exists pa_b_bl_bd_exact_upper pa_c_bl_bd_exact_upper. ((forall pa_i_bl_bd_exact_upper_repeat. (exists pa_lt_bl_bd_exact_upper_repeat_bound. pa_lt_bl_bd_exact_upper_repeat_bound + S pa_i_bl_bd_exact_upper_repeat = l) -> (((exists pa_h_bl_bd_exact_upper_repeat_decoded. pa_h_bl_bd_exact_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_exact_upper_repeat)) * pa_c_bl_bd_exact_upper)) /\ exists pa_q_bl_bd_exact_upper_repeat_decoded. pa_b_bl_bd_exact_upper = pa_q_bl_bd_exact_upper_repeat_decoded * S ((S (pa_i_bl_bd_exact_upper_repeat)) * pa_c_bl_bd_exact_upper) + (2)))) /\ (exists pa_u_bl_bd_exact_upper_product pa_v_bl_bd_exact_upper_product. ((((exists pa_h_bl_bd_exact_upper_product_start. pa_h_bl_bd_exact_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_start. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_start * S ((S (0)) * pa_v_bl_bd_exact_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_exact_upper_product_terminal. pa_h_bl_bd_exact_upper_product_terminal + S (p) = S ((S (l)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_terminal. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_exact_upper_product) + (p))) /\ forall pa_i_bl_bd_exact_upper_product. (exists pa_lt_bl_bd_exact_upper_product_bound. pa_lt_bl_bd_exact_upper_product_bound + S pa_i_bl_bd_exact_upper_product = l) -> exists pa_p_bl_bd_exact_upper_product pa_r_bl_bd_exact_upper_product pa_s_bl_bd_exact_upper_product. ((((exists pa_h_bl_bd_exact_upper_product_factor. pa_h_bl_bd_exact_upper_product_factor + S (pa_p_bl_bd_exact_upper_product) = S ((S (pa_i_bl_bd_exact_upper_product)) * pa_c_bl_bd_exact_upper)) /\ exists pa_q_bl_bd_exact_upper_product_factor. pa_b_bl_bd_exact_upper = pa_q_bl_bd_exact_upper_product_factor * S ((S (pa_i_bl_bd_exact_upper_product)) * pa_c_bl_bd_exact_upper) + (pa_p_bl_bd_exact_upper_product))) /\ ((((exists pa_h_bl_bd_exact_upper_product_partial. pa_h_bl_bd_exact_upper_product_partial + S (pa_r_bl_bd_exact_upper_product) = S ((S (pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_partial. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_partial * S ((S (pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product) + (pa_r_bl_bd_exact_upper_product))) /\ ((((exists pa_h_bl_bd_exact_upper_product_successor. pa_h_bl_bd_exact_upper_product_successor + S (pa_s_bl_bd_exact_upper_product) = S ((S (S pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_successor. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_successor * S ((S (S pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product) + (pa_s_bl_bd_exact_upper_product))) /\ pa_s_bl_bd_exact_upper_product = pa_r_bl_bd_exact_upper_product * pa_p_bl_bd_exact_upper_product)))))))) /\ (exists gap. gap + S n = p))
  5. 0005specialize binary_length_upper_power_bound n
  6. 0006specialize binary_length_upper_power_bound l
  7. 0007apply binary_length_upper_power_bound
  8. 0008exact hlength
  9. 0009cases hupper
  10. 0010cases hupper_witness
  11. 0011specialize binary_digit_bounded_prefix_exists l
  12. 0012specialize binary_digit_bounded_prefix_exists x
  13. 0013specialize binary_digit_bounded_prefix_exists n
  14. 0014apply binary_digit_bounded_prefix_exists
  15. 0015exact hupper_witness_left
  16. 0016exact hupper_witness_right

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