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.

The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. 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

∀ b. ∀ l. BitLen(b,l) → ∃ x. PowTwo(l,x) ∧ Lt(b,x)

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

Definition DAG

PowTwo(e,p) · 1 BitLen(n,ell) · 1 Lt(a,b) · 1

Actual proof prerequisites

binary_power_two_exists · checked external prerequisiteeuclidean_log_zero_below_power

Original expanded first-order 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))

Complete unchanged native tactic proof

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

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.

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)

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