BD0009

binary_exponent_digit_prefix_at_length

Every canonical binary-length witness constructs a genuine beta-coded equally long zero-or-one prefix whose base-two Horner value is the original exponent.

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. BitLen(n,l) → ∃ x. ∃ y. BinaryExponentDigitCode(n,l,x,y)

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

Definition DAG

BitLen(n,ell) · 1BinaryExponentDigitCode(e,ell,b,c) · 1

Actual proof prerequisites

binary_length_upper_power_boundbinary_digit_bounded_prefix_exists
Original expanded first-order statement 
forall n l. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_bd_exact_length ff_lower_bl_bd_exact_length ff_upper_bl_bd_exact_length. (((l) = S ff_exponent_bl_bd_exact_length) /\ ((exists ff_positive_bl_bd_exact_length. ff_positive_bl_bd_exact_length + 1 = (n)) /\ ((exists pa_b_bl_bd_exact_length_lower pa_c_bl_bd_exact_length_lower. ((forall pa_i_bl_bd_exact_length_lower_repeat. (exists pa_lt_bl_bd_exact_length_lower_repeat_bound. pa_lt_bl_bd_exact_length_lower_repeat_bound + S pa_i_bl_bd_exact_length_lower_repeat = ff_exponent_bl_bd_exact_length) -> (((exists pa_h_bl_bd_exact_length_lower_repeat_decoded. pa_h_bl_bd_exact_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_exact_length_lower_repeat)) * pa_c_bl_bd_exact_length_lower)) /\ exists pa_q_bl_bd_exact_length_lower_repeat_decoded. pa_b_bl_bd_exact_length_lower = pa_q_bl_bd_exact_length_lower_repeat_decoded * S ((S (pa_i_bl_bd_exact_length_lower_repeat)) * pa_c_bl_bd_exact_length_lower) + (2)))) /\ (exists pa_u_bl_bd_exact_length_lower_product pa_v_bl_bd_exact_length_lower_product. ((((exists pa_h_bl_bd_exact_length_lower_product_start. pa_h_bl_bd_exact_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_start. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_start * S ((S (0)) * pa_v_bl_bd_exact_length_lower_product) + (1))) /\ ((((exists pa_h_bl_bd_exact_length_lower_product_terminal. pa_h_bl_bd_exact_length_lower_product_terminal + S (ff_lower_bl_bd_exact_length) = S ((S (ff_exponent_bl_bd_exact_length)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_terminal. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_terminal * S ((S (ff_exponent_bl_bd_exact_length)) * pa_v_bl_bd_exact_length_lower_product) + (ff_lower_bl_bd_exact_length))) /\ forall pa_i_bl_bd_exact_length_lower_product. (exists pa_lt_bl_bd_exact_length_lower_product_bound. pa_lt_bl_bd_exact_length_lower_product_bound + S pa_i_bl_bd_exact_length_lower_product = ff_exponent_bl_bd_exact_length) -> exists pa_p_bl_bd_exact_length_lower_product pa_r_bl_bd_exact_length_lower_product pa_s_bl_bd_exact_length_lower_product. ((((exists pa_h_bl_bd_exact_length_lower_product_factor. pa_h_bl_bd_exact_length_lower_product_factor + S (pa_p_bl_bd_exact_length_lower_product) = S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_c_bl_bd_exact_length_lower)) /\ exists pa_q_bl_bd_exact_length_lower_product_factor. pa_b_bl_bd_exact_length_lower = pa_q_bl_bd_exact_length_lower_product_factor * S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_c_bl_bd_exact_length_lower) + (pa_p_bl_bd_exact_length_lower_product))) /\ ((((exists pa_h_bl_bd_exact_length_lower_product_partial. pa_h_bl_bd_exact_length_lower_product_partial + S (pa_r_bl_bd_exact_length_lower_product) = S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_partial. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_partial * S ((S (pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product) + (pa_r_bl_bd_exact_length_lower_product))) /\ ((((exists pa_h_bl_bd_exact_length_lower_product_successor. pa_h_bl_bd_exact_length_lower_product_successor + S (pa_s_bl_bd_exact_length_lower_product) = S ((S (S pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product)) /\ exists pa_q_bl_bd_exact_length_lower_product_successor. pa_u_bl_bd_exact_length_lower_product = pa_q_bl_bd_exact_length_lower_product_successor * S ((S (S pa_i_bl_bd_exact_length_lower_product)) * pa_v_bl_bd_exact_length_lower_product) + (pa_s_bl_bd_exact_length_lower_product))) /\ pa_s_bl_bd_exact_length_lower_product = pa_r_bl_bd_exact_length_lower_product * pa_p_bl_bd_exact_length_lower_product)))))))) /\ ((exists pa_b_bl_bd_exact_length_upper pa_c_bl_bd_exact_length_upper. ((forall pa_i_bl_bd_exact_length_upper_repeat. (exists pa_lt_bl_bd_exact_length_upper_repeat_bound. pa_lt_bl_bd_exact_length_upper_repeat_bound + S pa_i_bl_bd_exact_length_upper_repeat = l) -> (((exists pa_h_bl_bd_exact_length_upper_repeat_decoded. pa_h_bl_bd_exact_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_exact_length_upper_repeat)) * pa_c_bl_bd_exact_length_upper)) /\ exists pa_q_bl_bd_exact_length_upper_repeat_decoded. pa_b_bl_bd_exact_length_upper = pa_q_bl_bd_exact_length_upper_repeat_decoded * S ((S (pa_i_bl_bd_exact_length_upper_repeat)) * pa_c_bl_bd_exact_length_upper) + (2)))) /\ (exists pa_u_bl_bd_exact_length_upper_product pa_v_bl_bd_exact_length_upper_product. ((((exists pa_h_bl_bd_exact_length_upper_product_start. pa_h_bl_bd_exact_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_start. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_start * S ((S (0)) * pa_v_bl_bd_exact_length_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_exact_length_upper_product_terminal. pa_h_bl_bd_exact_length_upper_product_terminal + S (ff_upper_bl_bd_exact_length) = S ((S (l)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_terminal. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_exact_length_upper_product) + (ff_upper_bl_bd_exact_length))) /\ forall pa_i_bl_bd_exact_length_upper_product. (exists pa_lt_bl_bd_exact_length_upper_product_bound. pa_lt_bl_bd_exact_length_upper_product_bound + S pa_i_bl_bd_exact_length_upper_product = l) -> exists pa_p_bl_bd_exact_length_upper_product pa_r_bl_bd_exact_length_upper_product pa_s_bl_bd_exact_length_upper_product. ((((exists pa_h_bl_bd_exact_length_upper_product_factor. pa_h_bl_bd_exact_length_upper_product_factor + S (pa_p_bl_bd_exact_length_upper_product) = S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_c_bl_bd_exact_length_upper)) /\ exists pa_q_bl_bd_exact_length_upper_product_factor. pa_b_bl_bd_exact_length_upper = pa_q_bl_bd_exact_length_upper_product_factor * S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_c_bl_bd_exact_length_upper) + (pa_p_bl_bd_exact_length_upper_product))) /\ ((((exists pa_h_bl_bd_exact_length_upper_product_partial. pa_h_bl_bd_exact_length_upper_product_partial + S (pa_r_bl_bd_exact_length_upper_product) = S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_partial. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_partial * S ((S (pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product) + (pa_r_bl_bd_exact_length_upper_product))) /\ ((((exists pa_h_bl_bd_exact_length_upper_product_successor. pa_h_bl_bd_exact_length_upper_product_successor + S (pa_s_bl_bd_exact_length_upper_product) = S ((S (S pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product)) /\ exists pa_q_bl_bd_exact_length_upper_product_successor. pa_u_bl_bd_exact_length_upper_product = pa_q_bl_bd_exact_length_upper_product_successor * S ((S (S pa_i_bl_bd_exact_length_upper_product)) * pa_v_bl_bd_exact_length_upper_product) + (pa_s_bl_bd_exact_length_upper_product))) /\ pa_s_bl_bd_exact_length_upper_product = pa_r_bl_bd_exact_length_upper_product * pa_p_bl_bd_exact_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_bd_exact_length. ff_lower_gap_bl_bd_exact_length + (ff_lower_bl_bd_exact_length) = (n)) /\ (exists ff_upper_gap_bl_bd_exact_length. ff_upper_gap_bl_bd_exact_length + S (n) = (ff_upper_bl_bd_exact_length))))))))) -> exists b c. (((forall ff_index_be_bd_exact_length_digits ff_digit_be_bd_exact_length_digits. (exists ff_lt_be_bd_exact_length_digits_bound. ff_lt_be_bd_exact_length_digits_bound + S ff_index_be_bd_exact_length_digits = l) -> (((exists ff_h_be_bd_exact_length_digits_digit. ff_h_be_bd_exact_length_digits_digit + S (ff_digit_be_bd_exact_length_digits) = S ((S (ff_index_be_bd_exact_length_digits)) * c)) /\ exists ff_q_be_bd_exact_length_digits_digit. b = ff_q_be_bd_exact_length_digits_digit * S ((S (ff_index_be_bd_exact_length_digits)) * c) + (ff_digit_be_bd_exact_length_digits))) -> (ff_digit_be_bd_exact_length_digits = 0 \/ ff_digit_be_bd_exact_length_digits = 1)) /\ (exists ff_u_ph_bd_exact_length_horner ff_v_ph_bd_exact_length_horner. ((((exists fs_h_ph_bd_exact_length_horner_body_start. fs_h_ph_bd_exact_length_horner_body_start + S (0) = S ((S (0)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_start. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_start * S ((S (0)) * ff_v_ph_bd_exact_length_horner) + (0))) /\ ((((exists fs_h_ph_bd_exact_length_horner_body_terminal. fs_h_ph_bd_exact_length_horner_body_terminal + S (n) = S ((S (l)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_terminal. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_terminal * S ((S (l)) * ff_v_ph_bd_exact_length_horner) + (n))) /\ forall ff_i_ph_bd_exact_length_horner_body_steps. (exists ph_bound_bd_exact_length_horner_body_steps. ph_bound_bd_exact_length_horner_body_steps + S ff_i_ph_bd_exact_length_horner_body_steps = l) -> exists ff_coefficient_ph_bd_exact_length_horner_body_steps ff_previous_ph_bd_exact_length_horner_body_steps ff_current_ph_bd_exact_length_horner_body_steps. ((((exists fs_h_ph_bd_exact_length_horner_body_steps_coefficient. fs_h_ph_bd_exact_length_horner_body_steps_coefficient + S (ff_coefficient_ph_bd_exact_length_horner_body_steps) = S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * c)) /\ exists fs_q_ph_bd_exact_length_horner_body_steps_coefficient. b = fs_q_ph_bd_exact_length_horner_body_steps_coefficient * S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * c) + (ff_coefficient_ph_bd_exact_length_horner_body_steps))) /\ ((((exists fs_h_ph_bd_exact_length_horner_body_steps_before. fs_h_ph_bd_exact_length_horner_body_steps_before + S (ff_previous_ph_bd_exact_length_horner_body_steps) = S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_steps_before. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_steps_before * S ((S (ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner) + (ff_previous_ph_bd_exact_length_horner_body_steps))) /\ ((((exists fs_h_ph_bd_exact_length_horner_body_steps_after. fs_h_ph_bd_exact_length_horner_body_steps_after + S (ff_current_ph_bd_exact_length_horner_body_steps) = S ((S (S ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner)) /\ exists fs_q_ph_bd_exact_length_horner_body_steps_after. ff_u_ph_bd_exact_length_horner = fs_q_ph_bd_exact_length_horner_body_steps_after * S ((S (S ff_i_ph_bd_exact_length_horner_body_steps)) * ff_v_ph_bd_exact_length_horner) + (ff_current_ph_bd_exact_length_horner_body_steps))) /\ ff_current_ph_bd_exact_length_horner_body_steps = ff_previous_ph_bd_exact_length_horner_body_steps * 2 + ff_coefficient_ph_bd_exact_length_horner_body_steps))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

16 script commands · 4 reading checkpoints · 1 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 (2)
binary length upper power boundbinary digit bounded prefix exists

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

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

  1. L1
    intro n
  2. L2
    intro l
  3. L3
    intro hlength
02Establish hupperL4–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary length upper power bound.

  1. L4
    have hupper : ∃ p. PowTwo(l,p) ∧ Lt(n,p)Definitions: PowTwoLtOriginal native command in the exact edition
  2. L5
    specialize binary_length_upper_power_bound n
  3. L6
    specialize binary_length_upper_power_bound l
  4. L7
    apply binary_length_upper_power_bound
  5. L8
    exact hlength
03Separate the logical casesL9–10

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

  1. L9
    cases hupper
  2. L10
    cases hupper_witness
04Use earlier factsL11–16

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

  1. L11
    specialize binary_digit_bounded_prefix_exists l
  2. L12
    specialize binary_digit_bounded_prefix_exists x
  3. L13
    specialize binary_digit_bounded_prefix_exists n
  4. L14
    apply binary_digit_bounded_prefix_exists
  5. L15
    exact hupper_witness_left
  6. L16
    exact hupper_witness_right

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003intro hlength
  4. 0004have hupper : exists p. ((exists pa_b_bl_bd_exact_upper pa_c_bl_bd_exact_upper. ((forall pa_i_bl_bd_exact_upper_repeat. (exists pa_lt_bl_bd_exact_upper_repeat_bound. pa_lt_bl_bd_exact_upper_repeat_bound + S pa_i_bl_bd_exact_upper_repeat = l) -> (((exists pa_h_bl_bd_exact_upper_repeat_decoded. pa_h_bl_bd_exact_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_bd_exact_upper_repeat)) * pa_c_bl_bd_exact_upper)) /\ exists pa_q_bl_bd_exact_upper_repeat_decoded. pa_b_bl_bd_exact_upper = pa_q_bl_bd_exact_upper_repeat_decoded * S ((S (pa_i_bl_bd_exact_upper_repeat)) * pa_c_bl_bd_exact_upper) + (2)))) /\ (exists pa_u_bl_bd_exact_upper_product pa_v_bl_bd_exact_upper_product. ((((exists pa_h_bl_bd_exact_upper_product_start. pa_h_bl_bd_exact_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_start. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_start * S ((S (0)) * pa_v_bl_bd_exact_upper_product) + (1))) /\ ((((exists pa_h_bl_bd_exact_upper_product_terminal. pa_h_bl_bd_exact_upper_product_terminal + S (p) = S ((S (l)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_terminal. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_terminal * S ((S (l)) * pa_v_bl_bd_exact_upper_product) + (p))) /\ forall pa_i_bl_bd_exact_upper_product. (exists pa_lt_bl_bd_exact_upper_product_bound. pa_lt_bl_bd_exact_upper_product_bound + S pa_i_bl_bd_exact_upper_product = l) -> exists pa_p_bl_bd_exact_upper_product pa_r_bl_bd_exact_upper_product pa_s_bl_bd_exact_upper_product. ((((exists pa_h_bl_bd_exact_upper_product_factor. pa_h_bl_bd_exact_upper_product_factor + S (pa_p_bl_bd_exact_upper_product) = S ((S (pa_i_bl_bd_exact_upper_product)) * pa_c_bl_bd_exact_upper)) /\ exists pa_q_bl_bd_exact_upper_product_factor. pa_b_bl_bd_exact_upper = pa_q_bl_bd_exact_upper_product_factor * S ((S (pa_i_bl_bd_exact_upper_product)) * pa_c_bl_bd_exact_upper) + (pa_p_bl_bd_exact_upper_product))) /\ ((((exists pa_h_bl_bd_exact_upper_product_partial. pa_h_bl_bd_exact_upper_product_partial + S (pa_r_bl_bd_exact_upper_product) = S ((S (pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_partial. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_partial * S ((S (pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product) + (pa_r_bl_bd_exact_upper_product))) /\ ((((exists pa_h_bl_bd_exact_upper_product_successor. pa_h_bl_bd_exact_upper_product_successor + S (pa_s_bl_bd_exact_upper_product) = S ((S (S pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product)) /\ exists pa_q_bl_bd_exact_upper_product_successor. pa_u_bl_bd_exact_upper_product = pa_q_bl_bd_exact_upper_product_successor * S ((S (S pa_i_bl_bd_exact_upper_product)) * pa_v_bl_bd_exact_upper_product) + (pa_s_bl_bd_exact_upper_product))) /\ pa_s_bl_bd_exact_upper_product = pa_r_bl_bd_exact_upper_product * pa_p_bl_bd_exact_upper_product)))))))) /\ (exists gap. gap + S n = p))
  5. 0005specialize binary_length_upper_power_bound n
  6. 0006specialize binary_length_upper_power_bound l
  7. 0007apply binary_length_upper_power_bound
  8. 0008exact hlength
  9. 0009cases hupper
  10. 0010cases hupper_witness
  11. 0011specialize binary_digit_bounded_prefix_exists l
  12. 0012specialize binary_digit_bounded_prefix_exists x
  13. 0013specialize binary_digit_bounded_prefix_exists n
  14. 0014apply binary_digit_bounded_prefix_exists
  15. 0015exact hupper_witness_left
  16. 0016exact hupper_witness_right