BX0007

binary_exponent_odd_power

The relational power at an odd exponent is its squared half power times the base.

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

G102 was OPEN when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: every arbitrary exponent has actual canonical beta-coded digits, a complete modular execution, and exact counted bound operations≤3*BitLen(e)+2.

Exact theorem in conservative defined notation

∀ a. ∀ h. ∀ e. ∀ x. ∀ z. BinaryOddPower(a,h,e,x,z) → z = x · x · a

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

Definition DAG

BinaryOddPower(a,h,e,u,z) · 1

Actual proof prerequisites

pow_exists · checked external prerequisitebinary_exponent_doubled_powerpow_successor_pair_mul · checked external prerequisite
Original expanded first-order statement 
forall a h e x z. (((e = S (h + h)) /\ ((exists ff_b_binary_odd_half ff_c_binary_odd_half. ((forall ff_i_binary_odd_half_repeat. (exists ff_lt_binary_odd_half_repeat_bound. ff_lt_binary_odd_half_repeat_bound + S ff_i_binary_odd_half_repeat = h) -> (((exists ff_h_binary_odd_half_repeat_decoded. ff_h_binary_odd_half_repeat_decoded + S (a) = S ((S (ff_i_binary_odd_half_repeat)) * ff_c_binary_odd_half)) /\ exists ff_q_binary_odd_half_repeat_decoded. ff_b_binary_odd_half = ff_q_binary_odd_half_repeat_decoded * S ((S (ff_i_binary_odd_half_repeat)) * ff_c_binary_odd_half) + (a)))) /\ (exists ff_u_binary_odd_half_product ff_v_binary_odd_half_product. ((((exists ff_h_binary_odd_half_product_start. ff_h_binary_odd_half_product_start + S (1) = S ((S (0)) * ff_v_binary_odd_half_product)) /\ exists ff_q_binary_odd_half_product_start. ff_u_binary_odd_half_product = ff_q_binary_odd_half_product_start * S ((S (0)) * ff_v_binary_odd_half_product) + (1))) /\ ((((exists ff_h_binary_odd_half_product_terminal. ff_h_binary_odd_half_product_terminal + S (x) = S ((S (h)) * ff_v_binary_odd_half_product)) /\ exists ff_q_binary_odd_half_product_terminal. ff_u_binary_odd_half_product = ff_q_binary_odd_half_product_terminal * S ((S (h)) * ff_v_binary_odd_half_product) + (x))) /\ forall ff_i_binary_odd_half_product. (exists ff_lt_binary_odd_half_product_bound. ff_lt_binary_odd_half_product_bound + S ff_i_binary_odd_half_product = h) -> exists ff_p_binary_odd_half_product ff_r_binary_odd_half_product ff_s_binary_odd_half_product. ((((exists ff_h_binary_odd_half_product_factor. ff_h_binary_odd_half_product_factor + S (ff_p_binary_odd_half_product) = S ((S (ff_i_binary_odd_half_product)) * ff_c_binary_odd_half)) /\ exists ff_q_binary_odd_half_product_factor. ff_b_binary_odd_half = ff_q_binary_odd_half_product_factor * S ((S (ff_i_binary_odd_half_product)) * ff_c_binary_odd_half) + (ff_p_binary_odd_half_product))) /\ ((((exists ff_h_binary_odd_half_product_partial. ff_h_binary_odd_half_product_partial + S (ff_r_binary_odd_half_product) = S ((S (ff_i_binary_odd_half_product)) * ff_v_binary_odd_half_product)) /\ exists ff_q_binary_odd_half_product_partial. ff_u_binary_odd_half_product = ff_q_binary_odd_half_product_partial * S ((S (ff_i_binary_odd_half_product)) * ff_v_binary_odd_half_product) + (ff_r_binary_odd_half_product))) /\ ((((exists ff_h_binary_odd_half_product_successor. ff_h_binary_odd_half_product_successor + S (ff_s_binary_odd_half_product) = S ((S (S ff_i_binary_odd_half_product)) * ff_v_binary_odd_half_product)) /\ exists ff_q_binary_odd_half_product_successor. ff_u_binary_odd_half_product = ff_q_binary_odd_half_product_successor * S ((S (S ff_i_binary_odd_half_product)) * ff_v_binary_odd_half_product) + (ff_s_binary_odd_half_product))) /\ ff_s_binary_odd_half_product = ff_r_binary_odd_half_product * ff_p_binary_odd_half_product)))))))) /\ (exists ff_b_binary_odd_full ff_c_binary_odd_full. ((forall ff_i_binary_odd_full_repeat. (exists ff_lt_binary_odd_full_repeat_bound. ff_lt_binary_odd_full_repeat_bound + S ff_i_binary_odd_full_repeat = e) -> (((exists ff_h_binary_odd_full_repeat_decoded. ff_h_binary_odd_full_repeat_decoded + S (a) = S ((S (ff_i_binary_odd_full_repeat)) * ff_c_binary_odd_full)) /\ exists ff_q_binary_odd_full_repeat_decoded. ff_b_binary_odd_full = ff_q_binary_odd_full_repeat_decoded * S ((S (ff_i_binary_odd_full_repeat)) * ff_c_binary_odd_full) + (a)))) /\ (exists ff_u_binary_odd_full_product ff_v_binary_odd_full_product. ((((exists ff_h_binary_odd_full_product_start. ff_h_binary_odd_full_product_start + S (1) = S ((S (0)) * ff_v_binary_odd_full_product)) /\ exists ff_q_binary_odd_full_product_start. ff_u_binary_odd_full_product = ff_q_binary_odd_full_product_start * S ((S (0)) * ff_v_binary_odd_full_product) + (1))) /\ ((((exists ff_h_binary_odd_full_product_terminal. ff_h_binary_odd_full_product_terminal + S (z) = S ((S (e)) * ff_v_binary_odd_full_product)) /\ exists ff_q_binary_odd_full_product_terminal. ff_u_binary_odd_full_product = ff_q_binary_odd_full_product_terminal * S ((S (e)) * ff_v_binary_odd_full_product) + (z))) /\ forall ff_i_binary_odd_full_product. (exists ff_lt_binary_odd_full_product_bound. ff_lt_binary_odd_full_product_bound + S ff_i_binary_odd_full_product = e) -> exists ff_p_binary_odd_full_product ff_r_binary_odd_full_product ff_s_binary_odd_full_product. ((((exists ff_h_binary_odd_full_product_factor. ff_h_binary_odd_full_product_factor + S (ff_p_binary_odd_full_product) = S ((S (ff_i_binary_odd_full_product)) * ff_c_binary_odd_full)) /\ exists ff_q_binary_odd_full_product_factor. ff_b_binary_odd_full = ff_q_binary_odd_full_product_factor * S ((S (ff_i_binary_odd_full_product)) * ff_c_binary_odd_full) + (ff_p_binary_odd_full_product))) /\ ((((exists ff_h_binary_odd_full_product_partial. ff_h_binary_odd_full_product_partial + S (ff_r_binary_odd_full_product) = S ((S (ff_i_binary_odd_full_product)) * ff_v_binary_odd_full_product)) /\ exists ff_q_binary_odd_full_product_partial. ff_u_binary_odd_full_product = ff_q_binary_odd_full_product_partial * S ((S (ff_i_binary_odd_full_product)) * ff_v_binary_odd_full_product) + (ff_r_binary_odd_full_product))) /\ ((((exists ff_h_binary_odd_full_product_successor. ff_h_binary_odd_full_product_successor + S (ff_s_binary_odd_full_product) = S ((S (S ff_i_binary_odd_full_product)) * ff_v_binary_odd_full_product)) /\ exists ff_q_binary_odd_full_product_successor. ff_u_binary_odd_full_product = ff_q_binary_odd_full_product_successor * S ((S (S ff_i_binary_odd_full_product)) * ff_v_binary_odd_full_product) + (ff_s_binary_odd_full_product))) /\ ff_s_binary_odd_full_product = ff_r_binary_odd_full_product * ff_p_binary_odd_full_product))))))))))) -> z = (x * x) * a

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

