BD000A

binary_exponent_digit_prefix_exists

Every arbitrary natural exponent has an actual canonical-length beta-coded binary digit prefix with exactly that exponent as its Horner value.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

The exact G102 milestone is fully proved for every natural exponent and every modulus greater than one, including actual canonical digits, a beta-coded accumulator execution, modular-power correctness, and the formal bound k≤3·BitLen(e)+2. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ n. ∃ l. ∃ b. ∃ c. BinaryCanonicalExponentDigitCode(n,l,b,c)

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

Definition DAG

BinaryCanonicalExponentDigitCode(e,ell,b,c) · 1

Actual proof prerequisites

binary_length_exists · checked external prerequisitebinary_exponent_digit_prefix_at_length
Original expanded first-order statement 
forall n. exists l b c. ((((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_total_canonical_length ff_lower_bl_bd_total_canonical_length ff_upper_bl_bd_total_canonical_length. (((l) = S ff_exponent_bl_bd_total_canonical_length) /\ ((exists ff_positive_bl_bd_total_canonical_length. ff_positive_bl_bd_total_canonical_length + 1 = (n)) /\ ((exists pa_b_bl_bd_total_canonical_length_lower pa_c_bl_bd_total_canonical_length_lower. ((forall pa_i_bl_bd_total_canonical_length_lower_repeat. (exists pa_lt_bl_bd_total_canonical_length_lower_repeat_bound. pa_lt_bl_bd_total_canonical_length_lower_repeat_bound + S pa_i_bl_bd_total_canonical_length_lower_repeat = ff_exponent_bl_bd_total_canonical_length) -> (((exists pa_h_bl_bd_total_canonical_length_lower_repeat_decoded. pa_h_bl_bd_total_canonical_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_canonical_length_lower_repeat)) * pa_c_bl_bd_total_canonical_length_lower)) /\ exists pa_q_bl_bd_total_canonical_length_lower_repeat_decoded. pa_b_bl_bd_total_canonical_length_lower = pa_q_bl_bd_total_canonical_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_total_canonical_length_lower_repeat)) * pa_c_bl_bd_total_canonical_length_lower) + (2)))) /\ (exists pa_u_bl_bd_total_canonical_length_lower_product pa_v_bl_bd_total_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_canonical_length_lower_product_start. pa_h_bl_bd_total_canonical_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_start. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_total_canonical_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_total_canonical_length_lower_product_terminal. pa_h_bl_bd_total_canonical_length_lower_product_terminal + S (ff_lower_bl_bd_total_canonical_length) = S ((S (ff_exponent_bl_bd_total_canonical_length)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_terminal. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_total_canonical_length)) * pa_v_bl_bd_total_canonical_length_lower_product) + (ff_lower_bl_bd_total_canonical_length))) /\ forall pa_i_bl_bd_total_canonical_length_lower_product. (exists pa_lt_bl_bd_total_canonical_length_lower_product_bound. pa_lt_bl_bd_total_canonical_length_lower_product_bound + S pa_i_bl_bd_total_canonical_length_lower_product = ff_exponent_bl_bd_total_canonical_length) -> exists pa_p_bl_bd_total_canonical_length_lower_product pa_r_bl_bd_total_canonical_length_lower_product pa_s_bl_bd_total_canonical_length_lower_product. ((((exists pa_h_bl_bd_total_canonical_length_lower_product_factor. pa_h_bl_bd_total_canonical_length_lower_product_factor + S (pa_p_bl_bd_total_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_c_bl_bd_total_canonical_length_lower)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_factor. pa_b_bl_bd_total_canonical_length_lower = pa_q_bl_bd_total_canonical_length_lower_product_factor * S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_c_bl_bd_total_canonical_length_lower) + (pa_p_bl_bd_total_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_lower_product_partial. pa_h_bl_bd_total_canonical_length_lower_product_partial + S (pa_r_bl_bd_total_canonical_length_lower_product) = S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_partial. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_partial * S ((S (pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product) + (pa_r_bl_bd_total_canonical_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_lower_product_successor. pa_h_bl_bd_total_canonical_length_lower_product_successor + S (pa_s_bl_bd_total_canonical_length_lower_product) = S ((S (S pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product)) /\ exists pa_q_bl_bd_total_canonical_length_lower_product_successor. pa_u_bl_bd_total_canonical_length_lower_product = pa_q_bl_bd_total_canonical_length_lower_product_successor * S ((S (S pa_i_bl_bd_total_canonical_length_lower_product)) * pa_v_bl_bd_total_canonical_length_lower_product) + (pa_s_bl_bd_total_canonical_length_lower_product))) /\ pa_s_bl_bd_total_canonical_length_lower_product = pa_r_bl_bd_total_canonical_length_lower_product * pa_p_bl_bd_total_canonical_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_total_canonical_length_upper pa_c_bl_bd_total_canonical_length_upper. ((forall pa_i_bl_bd_total_canonical_length_upper_repeat. (exists pa_lt_bl_bd_total_canonical_length_upper_repeat_bound. pa_lt_bl_bd_total_canonical_length_upper_repeat_bound + S pa_i_bl_bd_total_canonical_length_upper_repeat = l) -> (((exists pa_h_bl_bd_total_canonical_length_upper_repeat_decoded. pa_h_bl_bd_total_canonical_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_canonical_length_upper_repeat)) * pa_c_bl_bd_total_canonical_length_upper)) /\ exists pa_q_bl_bd_total_canonical_length_upper_repeat_decoded. pa_b_bl_bd_total_canonical_length_upper = pa_q_bl_bd_total_canonical_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_total_canonical_length_upper_repeat)) * pa_c_bl_bd_total_canonical_length_upper) + (2)))) /\ (exists pa_u_bl_bd_total_canonical_length_upper_product pa_v_bl_bd_total_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_canonical_length_upper_product_start. pa_h_bl_bd_total_canonical_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_start. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_total_canonical_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_total_canonical_length_upper_product_terminal. pa_h_bl_bd_total_canonical_length_upper_product_terminal + S (ff_upper_bl_bd_total_canonical_length) = S ((S (l)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_terminal. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_total_canonical_length_upper_product) + (ff_upper_bl_bd_total_canonical_length))) /\ forall pa_i_bl_bd_total_canonical_length_upper_product. (exists pa_lt_bl_bd_total_canonical_length_upper_product_bound. pa_lt_bl_bd_total_canonical_length_upper_product_bound + S pa_i_bl_bd_total_canonical_length_upper_product = l) -> exists pa_p_bl_bd_total_canonical_length_upper_product pa_r_bl_bd_total_canonical_length_upper_product pa_s_bl_bd_total_canonical_length_upper_product. ((((exists pa_h_bl_bd_total_canonical_length_upper_product_factor. pa_h_bl_bd_total_canonical_length_upper_product_factor + S (pa_p_bl_bd_total_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_c_bl_bd_total_canonical_length_upper)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_factor. pa_b_bl_bd_total_canonical_length_upper = pa_q_bl_bd_total_canonical_length_upper_product_factor * S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_c_bl_bd_total_canonical_length_upper) + (pa_p_bl_bd_total_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_upper_product_partial. pa_h_bl_bd_total_canonical_length_upper_product_partial + S (pa_r_bl_bd_total_canonical_length_upper_product) = S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_partial. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_partial * S ((S (pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product) + (pa_r_bl_bd_total_canonical_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_canonical_length_upper_product_successor. pa_h_bl_bd_total_canonical_length_upper_product_successor + S (pa_s_bl_bd_total_canonical_length_upper_product) = S ((S (S pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product)) /\ exists pa_q_bl_bd_total_canonical_length_upper_product_successor. pa_u_bl_bd_total_canonical_length_upper_product = pa_q_bl_bd_total_canonical_length_upper_product_successor * S ((S (S pa_i_bl_bd_total_canonical_length_upper_product)) * pa_v_bl_bd_total_canonical_length_upper_product) + (pa_s_bl_bd_total_canonical_length_upper_product))) /\ pa_s_bl_bd_total_canonical_length_upper_product = pa_r_bl_bd_total_canonical_length_upper_product * pa_p_bl_bd_total_canonical_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_total_canonical_length. ff_lower_gap_bl_bd_total_canonical_length + (ff_lower_bl_bd_total_canonical_length) = (n)) /\ (exists ff_upper_gap_bl_bd_total_canonical_length. ff_upper_gap_bl_bd_total_canonical_length + S (n) = (ff_upper_bl_bd_total_canonical_length))))))))) /\ (((forall ff_index_be_bd_total_canonical_code_digits ff_digit_be_bd_total_canonical_code_digits. (exists ff_lt_be_bd_total_canonical_code_digits_bound. ff_lt_be_bd_total_canonical_code_digits_bound + S ff_index_be_bd_total_canonical_code_digits = l) -> (((exists ff_h_be_bd_total_canonical_code_digits_digit. ff_h_be_bd_total_canonical_code_digits_digit + S (ff_digit_be_bd_total_canonical_code_digits) = S ((S (ff_index_be_bd_total_canonical_code_digits)) * c)) /\ exists ff_q_be_bd_total_canonical_code_digits_digit. b = ff_q_be_bd_total_canonical_code_digits_digit * S ((S (ff_index_be_bd_total_canonical_code_digits)) * c) + (ff_digit_be_bd_total_canonical_code_digits))) -> (ff_digit_be_bd_total_canonical_code_digits = 0 \/ ff_digit_be_bd_total_canonical_code_digits = 1)) /\ (exists ff_u_ph_bd_total_canonical_code_horner ff_v_ph_bd_total_canonical_code_horner. ((((exists fs_h_ph_bd_total_canonical_code_horner_body_start. fs_h_ph_bd_total_canonical_code_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_start. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_start * S ((S (0)) * ff_v_ph_bd_total_canonical_code_horner) + (0))) /\ ((((exists fs_h_ph_bd_total_canonical_code_horner_body_terminal. fs_h_ph_bd_total_canonical_code_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_terminal. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_total_canonical_code_horner) + (n))) /\ forall ff_i_ph_bd_total_canonical_code_horner_body_steps. (exists ph_bound_bd_total_canonical_code_horner_body_steps. ph_bound_bd_total_canonical_code_horner_body_steps + S ff_i_ph_bd_total_canonical_code_horner_body_steps = l) -> exists ff_coefficient_ph_bd_total_canonical_code_horner_body_steps ff_previous_ph_bd_total_canonical_code_horner_body_steps ff_current_ph_bd_total_canonical_code_horner_body_steps. ((((exists fs_h_ph_bd_total_canonical_code_horner_body_steps_coefficient. fs_h_ph_bd_total_canonical_code_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_total_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_steps_coefficient. b = fs_q_ph_bd_total_canonical_code_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * c) + (ff_coefficient_ph_bd_total_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_canonical_code_horner_body_steps_before. fs_h_ph_bd_total_canonical_code_horner_body_steps_before + S (ff_previous_ph_bd_total_canonical_code_horner_body_steps) = S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_steps_before. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_steps_before * S ((S (ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner) + (ff_previous_ph_bd_total_canonical_code_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_canonical_code_horner_body_steps_after. fs_h_ph_bd_total_canonical_code_horner_body_steps_after + S (ff_current_ph_bd_total_canonical_code_horner_body_steps) = S ((S (S ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner)) /\ exists fs_q_ph_bd_total_canonical_code_horner_body_steps_after. ff_u_ph_bd_total_canonical_code_horner = fs_q_ph_bd_total_canonical_code_horner_body_steps_after * S ((S (S ff_i_ph_bd_total_canonical_code_horner_body_steps)) * ff_v_ph_bd_total_canonical_code_horner) + (ff_current_ph_bd_total_canonical_code_horner_body_steps))) /\ ff_current_ph_bd_total_canonical_code_horner_body_steps = ff_previous_ph_bd_total_canonical_code_horner_body_steps * 2 + ff_coefficient_ph_bd_total_canonical_code_horner_body_steps))))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

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

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 (1)
binary exponent digit prefix at length

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–1

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

  1. L1
    intro n
02Establish hlengthL2–4

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

  1. L2
    have hlength : ∃ l. BitLen(n,l)Definitions: BitLenOriginal native command in the exact edition
  2. L3
    specialize binary_length_exists n
  3. L4
    exact binary_length_exists
03Separate the logical casesL5–5

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

  1. L5
    cases hlength
04Establish hdigitsL6–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary exponent digit prefix at length.

  1. L6
    have hdigits : ∃ b. ∃ c. BinaryExponentDigitCode(n,x,b,c)Definitions: BinaryExponentDigitCodeOriginal native command in the exact edition
  2. L7
    specialize binary_exponent_digit_prefix_at_length n
  3. L8
    specialize binary_exponent_digit_prefix_at_length x
  4. L9
    apply binary_exponent_digit_prefix_at_length
  5. L10
    exact hlength_witness
05Separate the logical casesL11–12

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

  1. L11
    cases hdigits
  2. L12
    cases hdigits_witness
06Construct an explicit witnessL13–15

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

  1. L13
    exists x
  2. L14
    exists x1
  3. L15
    exists x2
07Separate the logical casesL16–16

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

  1. L16
    split
08Use earlier factsL17–18

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

  1. L17
    exact hlength_witness
  2. L18
    exact hdigits_witness_witness

Library-wide reading audit

Original defined command ledger · 18 lines
  1. 0001intro n
  2. 0002have hlength : exists l. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_total_length ff_lower_bl_bd_total_length ff_upper_bl_bd_total_length. (((l) = S ff_exponent_bl_bd_total_length) /\ ((exists ff_positive_bl_bd_total_length. ff_positive_bl_bd_total_length + 1 = (n)) /\ ((exists pa_b_bl_bd_total_length_lower pa_c_bl_bd_total_length_lower. ((forall pa_i_bl_bd_total_length_lower_repeat. (exists pa_lt_bl_bd_total_length_lower_repeat_bound. pa_lt_bl_bd_total_length_lower_repeat_bound + S pa_i_bl_bd_total_length_lower_repeat = ff_exponent_bl_bd_total_length) -> (((exists pa_h_bl_bd_total_length_lower_repeat_decoded. pa_h_bl_bd_total_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_length_lower_repeat)) * pa_c_bl_bd_total_length_lower)) /\ exists pa_q_bl_bd_total_length_lower_repeat_decoded. pa_b_bl_bd_total_length_lower = pa_q_bl_bd_total_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_total_length_lower_repeat)) * pa_c_bl_bd_total_length_lower) + (2)))) /\ (exists pa_u_bl_bd_total_length_lower_product pa_v_bl_bd_total_length_lower_product. ((((exists pa_h_bl_bd_total_length_lower_product_start. pa_h_bl_bd_total_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_start. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_total_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_total_length_lower_product_terminal. pa_h_bl_bd_total_length_lower_product_terminal + S (ff_lower_bl_bd_total_length) = S ((S (ff_exponent_bl_bd_total_length)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_terminal. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_total_length)) * pa_v_bl_bd_total_length_lower_product) + (ff_lower_bl_bd_total_length))) /\ forall pa_i_bl_bd_total_length_lower_product. (exists pa_lt_bl_bd_total_length_lower_product_bound. pa_lt_bl_bd_total_length_lower_product_bound + S pa_i_bl_bd_total_length_lower_product = ff_exponent_bl_bd_total_length) -> exists pa_p_bl_bd_total_length_lower_product pa_r_bl_bd_total_length_lower_product pa_s_bl_bd_total_length_lower_product. ((((exists pa_h_bl_bd_total_length_lower_product_factor. pa_h_bl_bd_total_length_lower_product_factor + S (pa_p_bl_bd_total_length_lower_product) = S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_c_bl_bd_total_length_lower)) /\ exists pa_q_bl_bd_total_length_lower_product_factor. pa_b_bl_bd_total_length_lower = pa_q_bl_bd_total_length_lower_product_factor * S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_c_bl_bd_total_length_lower) + (pa_p_bl_bd_total_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_length_lower_product_partial. pa_h_bl_bd_total_length_lower_product_partial + S (pa_r_bl_bd_total_length_lower_product) = S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_partial. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_partial * S ((S (pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product) + (pa_r_bl_bd_total_length_lower_product))) /\ ((((exists pa_h_bl_bd_total_length_lower_product_successor. pa_h_bl_bd_total_length_lower_product_successor + S (pa_s_bl_bd_total_length_lower_product) = S ((S (S pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product)) /\ exists pa_q_bl_bd_total_length_lower_product_successor. pa_u_bl_bd_total_length_lower_product = pa_q_bl_bd_total_length_lower_product_successor * S ((S (S pa_i_bl_bd_total_length_lower_product)) * pa_v_bl_bd_total_length_lower_product) + (pa_s_bl_bd_total_length_lower_product))) /\ pa_s_bl_bd_total_length_lower_product = pa_r_bl_bd_total_length_lower_product * pa_p_bl_bd_total_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_total_length_upper pa_c_bl_bd_total_length_upper. ((forall pa_i_bl_bd_total_length_upper_repeat. (exists pa_lt_bl_bd_total_length_upper_repeat_bound. pa_lt_bl_bd_total_length_upper_repeat_bound + S pa_i_bl_bd_total_length_upper_repeat = l) -> (((exists pa_h_bl_bd_total_length_upper_repeat_decoded. pa_h_bl_bd_total_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_total_length_upper_repeat)) * pa_c_bl_bd_total_length_upper)) /\ exists pa_q_bl_bd_total_length_upper_repeat_decoded. pa_b_bl_bd_total_length_upper = pa_q_bl_bd_total_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_total_length_upper_repeat)) * pa_c_bl_bd_total_length_upper) + (2)))) /\ (exists pa_u_bl_bd_total_length_upper_product pa_v_bl_bd_total_length_upper_product. ((((exists pa_h_bl_bd_total_length_upper_product_start. pa_h_bl_bd_total_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_start. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_total_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_total_length_upper_product_terminal. pa_h_bl_bd_total_length_upper_product_terminal + S (ff_upper_bl_bd_total_length) = S ((S (l)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_terminal. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_total_length_upper_product) + (ff_upper_bl_bd_total_length))) /\ forall pa_i_bl_bd_total_length_upper_product. (exists pa_lt_bl_bd_total_length_upper_product_bound. pa_lt_bl_bd_total_length_upper_product_bound + S pa_i_bl_bd_total_length_upper_product = l) -> exists pa_p_bl_bd_total_length_upper_product pa_r_bl_bd_total_length_upper_product pa_s_bl_bd_total_length_upper_product. ((((exists pa_h_bl_bd_total_length_upper_product_factor. pa_h_bl_bd_total_length_upper_product_factor + S (pa_p_bl_bd_total_length_upper_product) = S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_c_bl_bd_total_length_upper)) /\ exists pa_q_bl_bd_total_length_upper_product_factor. pa_b_bl_bd_total_length_upper = pa_q_bl_bd_total_length_upper_product_factor * S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_c_bl_bd_total_length_upper) + (pa_p_bl_bd_total_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_length_upper_product_partial. pa_h_bl_bd_total_length_upper_product_partial + S (pa_r_bl_bd_total_length_upper_product) = S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_partial. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_partial * S ((S (pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product) + (pa_r_bl_bd_total_length_upper_product))) /\ ((((exists pa_h_bl_bd_total_length_upper_product_successor. pa_h_bl_bd_total_length_upper_product_successor + S (pa_s_bl_bd_total_length_upper_product) = S ((S (S pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product)) /\ exists pa_q_bl_bd_total_length_upper_product_successor. pa_u_bl_bd_total_length_upper_product = pa_q_bl_bd_total_length_upper_product_successor * S ((S (S pa_i_bl_bd_total_length_upper_product)) * pa_v_bl_bd_total_length_upper_product) + (pa_s_bl_bd_total_length_upper_product))) /\ pa_s_bl_bd_total_length_upper_product = pa_r_bl_bd_total_length_upper_product * pa_p_bl_bd_total_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_total_length. ff_lower_gap_bl_bd_total_length + (ff_lower_bl_bd_total_length) = (n)) /\ (exists ff_upper_gap_bl_bd_total_length. ff_upper_gap_bl_bd_total_length + S (n) = (ff_upper_bl_bd_total_length)))))))))
  3. 0003specialize binary_length_exists n
  4. 0004exact binary_length_exists
  5. 0005cases hlength
  6. 0006have hdigits : exists b c. (((forall ff_index_be_bd_total_digits_digits ff_digit_be_bd_total_digits_digits. (exists ff_lt_be_bd_total_digits_digits_bound. ff_lt_be_bd_total_digits_digits_bound + S ff_index_be_bd_total_digits_digits = x) -> (((exists ff_h_be_bd_total_digits_digits_digit. ff_h_be_bd_total_digits_digits_digit + S (ff_digit_be_bd_total_digits_digits) = S ((S (ff_index_be_bd_total_digits_digits)) * c)) /\ exists ff_q_be_bd_total_digits_digits_digit. b = ff_q_be_bd_total_digits_digits_digit * S ((S (ff_index_be_bd_total_digits_digits)) * c) + (ff_digit_be_bd_total_digits_digits))) -> (ff_digit_be_bd_total_digits_digits = 0 \/ ff_digit_be_bd_total_digits_digits = 1)) /\ (exists ff_u_ph_bd_total_digits_horner ff_v_ph_bd_total_digits_horner. ((((exists fs_h_ph_bd_total_digits_horner_body_start. fs_h_ph_bd_total_digits_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_start. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_start * S ((S (0)) * ff_v_ph_bd_total_digits_horner) + (0))) /\ ((((exists fs_h_ph_bd_total_digits_horner_body_terminal. fs_h_ph_bd_total_digits_horner_body_terminal + S (n) = S ((S (x)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_terminal. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_terminal * S ((S (x)) * ff_v_ph_bd_total_digits_horner) + (n))) /\ forall ff_i_ph_bd_total_digits_horner_body_steps. (exists ph_bound_bd_total_digits_horner_body_steps. ph_bound_bd_total_digits_horner_body_steps + S ff_i_ph_bd_total_digits_horner_body_steps = x) -> exists ff_coefficient_ph_bd_total_digits_horner_body_steps ff_previous_ph_bd_total_digits_horner_body_steps ff_current_ph_bd_total_digits_horner_body_steps. ((((exists fs_h_ph_bd_total_digits_horner_body_steps_coefficient. fs_h_ph_bd_total_digits_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_total_digits_horner_body_steps) = S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_total_digits_horner_body_steps_coefficient. b = fs_q_ph_bd_total_digits_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * c) + (ff_coefficient_ph_bd_total_digits_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_digits_horner_body_steps_before. fs_h_ph_bd_total_digits_horner_body_steps_before + S (ff_previous_ph_bd_total_digits_horner_body_steps) = S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_steps_before. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_steps_before * S ((S (ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner) + (ff_previous_ph_bd_total_digits_horner_body_steps))) /\ ((((exists fs_h_ph_bd_total_digits_horner_body_steps_after. fs_h_ph_bd_total_digits_horner_body_steps_after + S (ff_current_ph_bd_total_digits_horner_body_steps) = S ((S (S ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner)) /\ exists fs_q_ph_bd_total_digits_horner_body_steps_after. ff_u_ph_bd_total_digits_horner = fs_q_ph_bd_total_digits_horner_body_steps_after * S ((S (S ff_i_ph_bd_total_digits_horner_body_steps)) * ff_v_ph_bd_total_digits_horner) + (ff_current_ph_bd_total_digits_horner_body_steps))) /\ ff_current_ph_bd_total_digits_horner_body_steps = ff_previous_ph_bd_total_digits_horner_body_steps * 2 + ff_coefficient_ph_bd_total_digits_horner_body_steps))))))))
  7. 0007specialize binary_exponent_digit_prefix_at_length n
  8. 0008specialize binary_exponent_digit_prefix_at_length x
  9. 0009apply binary_exponent_digit_prefix_at_length
  10. 0010exact hlength_witness
  11. 0011cases hdigits
  12. 0012cases hdigits_witness
  13. 0013exists x
  14. 0014exists x1
  15. 0015exists x2
  16. 0016split
  17. 0017exact hlength_witness
  18. 0018exact hdigits_witness_witness