PC0024

binary_length_positive

The established binary-length convention always has positive length, including zero input.

Alpha v34 checked-use · first admitted v27 · 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.

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. BitLen(n,ell) → Lt(0,ell)

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

Definition DAG

BitLen(n,ell) · 1Lt(a,b) · 1

Actual proof prerequisites

le_refl · checked external prerequisite
Original expanded first-order statement 
forall n ell. ((((n) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_length_positive_source ff_lower_bl_pc_length_positive_source ff_upper_bl_pc_length_positive_source. (((ell) = S ff_exponent_bl_pc_length_positive_source) /\ ((exists ff_positive_bl_pc_length_positive_source. ff_positive_bl_pc_length_positive_source + 1 = (n)) /\ ((exists pa_b_bl_pc_length_positive_source_lower pa_c_bl_pc_length_positive_source_lower. ((forall pa_i_bl_pc_length_positive_source_lower_repeat. (exists pa_lt_bl_pc_length_positive_source_lower_repeat_bound. pa_lt_bl_pc_length_positive_source_lower_repeat_bound + S pa_i_bl_pc_length_positive_source_lower_repeat = ff_exponent_bl_pc_length_positive_source) -> (((exists pa_h_bl_pc_length_positive_source_lower_repeat_decoded. pa_h_bl_pc_length_positive_source_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_length_positive_source_lower_repeat)) * pa_c_bl_pc_length_positive_source_lower)) /\ exists pa_q_bl_pc_length_positive_source_lower_repeat_decoded. pa_b_bl_pc_length_positive_source_lower = pa_q_bl_pc_length_positive_source_lower_repeat_decoded * S ((S (pa_i_bl_pc_length_positive_source_lower_repeat)) * pa_c_bl_pc_length_positive_source_lower) + (2)))) /\ (exists pa_u_bl_pc_length_positive_source_lower_product pa_v_bl_pc_length_positive_source_lower_product. ((((exists pa_h_bl_pc_length_positive_source_lower_product_start. pa_h_bl_pc_length_positive_source_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_length_positive_source_lower_product)) /\ exists pa_q_bl_pc_length_positive_source_lower_product_start. pa_u_bl_pc_length_positive_source_lower_product = pa_q_bl_pc_length_positive_source_lower_product_start * S ((S (0)) * pa_v_bl_pc_length_positive_source_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_length_positive_source_lower_product_terminal. pa_h_bl_pc_length_positive_source_lower_product_terminal + S (ff_lower_bl_pc_length_positive_source) = S ((S (ff_exponent_bl_pc_length_positive_source)) * pa_v_bl_pc_length_positive_source_lower_product)) /\ exists pa_q_bl_pc_length_positive_source_lower_product_terminal. pa_u_bl_pc_length_positive_source_lower_product = pa_q_bl_pc_length_positive_source_lower_product_terminal * S ((S (ff_exponent_bl_pc_length_positive_source)) * pa_v_bl_pc_length_positive_source_lower_product) + (ff_lower_bl_pc_length_positive_source))) /\ forall pa_i_bl_pc_length_positive_source_lower_product. (exists pa_lt_bl_pc_length_positive_source_lower_product_bound. pa_lt_bl_pc_length_positive_source_lower_product_bound + S pa_i_bl_pc_length_positive_source_lower_product = ff_exponent_bl_pc_length_positive_source) -> exists pa_p_bl_pc_length_positive_source_lower_product pa_r_bl_pc_length_positive_source_lower_product pa_s_bl_pc_length_positive_source_lower_product. ((((exists pa_h_bl_pc_length_positive_source_lower_product_factor. pa_h_bl_pc_length_positive_source_lower_product_factor + S (pa_p_bl_pc_length_positive_source_lower_product) = S ((S (pa_i_bl_pc_length_positive_source_lower_product)) * pa_c_bl_pc_length_positive_source_lower)) /\ exists pa_q_bl_pc_length_positive_source_lower_product_factor. pa_b_bl_pc_length_positive_source_lower = pa_q_bl_pc_length_positive_source_lower_product_factor * S ((S (pa_i_bl_pc_length_positive_source_lower_product)) * pa_c_bl_pc_length_positive_source_lower) + (pa_p_bl_pc_length_positive_source_lower_product))) /\ ((((exists pa_h_bl_pc_length_positive_source_lower_product_partial. pa_h_bl_pc_length_positive_source_lower_product_partial + S (pa_r_bl_pc_length_positive_source_lower_product) = S ((S (pa_i_bl_pc_length_positive_source_lower_product)) * pa_v_bl_pc_length_positive_source_lower_product)) /\ exists pa_q_bl_pc_length_positive_source_lower_product_partial. pa_u_bl_pc_length_positive_source_lower_product = pa_q_bl_pc_length_positive_source_lower_product_partial * S ((S (pa_i_bl_pc_length_positive_source_lower_product)) * pa_v_bl_pc_length_positive_source_lower_product) + (pa_r_bl_pc_length_positive_source_lower_product))) /\ ((((exists pa_h_bl_pc_length_positive_source_lower_product_successor. pa_h_bl_pc_length_positive_source_lower_product_successor + S (pa_s_bl_pc_length_positive_source_lower_product) = S ((S (S pa_i_bl_pc_length_positive_source_lower_product)) * pa_v_bl_pc_length_positive_source_lower_product)) /\ exists pa_q_bl_pc_length_positive_source_lower_product_successor. pa_u_bl_pc_length_positive_source_lower_product = pa_q_bl_pc_length_positive_source_lower_product_successor * S ((S (S pa_i_bl_pc_length_positive_source_lower_product)) * pa_v_bl_pc_length_positive_source_lower_product) + (pa_s_bl_pc_length_positive_source_lower_product))) /\ pa_s_bl_pc_length_positive_source_lower_product = pa_r_bl_pc_length_positive_source_lower_product * pa_p_bl_pc_length_positive_source_lower_product)))))))) /\ ((exists pa_b_bl_pc_length_positive_source_upper pa_c_bl_pc_length_positive_source_upper. ((forall pa_i_bl_pc_length_positive_source_upper_repeat. (exists pa_lt_bl_pc_length_positive_source_upper_repeat_bound. pa_lt_bl_pc_length_positive_source_upper_repeat_bound + S pa_i_bl_pc_length_positive_source_upper_repeat = ell) -> (((exists pa_h_bl_pc_length_positive_source_upper_repeat_decoded. pa_h_bl_pc_length_positive_source_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_length_positive_source_upper_repeat)) * pa_c_bl_pc_length_positive_source_upper)) /\ exists pa_q_bl_pc_length_positive_source_upper_repeat_decoded. pa_b_bl_pc_length_positive_source_upper = pa_q_bl_pc_length_positive_source_upper_repeat_decoded * S ((S (pa_i_bl_pc_length_positive_source_upper_repeat)) * pa_c_bl_pc_length_positive_source_upper) + (2)))) /\ (exists pa_u_bl_pc_length_positive_source_upper_product pa_v_bl_pc_length_positive_source_upper_product. ((((exists pa_h_bl_pc_length_positive_source_upper_product_start. pa_h_bl_pc_length_positive_source_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_length_positive_source_upper_product)) /\ exists pa_q_bl_pc_length_positive_source_upper_product_start. pa_u_bl_pc_length_positive_source_upper_product = pa_q_bl_pc_length_positive_source_upper_product_start * S ((S (0)) * pa_v_bl_pc_length_positive_source_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_length_positive_source_upper_product_terminal. pa_h_bl_pc_length_positive_source_upper_product_terminal + S (ff_upper_bl_pc_length_positive_source) = S ((S (ell)) * pa_v_bl_pc_length_positive_source_upper_product)) /\ exists pa_q_bl_pc_length_positive_source_upper_product_terminal. pa_u_bl_pc_length_positive_source_upper_product = pa_q_bl_pc_length_positive_source_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_length_positive_source_upper_product) + (ff_upper_bl_pc_length_positive_source))) /\ forall pa_i_bl_pc_length_positive_source_upper_product. (exists pa_lt_bl_pc_length_positive_source_upper_product_bound. pa_lt_bl_pc_length_positive_source_upper_product_bound + S pa_i_bl_pc_length_positive_source_upper_product = ell) -> exists pa_p_bl_pc_length_positive_source_upper_product pa_r_bl_pc_length_positive_source_upper_product pa_s_bl_pc_length_positive_source_upper_product. ((((exists pa_h_bl_pc_length_positive_source_upper_product_factor. pa_h_bl_pc_length_positive_source_upper_product_factor + S (pa_p_bl_pc_length_positive_source_upper_product) = S ((S (pa_i_bl_pc_length_positive_source_upper_product)) * pa_c_bl_pc_length_positive_source_upper)) /\ exists pa_q_bl_pc_length_positive_source_upper_product_factor. pa_b_bl_pc_length_positive_source_upper = pa_q_bl_pc_length_positive_source_upper_product_factor * S ((S (pa_i_bl_pc_length_positive_source_upper_product)) * pa_c_bl_pc_length_positive_source_upper) + (pa_p_bl_pc_length_positive_source_upper_product))) /\ ((((exists pa_h_bl_pc_length_positive_source_upper_product_partial. pa_h_bl_pc_length_positive_source_upper_product_partial + S (pa_r_bl_pc_length_positive_source_upper_product) = S ((S (pa_i_bl_pc_length_positive_source_upper_product)) * pa_v_bl_pc_length_positive_source_upper_product)) /\ exists pa_q_bl_pc_length_positive_source_upper_product_partial. pa_u_bl_pc_length_positive_source_upper_product = pa_q_bl_pc_length_positive_source_upper_product_partial * S ((S (pa_i_bl_pc_length_positive_source_upper_product)) * pa_v_bl_pc_length_positive_source_upper_product) + (pa_r_bl_pc_length_positive_source_upper_product))) /\ ((((exists pa_h_bl_pc_length_positive_source_upper_product_successor. pa_h_bl_pc_length_positive_source_upper_product_successor + S (pa_s_bl_pc_length_positive_source_upper_product) = S ((S (S pa_i_bl_pc_length_positive_source_upper_product)) * pa_v_bl_pc_length_positive_source_upper_product)) /\ exists pa_q_bl_pc_length_positive_source_upper_product_successor. pa_u_bl_pc_length_positive_source_upper_product = pa_q_bl_pc_length_positive_source_upper_product_successor * S ((S (S pa_i_bl_pc_length_positive_source_upper_product)) * pa_v_bl_pc_length_positive_source_upper_product) + (pa_s_bl_pc_length_positive_source_upper_product))) /\ pa_s_bl_pc_length_positive_source_upper_product = pa_r_bl_pc_length_positive_source_upper_product * pa_p_bl_pc_length_positive_source_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_length_positive_source. ff_lower_gap_bl_pc_length_positive_source + (ff_lower_bl_pc_length_positive_source) = (n)) /\ (exists ff_upper_gap_bl_pc_length_positive_source. ff_upper_gap_bl_pc_length_positive_source + S (n) = (ff_upper_bl_pc_length_positive_source))))))))) -> (exists pc_le_length_positive_result. pc_le_length_positive_result + (1) = (ell))