40 script commands · 15 reading checkpoints · 3 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)
binary exponent doubled power

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

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

  1. L1
    intro a
  2. L2
    intro h
  3. L3
    intro e
  4. L4
    intro x
  5. L5
    intro z
  6. L6
    intro hodd
02Separate the logical casesL7–8

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

  1. L7
    cases hodd
  2. L8
    cases hodd_right
03Establish hdoubleL9–12

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hdouble : ∃ y. Pow(a,h + h,y)Definitions: PowOriginal native command in the exact edition
  2. L10
    specialize pow_exists a
  3. L11
    specialize pow_exists (h + h)
  4. L12
    exact pow_exists
04Separate the logical casesL13–13

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

  1. L13
    cases hdouble
05Establish hsquareL14–20

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

  1. L14
    have hsquare : x1 = x * x
  2. L15
    specialize binary_exponent_doubled_power a
  3. L16
    specialize binary_exponent_doubled_power h
  4. L17
    specialize binary_exponent_doubled_power (h + h)
  5. L18
    specialize binary_exponent_doubled_power x
  6. L19
    specialize binary_exponent_doubled_power x1
  7. L20
    apply binary_exponent_doubled_power
06Separate the logical casesL21–21

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

  1. L21
    split
07Calculate and transport equalitiesL22–22

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

  1. L22
    refl
