EL000D — euclidean_log_binary_length_upper_power

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

Exact expanded first-order arithmetic statement

forall b l. ((((b) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_elb_length ff_lower_bl_elb_length ff_upper_bl_elb_length. (((l) = S ff_exponent_bl_elb_length) /\ ((exists ff_positive_bl_elb_length. ff_positive_bl_elb_length + 1 = (b)) /\ ((exists pa_b_bl_elb_length_lower pa_c_bl_elb_length_lower. ((forall pa_i_bl_elb_length_lower_repeat. (exists pa_lt_bl_elb_length_lower_repeat_bound. pa_lt_bl_elb_length_lower_repeat_bound + S pa_i_bl_elb_length_lower_repeat = ff_exponent_bl_elb_length) -> (((exists pa_h_bl_elb_length_lower_repeat_decoded. pa_h_bl_elb_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_repeat_decoded. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_repeat_decoded * S ((S (pa_i_bl_elb_length_lower_repeat)) * pa_c_bl_elb_length_lower) + (2)))) /\ (exists pa_u_bl_elb_length_lower_product pa_v_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_start. pa_h_bl_elb_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_start. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_start * S ((S (0)) * pa_v_bl_elb_length_lower_product) + (1))) /\ ((((exists pa_h_bl_elb_length_lower_product_terminal. pa_h_bl_elb_length_lower_product_terminal + S (ff_lower_bl_elb_length) = S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_terminal. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_terminal * S ((S (ff_exponent_bl_elb_length)) * pa_v_bl_elb_length_lower_product) + (ff_lower_bl_elb_length))) /\ forall pa_i_bl_elb_length_lower_product. (exists pa_lt_bl_elb_length_lower_product_bound. pa_lt_bl_elb_length_lower_product_bound + S pa_i_bl_elb_length_lower_product = ff_exponent_bl_elb_length) -> exists pa_p_bl_elb_length_lower_product pa_r_bl_elb_length_lower_product pa_s_bl_elb_length_lower_product. ((((exists pa_h_bl_elb_length_lower_product_factor. pa_h_bl_elb_length_lower_product_factor + S (pa_p_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower)) /\ exists pa_q_bl_elb_length_lower_product_factor. pa_b_bl_elb_length_lower = pa_q_bl_elb_length_lower_product_factor * S ((S (pa_i_bl_elb_length_lower_product)) * pa_c_bl_elb_length_lower) + (pa_p_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_partial. pa_h_bl_elb_length_lower_product_partial + S (pa_r_bl_elb_length_lower_product) = S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_partial. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_partial * S ((S (pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_r_bl_elb_length_lower_product))) /\ ((((exists pa_h_bl_elb_length_lower_product_successor. pa_h_bl_elb_length_lower_product_successor + S (pa_s_bl_elb_length_lower_product) = S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product)) /\ exists pa_q_bl_elb_length_lower_product_successor. pa_u_bl_elb_length_lower_product = pa_q_bl_elb_length_lower_product_successor * S ((S (S pa_i_bl_elb_length_lower_product)) * pa_v_bl_elb_length_lower_product) + (pa_s_bl_elb_length_lower_product))) /\ pa_s_bl_elb_length_lower_product = pa_r_bl_elb_length_lower_product * pa_p_bl_elb_length_lower_product)))))))) /\ ((exists pa_b_bl_elb_length_upper pa_c_bl_elb_length_upper. ((forall pa_i_bl_elb_length_upper_repeat. (exists pa_lt_bl_elb_length_upper_repeat_bound. pa_lt_bl_elb_length_upper_repeat_bound + S pa_i_bl_elb_length_upper_repeat = l) -> (((exists pa_h_bl_elb_length_upper_repeat_decoded. pa_h_bl_elb_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_repeat_decoded. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_repeat_decoded * S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper) + (2)))) /\ (exists pa_u_bl_elb_length_upper_product pa_v_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_start. pa_h_bl_elb_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_start. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_start * S ((S (0)) * pa_v_bl_elb_length_upper_product) + (1))) /\ ((((exists pa_h_bl_elb_length_upper_product_terminal. pa_h_bl_elb_length_upper_product_terminal + S (ff_upper_bl_elb_length) = S ((S (l)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_terminal. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_terminal * S ((S (l)) * pa_v_bl_elb_length_upper_product) + (ff_upper_bl_elb_length))) /\ forall pa_i_bl_elb_length_upper_product. (exists pa_lt_bl_elb_length_upper_product_bound. pa_lt_bl_elb_length_upper_product_bound + S pa_i_bl_elb_length_upper_product = l) -> exists pa_p_bl_elb_length_upper_product pa_r_bl_elb_length_upper_product pa_s_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_factor. pa_h_bl_elb_length_upper_product_factor + S (pa_p_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_product_factor. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_product_factor * S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper) + (pa_p_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_partial. pa_h_bl_elb_length_upper_product_partial + S (pa_r_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_partial. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_partial * S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_r_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_successor. pa_h_bl_elb_length_upper_product_successor + S (pa_s_bl_elb_length_upper_product) = S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_successor. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_successor * S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_s_bl_elb_length_upper_product))) /\ pa_s_bl_elb_length_upper_product = pa_r_bl_elb_length_upper_product * pa_p_bl_elb_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_elb_length. ff_lower_gap_bl_elb_length + (ff_lower_bl_elb_length) = (b)) /\ (exists ff_upper_gap_bl_elb_length. ff_upper_gap_bl_elb_length + S (b) = (ff_upper_bl_elb_length))))))))) -> exists p. ((exists pa_b_bl_elb_length_upper pa_c_bl_elb_length_upper. ((forall pa_i_bl_elb_length_upper_repeat. (exists pa_lt_bl_elb_length_upper_repeat_bound. pa_lt_bl_elb_length_upper_repeat_bound + S pa_i_bl_elb_length_upper_repeat = l) -> (((exists pa_h_bl_elb_length_upper_repeat_decoded. pa_h_bl_elb_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_repeat_decoded. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_repeat_decoded * S ((S (pa_i_bl_elb_length_upper_repeat)) * pa_c_bl_elb_length_upper) + (2)))) /\ (exists pa_u_bl_elb_length_upper_product pa_v_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_start. pa_h_bl_elb_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_start. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_start * S ((S (0)) * pa_v_bl_elb_length_upper_product) + (1))) /\ ((((exists pa_h_bl_elb_length_upper_product_terminal. pa_h_bl_elb_length_upper_product_terminal + S (p) = S ((S (l)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_terminal. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_terminal * S ((S (l)) * pa_v_bl_elb_length_upper_product) + (p))) /\ forall pa_i_bl_elb_length_upper_product. (exists pa_lt_bl_elb_length_upper_product_bound. pa_lt_bl_elb_length_upper_product_bound + S pa_i_bl_elb_length_upper_product = l) -> exists pa_p_bl_elb_length_upper_product pa_r_bl_elb_length_upper_product pa_s_bl_elb_length_upper_product. ((((exists pa_h_bl_elb_length_upper_product_factor. pa_h_bl_elb_length_upper_product_factor + S (pa_p_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper)) /\ exists pa_q_bl_elb_length_upper_product_factor. pa_b_bl_elb_length_upper = pa_q_bl_elb_length_upper_product_factor * S ((S (pa_i_bl_elb_length_upper_product)) * pa_c_bl_elb_length_upper) + (pa_p_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_partial. pa_h_bl_elb_length_upper_product_partial + S (pa_r_bl_elb_length_upper_product) = S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_partial. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_partial * S ((S (pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_r_bl_elb_length_upper_product))) /\ ((((exists pa_h_bl_elb_length_upper_product_successor. pa_h_bl_elb_length_upper_product_successor + S (pa_s_bl_elb_length_upper_product) = S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product)) /\ exists pa_q_bl_elb_length_upper_product_successor. pa_u_bl_elb_length_upper_product = pa_q_bl_elb_length_upper_product_successor * S ((S (S pa_i_bl_elb_length_upper_product)) * pa_v_bl_elb_length_upper_product) + (pa_s_bl_elb_length_upper_product))) /\ pa_s_bl_elb_length_upper_product = pa_r_bl_elb_length_upper_product * pa_p_bl_elb_length_upper_product)))))))) /\ (exists ff_lt_elb_length_upper. ff_lt_elb_length_upper + S b = p))

Constructive proof overview

Generated structural guide

Every genuine BitLen witness, including the zero-has-one-digit convention, supplies a witnessed strict upper power of two.

The unchanged tactic script uses 2 declared prerequisites and contains 28 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 EL000A euclidean_log_zero_below_power

Direct dependents

EL000E euclidean_log_trace_bound

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

28 script commands · 11 reading checkpoints · 0 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 (1)

euclidean log zero below power

01Fix variables and assumptionsL1–3

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

L1
intro b
L2
intro l
L3
intro hlength

02Separate the logical casesL4–5