Complete tactic proof in conservative notation

All 15 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

15 script commands · 8 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–3

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

  1. L1
    intro n
  2. L2
    intro ell
  3. L3
    intro h
02Separate the logical casesL4–5

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

  1. L4
    cases h
  2. L5
    cases h_left
03Calculate and transport equalitiesL6–6

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L6
    rewrite h_left_right
04Use earlier factsL7–8

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

  1. L7
    specialize le_refl 1
  2. L8
    apply le_refl
05Separate the logical casesL9–12

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

  1. L9
    cases h_right
  2. L10
    cases h_right_witness
  3. L11
    cases h_right_witness_witness
  4. L12
    cases h_right_witness_witness_witness
06Calculate and transport equalitiesL13–13

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L13
    rewrite h_right_witness_witness_witness_left
07Construct an explicit witnessL14–14

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

  1. L14
    exists x
08Calculate and transport equalitiesL15–15

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L15
    simp

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro n
  2. 0002intro ell
  3. 0003intro h
  4. 0004cases h
  5. 0005cases h_left
  6. 0006rewrite h_left_right
  7. 0007specialize le_refl 1
  8. 0008apply le_refl
  9. 0009cases h_right
  10. 0010cases h_right_witness
  11. 0011cases h_right_witness_witness
  12. 0012cases h_right_witness_witness_witness
  13. 0013rewrite h_right_witness_witness_witness_left
  14. 0014exists x
  15. 0015simp