08Separate the logical casesL23–23

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

  1. L23
    split
09Use earlier factsL24–25

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

  1. L24
    exact hodd_right_left
  2. L25
    exact hdouble_witness
10Establish hsuccessorL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor pair mul.

  1. L26
    have hsuccessor : z = x1 * a
  2. L27
    specialize pow_successor_pair_mul a
  3. L28
    specialize pow_successor_pair_mul (h + h)
  4. L29
    specialize pow_successor_pair_mul e
  5. L30
    specialize pow_successor_pair_mul x1
  6. L31
    specialize pow_successor_pair_mul z
  7. L32
    apply pow_successor_pair_mul
  8. L33
    exact hodd_left
  9. L34
    exact hdouble_witness
  10. L35
    exact hodd_right_right
11Calculate and transport equalitiesL36–36

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

  1. L36
    trans x1 * a
12Use earlier factsL37–37

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

  1. L37
    exact hsuccessor
13Calculate and transport equalitiesL38–38

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

  1. L38
    congr
14Use earlier factsL39–39

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

  1. L39
    exact hsquare
15Calculate and transport equalitiesL40–40

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

  1. L40
    refl

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro a
  2. 0002intro h
  3. 0003intro e
  4. 0004intro x
  5. 0005intro z
  6. 0006intro hodd
  7. 0007cases hodd
  8. 0008cases hodd_right
  9. 0009have hdouble : exists y. (exists pa_b_binary_odd_double pa_c_binary_odd_double. ((forall pa_i_binary_odd_double_repeat. (exists pa_lt_binary_odd_double_repeat_bound. pa_lt_binary_odd_double_repeat_bound + S pa_i_binary_odd_double_repeat = h + h) -> (((exists pa_h_binary_odd_double_repeat_decoded. pa_h_binary_odd_double_repeat_decoded + S (a) = S ((S (pa_i_binary_odd_double_repeat)) * pa_c_binary_odd_double)) /\ exists pa_q_binary_odd_double_repeat_decoded. pa_b_binary_odd_double = pa_q_binary_odd_double_repeat_decoded * S ((S (pa_i_binary_odd_double_repeat)) * pa_c_binary_odd_double) + (a)))) /\ (exists pa_u_binary_odd_double_product pa_v_binary_odd_double_product. ((((exists pa_h_binary_odd_double_product_start. pa_h_binary_odd_double_product_start + S (1) = S ((S (0)) * pa_v_binary_odd_double_product)) /\ exists pa_q_binary_odd_double_product_start. pa_u_binary_odd_double_product = pa_q_binary_odd_double_product_start * S ((S (0)) * pa_v_binary_odd_double_product) + (1))) /\ ((((exists pa_h_binary_odd_double_product_terminal. pa_h_binary_odd_double_product_terminal + S (y) = S ((S (h + h)) * pa_v_binary_odd_double_product)) /\ exists pa_q_binary_odd_double_product_terminal. pa_u_binary_odd_double_product = pa_q_binary_odd_double_product_terminal * S ((S (h + h)) * pa_v_binary_odd_double_product) + (y))) /\ forall pa_i_binary_odd_double_product. (exists pa_lt_binary_odd_double_product_bound. pa_lt_binary_odd_double_product_bound + S pa_i_binary_odd_double_product = h + h) -> exists pa_p_binary_odd_double_product pa_r_binary_odd_double_product pa_s_binary_odd_double_product. ((((exists pa_h_binary_odd_double_product_factor. pa_h_binary_odd_double_product_factor + S (pa_p_binary_odd_double_product) = S ((S (pa_i_binary_odd_double_product)) * pa_c_binary_odd_double)) /\ exists pa_q_binary_odd_double_product_factor. pa_b_binary_odd_double = pa_q_binary_odd_double_product_factor * S ((S (pa_i_binary_odd_double_product)) * pa_c_binary_odd_double) + (pa_p_binary_odd_double_product))) /\ ((((exists pa_h_binary_odd_double_product_partial. pa_h_binary_odd_double_product_partial + S (pa_r_binary_odd_double_product) = S ((S (pa_i_binary_odd_double_product)) * pa_v_binary_odd_double_product)) /\ exists pa_q_binary_odd_double_product_partial. pa_u_binary_odd_double_product = pa_q_binary_odd_double_product_partial * S ((S (pa_i_binary_odd_double_product)) * pa_v_binary_odd_double_product) + (pa_r_binary_odd_double_product))) /\ ((((exists pa_h_binary_odd_double_product_successor. pa_h_binary_odd_double_product_successor + S (pa_s_binary_odd_double_product) = S ((S (S pa_i_binary_odd_double_product)) * pa_v_binary_odd_double_product)) /\ exists pa_q_binary_odd_double_product_successor. pa_u_binary_odd_double_product = pa_q_binary_odd_double_product_successor * S ((S (S pa_i_binary_odd_double_product)) * pa_v_binary_odd_double_product) + (pa_s_binary_odd_double_product))) /\ pa_s_binary_odd_double_product = pa_r_binary_odd_double_product * pa_p_binary_odd_double_product))))))))
  10. 0010specialize pow_exists a
  11. 0011specialize pow_exists (h + h)
  12. 0012exact pow_exists
  13. 0013cases hdouble
  14. 0014have hsquare : x1 = x * x
  15. 0015specialize binary_exponent_doubled_power a
  16. 0016specialize binary_exponent_doubled_power h
  17. 0017specialize binary_exponent_doubled_power (h + h)
  18. 0018specialize binary_exponent_doubled_power x
  19. 0019specialize binary_exponent_doubled_power x1
  20. 0020apply binary_exponent_doubled_power
  21. 0021split
  22. 0022refl
  23. 0023split
  24. 0024exact hodd_right_left
  25. 0025exact hdouble_witness
  26. 0026have hsuccessor : z = x1 * a
  27. 0027specialize pow_successor_pair_mul a
  28. 0028specialize pow_successor_pair_mul (h + h)
  29. 0029specialize pow_successor_pair_mul e
  30. 0030specialize pow_successor_pair_mul x1
  31. 0031specialize pow_successor_pair_mul z
  32. 0032apply pow_successor_pair_mul
  33. 0033exact hodd_left
  34. 0034exact hdouble_witness
  35. 0035exact hodd_right_right
  36. 0036trans x1 * a
  37. 0037exact hsuccessor
  38. 0038congr
  39. 0039exact hsquare
  40. 0040refl