BE0009

binary_execution_step_power_invariant

Every actual zero-or-one modular transition preserves the matching binary-prefix power.

Alpha v34 checked-use · first admitted v22 · 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 at this family's Alpha-v22 first admission: complete execution was proved only for a supplied valid beta-coded digit prefix. G102 is now CLOSED in Alpha v23 for every arbitrary exponent, with actual canonical digits and operations≤3*BitLen(e)+2.

Exact theorem in conservative defined notation

∀ a. ∀ h. ∀ e. ∀ m. ∀ r. ∀ d. ∀ s. BinaryModularPower(a,h,m,r) → BinaryExponentSplit(e,h,d) → BinaryModularStep(m,r,a,d,s) → BinaryModularPower(a,e,m,s)

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

Definition DAG

BinaryExponentSplit(e,h,b) · 1BinaryModularStep(m,u,a,b,r) · 1BinaryModularPower(a,e,m,r) · 2

Actual proof prerequisites

binary_execution_even_power_invariantbinary_execution_odd_power_invariantsucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall a h e m r d s. (exists ff_power_binary_previous_power. ((exists ff_b_binary_previous_power_value ff_c_binary_previous_power_value. ((forall ff_i_binary_previous_power_value_repeat. (exists ff_lt_binary_previous_power_value_repeat_bound. ff_lt_binary_previous_power_value_repeat_bound + S ff_i_binary_previous_power_value_repeat = h) -> (((exists ff_h_binary_previous_power_value_repeat_decoded. ff_h_binary_previous_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_previous_power_value_repeat)) * ff_c_binary_previous_power_value)) /\ exists ff_q_binary_previous_power_value_repeat_decoded. ff_b_binary_previous_power_value = ff_q_binary_previous_power_value_repeat_decoded * S ((S (ff_i_binary_previous_power_value_repeat)) * ff_c_binary_previous_power_value) + (a)))) /\ (exists ff_u_binary_previous_power_value_product ff_v_binary_previous_power_value_product. ((((exists ff_h_binary_previous_power_value_product_start. ff_h_binary_previous_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_previous_power_value_product)) /\ exists ff_q_binary_previous_power_value_product_start. ff_u_binary_previous_power_value_product = ff_q_binary_previous_power_value_product_start * S ((S (0)) * ff_v_binary_previous_power_value_product) + (1))) /\ ((((exists ff_h_binary_previous_power_value_product_terminal. ff_h_binary_previous_power_value_product_terminal + S (ff_power_binary_previous_power) = S ((S (h)) * ff_v_binary_previous_power_value_product)) /\ exists ff_q_binary_previous_power_value_product_terminal. ff_u_binary_previous_power_value_product = ff_q_binary_previous_power_value_product_terminal * S ((S (h)) * ff_v_binary_previous_power_value_product) + (ff_power_binary_previous_power))) /\ forall ff_i_binary_previous_power_value_product. (exists ff_lt_binary_previous_power_value_product_bound. ff_lt_binary_previous_power_value_product_bound + S ff_i_binary_previous_power_value_product = h) -> exists ff_p_binary_previous_power_value_product ff_r_binary_previous_power_value_product ff_s_binary_previous_power_value_product. ((((exists ff_h_binary_previous_power_value_product_factor. ff_h_binary_previous_power_value_product_factor + S (ff_p_binary_previous_power_value_product) = S ((S (ff_i_binary_previous_power_value_product)) * ff_c_binary_previous_power_value)) /\ exists ff_q_binary_previous_power_value_product_factor. ff_b_binary_previous_power_value = ff_q_binary_previous_power_value_product_factor * S ((S (ff_i_binary_previous_power_value_product)) * ff_c_binary_previous_power_value) + (ff_p_binary_previous_power_value_product))) /\ ((((exists ff_h_binary_previous_power_value_product_partial. ff_h_binary_previous_power_value_product_partial + S (ff_r_binary_previous_power_value_product) = S ((S (ff_i_binary_previous_power_value_product)) * ff_v_binary_previous_power_value_product)) /\ exists ff_q_binary_previous_power_value_product_partial. ff_u_binary_previous_power_value_product = ff_q_binary_previous_power_value_product_partial * S ((S (ff_i_binary_previous_power_value_product)) * ff_v_binary_previous_power_value_product) + (ff_r_binary_previous_power_value_product))) /\ ((((exists ff_h_binary_previous_power_value_product_successor. ff_h_binary_previous_power_value_product_successor + S (ff_s_binary_previous_power_value_product) = S ((S (S ff_i_binary_previous_power_value_product)) * ff_v_binary_previous_power_value_product)) /\ exists ff_q_binary_previous_power_value_product_successor. ff_u_binary_previous_power_value_product = ff_q_binary_previous_power_value_product_successor * S ((S (S ff_i_binary_previous_power_value_product)) * ff_v_binary_previous_power_value_product) + (ff_s_binary_previous_power_value_product))) /\ ff_s_binary_previous_power_value_product = ff_r_binary_previous_power_value_product * ff_p_binary_previous_power_value_product)))))))) /\ (((exists ff_gap_binary_previous_power_residue. ff_gap_binary_previous_power_residue + S (r) = m) /\ (exists ff_left_binary_previous_power_residue_congruence ff_right_binary_previous_power_residue_congruence. (ff_power_binary_previous_power) + m * ff_left_binary_previous_power_residue_congruence = (r) + m * ff_right_binary_previous_power_residue_congruence))))) -> ((((d = 0) \/ (d = 1)) /\ e = (h + h) + d)) -> ((((d = 0) /\ (((exists ff_gap_binary_step_square. ff_gap_binary_step_square + S (s) = m) /\ (exists ff_left_binary_step_square_congruence ff_right_binary_step_square_congruence. (r * r) + m * ff_left_binary_step_square_congruence = (s) + m * ff_right_binary_step_square_congruence)))) \/ ((d = 1) /\ (((exists ff_gap_binary_step_multiply. ff_gap_binary_step_multiply + S (s) = m) /\ (exists ff_left_binary_step_multiply_congruence ff_right_binary_step_multiply_congruence. ((r * r) * a) + m * ff_left_binary_step_multiply_congruence = (s) + m * ff_right_binary_step_multiply_congruence)))))) -> (exists ff_power_binary_current_power. ((exists ff_b_binary_current_power_value ff_c_binary_current_power_value. ((forall ff_i_binary_current_power_value_repeat. (exists ff_lt_binary_current_power_value_repeat_bound. ff_lt_binary_current_power_value_repeat_bound + S ff_i_binary_current_power_value_repeat = e) -> (((exists ff_h_binary_current_power_value_repeat_decoded. ff_h_binary_current_power_value_repeat_decoded + S (a) = S ((S (ff_i_binary_current_power_value_repeat)) * ff_c_binary_current_power_value)) /\ exists ff_q_binary_current_power_value_repeat_decoded. ff_b_binary_current_power_value = ff_q_binary_current_power_value_repeat_decoded * S ((S (ff_i_binary_current_power_value_repeat)) * ff_c_binary_current_power_value) + (a)))) /\ (exists ff_u_binary_current_power_value_product ff_v_binary_current_power_value_product. ((((exists ff_h_binary_current_power_value_product_start. ff_h_binary_current_power_value_product_start + S (1) = S ((S (0)) * ff_v_binary_current_power_value_product)) /\ exists ff_q_binary_current_power_value_product_start. ff_u_binary_current_power_value_product = ff_q_binary_current_power_value_product_start * S ((S (0)) * ff_v_binary_current_power_value_product) + (1))) /\ ((((exists ff_h_binary_current_power_value_product_terminal. ff_h_binary_current_power_value_product_terminal + S (ff_power_binary_current_power) = S ((S (e)) * ff_v_binary_current_power_value_product)) /\ exists ff_q_binary_current_power_value_product_terminal. ff_u_binary_current_power_value_product = ff_q_binary_current_power_value_product_terminal * S ((S (e)) * ff_v_binary_current_power_value_product) + (ff_power_binary_current_power))) /\ forall ff_i_binary_current_power_value_product. (exists ff_lt_binary_current_power_value_product_bound. ff_lt_binary_current_power_value_product_bound + S ff_i_binary_current_power_value_product = e) -> exists ff_p_binary_current_power_value_product ff_r_binary_current_power_value_product ff_s_binary_current_power_value_product. ((((exists ff_h_binary_current_power_value_product_factor. ff_h_binary_current_power_value_product_factor + S (ff_p_binary_current_power_value_product) = S ((S (ff_i_binary_current_power_value_product)) * ff_c_binary_current_power_value)) /\ exists ff_q_binary_current_power_value_product_factor. ff_b_binary_current_power_value = ff_q_binary_current_power_value_product_factor * S ((S (ff_i_binary_current_power_value_product)) * ff_c_binary_current_power_value) + (ff_p_binary_current_power_value_product))) /\ ((((exists ff_h_binary_current_power_value_product_partial. ff_h_binary_current_power_value_product_partial + S (ff_r_binary_current_power_value_product) = S ((S (ff_i_binary_current_power_value_product)) * ff_v_binary_current_power_value_product)) /\ exists ff_q_binary_current_power_value_product_partial. ff_u_binary_current_power_value_product = ff_q_binary_current_power_value_product_partial * S ((S (ff_i_binary_current_power_value_product)) * ff_v_binary_current_power_value_product) + (ff_r_binary_current_power_value_product))) /\ ((((exists ff_h_binary_current_power_value_product_successor. ff_h_binary_current_power_value_product_successor + S (ff_s_binary_current_power_value_product) = S ((S (S ff_i_binary_current_power_value_product)) * ff_v_binary_current_power_value_product)) /\ exists ff_q_binary_current_power_value_product_successor. ff_u_binary_current_power_value_product = ff_q_binary_current_power_value_product_successor * S ((S (S ff_i_binary_current_power_value_product)) * ff_v_binary_current_power_value_product) + (ff_s_binary_current_power_value_product))) /\ ff_s_binary_current_power_value_product = ff_r_binary_current_power_value_product * ff_p_binary_current_power_value_product)))))))) /\ (((exists ff_gap_binary_current_power_residue. ff_gap_binary_current_power_residue + S (s) = m) /\ (exists ff_left_binary_current_power_residue_congruence ff_right_binary_current_power_residue_congruence. (ff_power_binary_current_power) + m * ff_left_binary_current_power_residue_congruence = (s) + m * ff_right_binary_current_power_residue_congruence)))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

60 script commands · 18 reading checkpoints · 2 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 execution even power invariantbinary execution odd power invariant
01Fix variables and assumptionsL1–10

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 m
  5. L5
    intro r
  6. L6
    intro d
  7. L7
    intro s
  8. L8
    intro hpower
  9. L9
    intro hsplit
  10. L10
    intro hstep
02Separate the logical casesL11–12

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

  1. L11
    cases hsplit
  2. L12
    cases hsplit_left
03Calculate and transport equalitiesL13–14

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

  1. L13
    rewrite hsplit_left_left at hsplit_right
  2. L14
    rewrite hsplit_left_left at hstep
04Separate the logical casesL15–16

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

  1. L15
    cases hstep
  2. L16
    cases hstep_left
05Establish hevenL17–26

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

  1. L17
    have heven : e = h + h
  2. L18
    trans (h + h) + 0
  3. L19
    exact hsplit_right
  4. L20
    simp
  5. L21
    specialize binary_execution_even_power_invariant a
  6. L22
    specialize binary_execution_even_power_invariant h
  7. L23
    specialize binary_execution_even_power_invariant e
  8. L24
    specialize binary_execution_even_power_invariant m
  9. L25
    specialize binary_execution_even_power_invariant r
  10. L26
    specialize binary_execution_even_power_invariant s
06Use earlier factsL27–30

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

  1. L27
    apply binary_execution_even_power_invariant
  2. L28
    exact heven
  3. L29
    exact hpower
  4. L30
    exact hstep_left_right
07Separate the logical casesL31–31

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

  1. L31
    cases hstep_right
08Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite hsplit_left_left at hstep_right_left
09Separate the logical casesL33–33

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

  1. L33
    exfalso
10Use earlier factsL34–35

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

  1. L34
    specialize succ_ne_zero 0
  2. L35
    apply succ_ne_zero
11Calculate and transport equalitiesL36–36

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

  1. L36
    symm
12Use earlier factsL37–37

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

  1. L37
    exact hstep_right_left
13Calculate and transport equalitiesL38–39

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

  1. L38
    rewrite hsplit_left_right at hsplit_right
  2. L39
    rewrite hsplit_left_right at hstep
14Separate the logical casesL40–42

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

  1. L40
    cases hstep
  2. L41
    cases hstep_left
  3. L42
    exfalso
15Use earlier factsL43–45

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

  1. L43
    specialize succ_ne_zero 0
  2. L44
    apply succ_ne_zero
  3. L45
    exact hstep_left_left
16Separate the logical casesL46–46

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

  1. L46
    cases hstep_right
17Establish hoddL47–56

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

  1. L47
    have hodd : e = S (h + h)
  2. L48
    trans (h + h) + 1
  3. L49
    exact hsplit_right
  4. L50
    simp
  5. L51
    specialize binary_execution_odd_power_invariant a
  6. L52
    specialize binary_execution_odd_power_invariant h
  7. L53
    specialize binary_execution_odd_power_invariant e
  8. L54
    specialize binary_execution_odd_power_invariant m
  9. L55
    specialize binary_execution_odd_power_invariant r
  10. L56
    specialize binary_execution_odd_power_invariant s
18Use earlier factsL57–60

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

  1. L57
    apply binary_execution_odd_power_invariant
  2. L58
    exact hodd
  3. L59
    exact hpower
  4. L60
    exact hstep_right_right

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro a
  2. 0002intro h
  3. 0003intro e
  4. 0004intro m
  5. 0005intro r
  6. 0006intro d
  7. 0007intro s
  8. 0008intro hpower
  9. 0009intro hsplit
  10. 0010intro hstep
  11. 0011cases hsplit
  12. 0012cases hsplit_left
  13. 0013rewrite hsplit_left_left at hsplit_right
  14. 0014rewrite hsplit_left_left at hstep
  15. 0015cases hstep
  16. 0016cases hstep_left
  17. 0017have heven : e = h + h
  18. 0018trans (h + h) + 0
  19. 0019exact hsplit_right
  20. 0020simp
  21. 0021specialize binary_execution_even_power_invariant a
  22. 0022specialize binary_execution_even_power_invariant h
  23. 0023specialize binary_execution_even_power_invariant e
  24. 0024specialize binary_execution_even_power_invariant m
  25. 0025specialize binary_execution_even_power_invariant r
  26. 0026specialize binary_execution_even_power_invariant s
  27. 0027apply binary_execution_even_power_invariant
  28. 0028exact heven
  29. 0029exact hpower
  30. 0030exact hstep_left_right
  31. 0031cases hstep_right
  32. 0032rewrite hsplit_left_left at hstep_right_left
  33. 0033exfalso
  34. 0034specialize succ_ne_zero 0
  35. 0035apply succ_ne_zero
  36. 0036symm
  37. 0037exact hstep_right_left
  38. 0038rewrite hsplit_left_right at hsplit_right
  39. 0039rewrite hsplit_left_right at hstep
  40. 0040cases hstep
  41. 0041cases hstep_left
  42. 0042exfalso
  43. 0043specialize succ_ne_zero 0
  44. 0044apply succ_ne_zero
  45. 0045exact hstep_left_left
  46. 0046cases hstep_right
  47. 0047have hodd : e = S (h + h)
  48. 0048trans (h + h) + 1
  49. 0049exact hsplit_right
  50. 0050simp
  51. 0051specialize binary_execution_odd_power_invariant a
  52. 0052specialize binary_execution_odd_power_invariant h
  53. 0053specialize binary_execution_odd_power_invariant e
  54. 0054specialize binary_execution_odd_power_invariant m
  55. 0055specialize binary_execution_odd_power_invariant r
  56. 0056specialize binary_execution_odd_power_invariant s
  57. 0057apply binary_execution_odd_power_invariant
  58. 0058exact hodd
  59. 0059exact hpower
  60. 0060exact hstep_right_right