PC0025 — binary_length_nonzero_components

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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ n. ∀ ell. ¬n = 0 → BitLen(n,ell) → ∃ x. ∃ y. ∃ z. ell = S x ∧ (PowTwo(x,y) ∧ (PowTwo(ell,z) ∧ (Le(y,n) ∧ Lt(n,z))))

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

Definition DAG

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

Actual proof prerequisites

none

Original expanded first-order statement

forall n ell. ~(n = 0) -> ((((n) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_length_components_source ff_lower_bl_pc_length_components_source ff_upper_bl_pc_length_components_source. (((ell) = S ff_exponent_bl_pc_length_components_source) /\ ((exists ff_positive_bl_pc_length_components_source. ff_positive_bl_pc_length_components_source + 1 = (n)) /\ ((exists pa_b_bl_pc_length_components_source_lower pa_c_bl_pc_length_components_source_lower. ((forall pa_i_bl_pc_length_components_source_lower_repeat. (exists pa_lt_bl_pc_length_components_source_lower_repeat_bound. pa_lt_bl_pc_length_components_source_lower_repeat_bound + S pa_i_bl_pc_length_components_source_lower_repeat = ff_exponent_bl_pc_length_components_source) -> (((exists pa_h_bl_pc_length_components_source_lower_repeat_decoded. pa_h_bl_pc_length_components_source_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_length_components_source_lower_repeat)) * pa_c_bl_pc_length_components_source_lower)) /\ exists pa_q_bl_pc_length_components_source_lower_repeat_decoded. pa_b_bl_pc_length_components_source_lower = pa_q_bl_pc_length_components_source_lower_repeat_decoded * S ((S (pa_i_bl_pc_length_components_source_lower_repeat)) * pa_c_bl_pc_length_components_source_lower) + (2)))) /\ (exists pa_u_bl_pc_length_components_source_lower_product pa_v_bl_pc_length_components_source_lower_product. ((((exists pa_h_bl_pc_length_components_source_lower_product_start. pa_h_bl_pc_length_components_source_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_length_components_source_lower_product)) /\ exists pa_q_bl_pc_length_components_source_lower_product_start. pa_u_bl_pc_length_components_source_lower_product = pa_q_bl_pc_length_components_source_lower_product_start * S ((S (0)) * pa_v_bl_pc_length_components_source_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_length_components_source_lower_product_terminal. pa_h_bl_pc_length_components_source_lower_product_terminal + S (ff_lower_bl_pc_length_components_source) = S ((S (ff_exponent_bl_pc_length_components_source)) * pa_v_bl_pc_length_components_source_lower_product)) /\ exists pa_q_bl_pc_length_components_source_lower_product_terminal. pa_u_bl_pc_length_components_source_lower_product = pa_q_bl_pc_length_components_source_lower_product_terminal * S ((S (ff_exponent_bl_pc_length_components_source)) * pa_v_bl_pc_length_components_source_lower_product) + (ff_lower_bl_pc_length_components_source))) /\ forall pa_i_bl_pc_length_components_source_lower_product. (exists pa_lt_bl_pc_length_components_source_lower_product_bound. pa_lt_bl_pc_length_components_source_lower_product_bound + S pa_i_bl_pc_length_components_source_lower_product = ff_exponent_bl_pc_length_components_source) -> exists pa_p_bl_pc_length_components_source_lower_product pa_r_bl_pc_length_components_source_lower_product pa_s_bl_pc_length_components_source_lower_product. ((((exists pa_h_bl_pc_length_components_source_lower_product_factor. pa_h_bl_pc_length_components_source_lower_product_factor + S (pa_p_bl_pc_length_components_source_lower_product) = S ((S (pa_i_bl_pc_length_components_source_lower_product)) * pa_c_bl_pc_length_components_source_lower)) /\ exists pa_q_bl_pc_length_components_source_lower_product_factor. pa_b_bl_pc_length_components_source_lower = pa_q_bl_pc_length_components_source_lower_product_factor * S ((S (pa_i_bl_pc_length_components_source_lower_product)) * pa_c_bl_pc_length_components_source_lower) + (pa_p_bl_pc_length_components_source_lower_product))) /\ ((((exists pa_h_bl_pc_length_components_source_lower_product_partial. pa_h_bl_pc_length_components_source_lower_product_partial + S (pa_r_bl_pc_length_components_source_lower_product) = S ((S (pa_i_bl_pc_length_components_source_lower_product)) * pa_v_bl_pc_length_components_source_lower_product)) /\ exists pa_q_bl_pc_length_components_source_lower_product_partial. pa_u_bl_pc_length_components_source_lower_product = pa_q_bl_pc_length_components_source_lower_product_partial * S ((S (pa_i_bl_pc_length_components_source_lower_product)) * pa_v_bl_pc_length_components_source_lower_product) + (pa_r_bl_pc_length_components_source_lower_product))) /\ ((((exists pa_h_bl_pc_length_components_source_lower_product_successor. pa_h_bl_pc_length_components_source_lower_product_successor + S (pa_s_bl_pc_length_components_source_lower_product) = S ((S (S pa_i_bl_pc_length_components_source_lower_product)) * pa_v_bl_pc_length_components_source_lower_product)) /\ exists pa_q_bl_pc_length_components_source_lower_product_successor. pa_u_bl_pc_length_components_source_lower_product = pa_q_bl_pc_length_components_source_lower_product_successor * S ((S (S pa_i_bl_pc_length_components_source_lower_product)) * pa_v_bl_pc_length_components_source_lower_product) + (pa_s_bl_pc_length_components_source_lower_product))) /\ pa_s_bl_pc_length_components_source_lower_product = pa_r_bl_pc_length_components_source_lower_product * pa_p_bl_pc_length_components_source_lower_product)))))))) /\ ((exists pa_b_bl_pc_length_components_source_upper pa_c_bl_pc_length_components_source_upper. ((forall pa_i_bl_pc_length_components_source_upper_repeat. (exists pa_lt_bl_pc_length_components_source_upper_repeat_bound. pa_lt_bl_pc_length_components_source_upper_repeat_bound + S pa_i_bl_pc_length_components_source_upper_repeat = ell) -> (((exists pa_h_bl_pc_length_components_source_upper_repeat_decoded. pa_h_bl_pc_length_components_source_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_length_components_source_upper_repeat)) * pa_c_bl_pc_length_components_source_upper)) /\ exists pa_q_bl_pc_length_components_source_upper_repeat_decoded. pa_b_bl_pc_length_components_source_upper = pa_q_bl_pc_length_components_source_upper_repeat_decoded * S ((S (pa_i_bl_pc_length_components_source_upper_repeat)) * pa_c_bl_pc_length_components_source_upper) + (2)))) /\ (exists pa_u_bl_pc_length_components_source_upper_product pa_v_bl_pc_length_components_source_upper_product. ((((exists pa_h_bl_pc_length_components_source_upper_product_start. pa_h_bl_pc_length_components_source_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_length_components_source_upper_product)) /\ exists pa_q_bl_pc_length_components_source_upper_product_start. pa_u_bl_pc_length_components_source_upper_product = pa_q_bl_pc_length_components_source_upper_product_start * S ((S (0)) * pa_v_bl_pc_length_components_source_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_length_components_source_upper_product_terminal. pa_h_bl_pc_length_components_source_upper_product_terminal + S (ff_upper_bl_pc_length_components_source) = S ((S (ell)) * pa_v_bl_pc_length_components_source_upper_product)) /\ exists pa_q_bl_pc_length_components_source_upper_product_terminal. pa_u_bl_pc_length_components_source_upper_product = pa_q_bl_pc_length_components_source_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_length_components_source_upper_product) + (ff_upper_bl_pc_length_components_source))) /\ forall pa_i_bl_pc_length_components_source_upper_product. (exists pa_lt_bl_pc_length_components_source_upper_product_bound. pa_lt_bl_pc_length_components_source_upper_product_bound + S pa_i_bl_pc_length_components_source_upper_product = ell) -> exists pa_p_bl_pc_length_components_source_upper_product pa_r_bl_pc_length_components_source_upper_product pa_s_bl_pc_length_components_source_upper_product. ((((exists pa_h_bl_pc_length_components_source_upper_product_factor. pa_h_bl_pc_length_components_source_upper_product_factor + S (pa_p_bl_pc_length_components_source_upper_product) = S ((S (pa_i_bl_pc_length_components_source_upper_product)) * pa_c_bl_pc_length_components_source_upper)) /\ exists pa_q_bl_pc_length_components_source_upper_product_factor. pa_b_bl_pc_length_components_source_upper = pa_q_bl_pc_length_components_source_upper_product_factor * S ((S (pa_i_bl_pc_length_components_source_upper_product)) * pa_c_bl_pc_length_components_source_upper) + (pa_p_bl_pc_length_components_source_upper_product))) /\ ((((exists pa_h_bl_pc_length_components_source_upper_product_partial. pa_h_bl_pc_length_components_source_upper_product_partial + S (pa_r_bl_pc_length_components_source_upper_product) = S ((S (pa_i_bl_pc_length_components_source_upper_product)) * pa_v_bl_pc_length_components_source_upper_product)) /\ exists pa_q_bl_pc_length_components_source_upper_product_partial. pa_u_bl_pc_length_components_source_upper_product = pa_q_bl_pc_length_components_source_upper_product_partial * S ((S (pa_i_bl_pc_length_components_source_upper_product)) * pa_v_bl_pc_length_components_source_upper_product) + (pa_r_bl_pc_length_components_source_upper_product))) /\ ((((exists pa_h_bl_pc_length_components_source_upper_product_successor. pa_h_bl_pc_length_components_source_upper_product_successor + S (pa_s_bl_pc_length_components_source_upper_product) = S ((S (S pa_i_bl_pc_length_components_source_upper_product)) * pa_v_bl_pc_length_components_source_upper_product)) /\ exists pa_q_bl_pc_length_components_source_upper_product_successor. pa_u_bl_pc_length_components_source_upper_product = pa_q_bl_pc_length_components_source_upper_product_successor * S ((S (S pa_i_bl_pc_length_components_source_upper_product)) * pa_v_bl_pc_length_components_source_upper_product) + (pa_s_bl_pc_length_components_source_upper_product))) /\ pa_s_bl_pc_length_components_source_upper_product = pa_r_bl_pc_length_components_source_upper_product * pa_p_bl_pc_length_components_source_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_length_components_source. ff_lower_gap_bl_pc_length_components_source + (ff_lower_bl_pc_length_components_source) = (n)) /\ (exists ff_upper_gap_bl_pc_length_components_source. ff_upper_gap_bl_pc_length_components_source + S (n) = (ff_upper_bl_pc_length_components_source))))))))) -> exists e v w. ell = S e /\ ((exists pa_b_pc_length_components_lower_power pa_c_pc_length_components_lower_power. ((forall pa_i_pc_length_components_lower_power_repeat. (exists pa_lt_pc_length_components_lower_power_repeat_bound. pa_lt_pc_length_components_lower_power_repeat_bound + S pa_i_pc_length_components_lower_power_repeat = e) -> (((exists pa_h_pc_length_components_lower_power_repeat_decoded. pa_h_pc_length_components_lower_power_repeat_decoded + S (2) = S ((S (pa_i_pc_length_components_lower_power_repeat)) * pa_c_pc_length_components_lower_power)) /\ exists pa_q_pc_length_components_lower_power_repeat_decoded. pa_b_pc_length_components_lower_power = pa_q_pc_length_components_lower_power_repeat_decoded * S ((S (pa_i_pc_length_components_lower_power_repeat)) * pa_c_pc_length_components_lower_power) + (2)))) /\ (exists pa_u_pc_length_components_lower_power_product pa_v_pc_length_components_lower_power_product. ((((exists pa_h_pc_length_components_lower_power_product_start. pa_h_pc_length_components_lower_power_product_start + S (1) = S ((S (0)) * pa_v_pc_length_components_lower_power_product)) /\ exists pa_q_pc_length_components_lower_power_product_start. pa_u_pc_length_components_lower_power_product = pa_q_pc_length_components_lower_power_product_start * S ((S (0)) * pa_v_pc_length_components_lower_power_product) + (1))) /\ ((((exists pa_h_pc_length_components_lower_power_product_terminal. pa_h_pc_length_components_lower_power_product_terminal + S (v) = S ((S (e)) * pa_v_pc_length_components_lower_power_product)) /\ exists pa_q_pc_length_components_lower_power_product_terminal. pa_u_pc_length_components_lower_power_product = pa_q_pc_length_components_lower_power_product_terminal * S ((S (e)) * pa_v_pc_length_components_lower_power_product) + (v))) /\ forall pa_i_pc_length_components_lower_power_product. (exists pa_lt_pc_length_components_lower_power_product_bound. pa_lt_pc_length_components_lower_power_product_bound + S pa_i_pc_length_components_lower_power_product = e) -> exists pa_p_pc_length_components_lower_power_product pa_r_pc_length_components_lower_power_product pa_s_pc_length_components_lower_power_product. ((((exists pa_h_pc_length_components_lower_power_product_factor. pa_h_pc_length_components_lower_power_product_factor + S (pa_p_pc_length_components_lower_power_product) = S ((S (pa_i_pc_length_components_lower_power_product)) * pa_c_pc_length_components_lower_power)) /\ exists pa_q_pc_length_components_lower_power_product_factor. pa_b_pc_length_components_lower_power = pa_q_pc_length_components_lower_power_product_factor * S ((S (pa_i_pc_length_components_lower_power_product)) * pa_c_pc_length_components_lower_power) + (pa_p_pc_length_components_lower_power_product))) /\ ((((exists pa_h_pc_length_components_lower_power_product_partial. pa_h_pc_length_components_lower_power_product_partial + S (pa_r_pc_length_components_lower_power_product) = S ((S (pa_i_pc_length_components_lower_power_product)) * pa_v_pc_length_components_lower_power_product)) /\ exists pa_q_pc_length_components_lower_power_product_partial. pa_u_pc_length_components_lower_power_product = pa_q_pc_length_components_lower_power_product_partial * S ((S (pa_i_pc_length_components_lower_power_product)) * pa_v_pc_length_components_lower_power_product) + (pa_r_pc_length_components_lower_power_product))) /\ ((((exists pa_h_pc_length_components_lower_power_product_successor. pa_h_pc_length_components_lower_power_product_successor + S (pa_s_pc_length_components_lower_power_product) = S ((S (S pa_i_pc_length_components_lower_power_product)) * pa_v_pc_length_components_lower_power_product)) /\ exists pa_q_pc_length_components_lower_power_product_successor. pa_u_pc_length_components_lower_power_product = pa_q_pc_length_components_lower_power_product_successor * S ((S (S pa_i_pc_length_components_lower_power_product)) * pa_v_pc_length_components_lower_power_product) + (pa_s_pc_length_components_lower_power_product))) /\ pa_s_pc_length_components_lower_power_product = pa_r_pc_length_components_lower_power_product * pa_p_pc_length_components_lower_power_product)))))))) /\ ((exists pa_b_pc_length_components_upper_power pa_c_pc_length_components_upper_power. ((forall pa_i_pc_length_components_upper_power_repeat. (exists pa_lt_pc_length_components_upper_power_repeat_bound. pa_lt_pc_length_components_upper_power_repeat_bound + S pa_i_pc_length_components_upper_power_repeat = ell) -> (((exists pa_h_pc_length_components_upper_power_repeat_decoded. pa_h_pc_length_components_upper_power_repeat_decoded + S (2) = S ((S (pa_i_pc_length_components_upper_power_repeat)) * pa_c_pc_length_components_upper_power)) /\ exists pa_q_pc_length_components_upper_power_repeat_decoded. pa_b_pc_length_components_upper_power = pa_q_pc_length_components_upper_power_repeat_decoded * S ((S (pa_i_pc_length_components_upper_power_repeat)) * pa_c_pc_length_components_upper_power) + (2)))) /\ (exists pa_u_pc_length_components_upper_power_product pa_v_pc_length_components_upper_power_product. ((((exists pa_h_pc_length_components_upper_power_product_start. pa_h_pc_length_components_upper_power_product_start + S (1) = S ((S (0)) * pa_v_pc_length_components_upper_power_product)) /\ exists pa_q_pc_length_components_upper_power_product_start. pa_u_pc_length_components_upper_power_product = pa_q_pc_length_components_upper_power_product_start * S ((S (0)) * pa_v_pc_length_components_upper_power_product) + (1))) /\ ((((exists pa_h_pc_length_components_upper_power_product_terminal. pa_h_pc_length_components_upper_power_product_terminal + S (w) = S ((S (ell)) * pa_v_pc_length_components_upper_power_product)) /\ exists pa_q_pc_length_components_upper_power_product_terminal. pa_u_pc_length_components_upper_power_product = pa_q_pc_length_components_upper_power_product_terminal * S ((S (ell)) * pa_v_pc_length_components_upper_power_product) + (w))) /\ forall pa_i_pc_length_components_upper_power_product. (exists pa_lt_pc_length_components_upper_power_product_bound. pa_lt_pc_length_components_upper_power_product_bound + S pa_i_pc_length_components_upper_power_product = ell) -> exists pa_p_pc_length_components_upper_power_product pa_r_pc_length_components_upper_power_product pa_s_pc_length_components_upper_power_product. ((((exists pa_h_pc_length_components_upper_power_product_factor. pa_h_pc_length_components_upper_power_product_factor + S (pa_p_pc_length_components_upper_power_product) = S ((S (pa_i_pc_length_components_upper_power_product)) * pa_c_pc_length_components_upper_power)) /\ exists pa_q_pc_length_components_upper_power_product_factor. pa_b_pc_length_components_upper_power = pa_q_pc_length_components_upper_power_product_factor * S ((S (pa_i_pc_length_components_upper_power_product)) * pa_c_pc_length_components_upper_power) + (pa_p_pc_length_components_upper_power_product))) /\ ((((exists pa_h_pc_length_components_upper_power_product_partial. pa_h_pc_length_components_upper_power_product_partial + S (pa_r_pc_length_components_upper_power_product) = S ((S (pa_i_pc_length_components_upper_power_product)) * pa_v_pc_length_components_upper_power_product)) /\ exists pa_q_pc_length_components_upper_power_product_partial. pa_u_pc_length_components_upper_power_product = pa_q_pc_length_components_upper_power_product_partial * S ((S (pa_i_pc_length_components_upper_power_product)) * pa_v_pc_length_components_upper_power_product) + (pa_r_pc_length_components_upper_power_product))) /\ ((((exists pa_h_pc_length_components_upper_power_product_successor. pa_h_pc_length_components_upper_power_product_successor + S (pa_s_pc_length_components_upper_power_product) = S ((S (S pa_i_pc_length_components_upper_power_product)) * pa_v_pc_length_components_upper_power_product)) /\ exists pa_q_pc_length_components_upper_power_product_successor. pa_u_pc_length_components_upper_power_product = pa_q_pc_length_components_upper_power_product_successor * S ((S (S pa_i_pc_length_components_upper_power_product)) * pa_v_pc_length_components_upper_power_product) + (pa_s_pc_length_components_upper_power_product))) /\ pa_s_pc_length_components_upper_power_product = pa_r_pc_length_components_upper_power_product * pa_p_pc_length_components_upper_power_product)))))))) /\ ((exists pc_le_length_components_lower. pc_le_length_components_lower + (v) = (n)) /\ (exists pc_lt_length_components_upper. pc_lt_length_components_upper + S (n) = (w)))))

Complete tactic proof in conservative notation

All 26 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

26 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.

01Fix variables and assumptionsL1–4

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

L1
intro n
L2
intro ell
L3
intro hn
L4
intro h

02Separate the logical casesL5–7