BE0008

binary_execution_odd_power_invariant

One exact binary one transition preserves the witnessed canonical power invariant.

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. ∀ s. e = S (h + h) → BinaryModularPower(a,h,m,r) → CanonicalModularResidue(m,r · r · a,s) → BinaryModularPower(a,e,m,s)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1BinaryModularPower(a,e,m,r) · 2

Actual proof prerequisites

pow_exists · checked external prerequisitebinary_exponent_odd_power · checked external prerequisitebinary_modular_square_congruence · checked external prerequisitemod_eq_refl · checked external prerequisitemod_eq_mul · checked external prerequisitemod_eq_trans · checked external prerequisite
Original expanded first-order statement 
forall a h e m r s. e = S (h + h) -> (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))))) -> (((exists ff_gap_binary_execution_odd. ff_gap_binary_execution_odd + S (s) = m) /\ (exists ff_left_binary_execution_odd_congruence ff_right_binary_execution_odd_congruence. ((r * r) * a) + m * ff_left_binary_execution_odd_congruence = (s) + m * ff_right_binary_execution_odd_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 64 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

64 script commands · 20 reading checkpoints · 6 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.

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

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 s
  7. L7
    intro he
  8. L8
    intro hprevious
  9. L9
    intro hresidue
02Separate the logical casesL10–13

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

  1. L10
    cases hprevious
  2. L11
    cases hprevious_witness
  3. L12
    cases hprevious_witness_right
  4. L13
    cases hresidue
03Establish hpowerL14–17

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

  1. L14
    have hpower : ∃ y. Pow(a,e,y)Definitions: PowOriginal native command in the exact edition
  2. L15
    specialize pow_exists a
  3. L16
    specialize pow_exists e
  4. L17
    exact pow_exists
04Separate the logical casesL18–18

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

  1. L18
    cases hpower
05Establish hoddL19–25

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

  1. L19
    have hodd : x1 = (x * x) * a
  2. L20
    specialize binary_exponent_odd_power a
  3. L21
    specialize binary_exponent_odd_power h
  4. L22
    specialize binary_exponent_odd_power e
  5. L23
    specialize binary_exponent_odd_power x
  6. L24
    specialize binary_exponent_odd_power x1
  7. L25
    apply binary_exponent_odd_power
06Separate the logical casesL26–26

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

  1. L26
    split
07Use earlier factsL27–27

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

  1. L27
    exact he
08Separate the logical casesL28–28

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

  1. L28
    split
09Use earlier factsL29–30

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

  1. L29
    exact hprevious_witness_left
  2. L30
    exact hpower_witness
10Establish hsquareL31–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary modular square congruence.

  1. L31
    have hsquare : exists ff_left_binary_execution_odd_square ff_right_binary_execution_odd_square. (x * x) + m * ff_left_binary_execution_odd_square = (r * r) + m * ff_right_binary_execution_odd_square
  2. L32
    specialize binary_modular_square_congruence m
  3. L33
    specialize binary_modular_square_congruence x
  4. L34
    specialize binary_modular_square_congruence r
  5. L35
    apply binary_modular_square_congruence
  6. L36
    exact hprevious_witness_right_right
11Establish hbaseL37–40

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

  1. L37
    have hbase : exists ff_left_binary_execution_odd_base ff_right_binary_execution_odd_base. (a) + m * ff_left_binary_execution_odd_base = (a) + m * ff_right_binary_execution_odd_base
  2. L38
    specialize mod_eq_refl m
  3. L39
    specialize mod_eq_refl a
  4. L40
    exact mod_eq_refl
12Establish hproductL41–49

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

  1. L41
    have hproduct : exists ff_left_binary_execution_odd_product ff_right_binary_execution_odd_product. ((x * x) * a) + m * ff_left_binary_execution_odd_product = ((r * r) * a) + m * ff_right_binary_execution_odd_product
  2. L42
    specialize mod_eq_mul m
  3. L43
    specialize mod_eq_mul (x * x)
  4. L44
    specialize mod_eq_mul (r * r)
  5. L45
    specialize mod_eq_mul a
  6. L46
    specialize mod_eq_mul a
  7. L47
    apply mod_eq_mul
  8. L48
    exact hsquare
  9. L49
    exact hbase
13Establish htotalL50–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L50
    have htotal : exists ff_left_binary_execution_odd_total ff_right_binary_execution_odd_total. ((x * x) * a) + m * ff_left_binary_execution_odd_total = (s) + m * ff_right_binary_execution_odd_total
  2. L51
    specialize mod_eq_trans m
  3. L52
    specialize mod_eq_trans ((x * x) * a)
  4. L53
    specialize mod_eq_trans ((r * r) * a)
  5. L54
    specialize mod_eq_trans s
  6. L55
    apply mod_eq_trans
  7. L56
    exact hproduct
  8. L57
    exact hresidue_right
14Construct an explicit witnessL58–58

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

  1. L58
    exists x1
15Separate the logical casesL59–59

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

  1. L59
    split
16Use earlier factsL60–60

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

  1. L60
    exact hpower_witness
17Separate the logical casesL61–61

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

  1. L61
    split
18Use earlier factsL62–62

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

  1. L62
    exact hresidue_left
19Calculate and transport equalitiesL63–63

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

  1. L63
    rewrite hodd
20Use earlier factsL64–64

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

  1. L64
    exact htotal

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro a
  2. 0002intro h
  3. 0003intro e
  4. 0004intro m
  5. 0005intro r
  6. 0006intro s
  7. 0007intro he
  8. 0008intro hprevious
  9. 0009intro hresidue
  10. 0010cases hprevious
  11. 0011cases hprevious_witness
  12. 0012cases hprevious_witness_right
  13. 0013cases hresidue
  14. 0014have hpower : exists y. (exists ff_b_be_odd_full ff_c_be_odd_full. ((forall ff_i_be_odd_full_repeat. (exists ff_lt_be_odd_full_repeat_bound. ff_lt_be_odd_full_repeat_bound + S ff_i_be_odd_full_repeat = e) -> (((exists ff_h_be_odd_full_repeat_decoded. ff_h_be_odd_full_repeat_decoded + S (a) = S ((S (ff_i_be_odd_full_repeat)) * ff_c_be_odd_full)) /\ exists ff_q_be_odd_full_repeat_decoded. ff_b_be_odd_full = ff_q_be_odd_full_repeat_decoded * S ((S (ff_i_be_odd_full_repeat)) * ff_c_be_odd_full) + (a)))) /\ (exists ff_u_be_odd_full_product ff_v_be_odd_full_product. ((((exists ff_h_be_odd_full_product_start. ff_h_be_odd_full_product_start + S (1) = S ((S (0)) * ff_v_be_odd_full_product)) /\ exists ff_q_be_odd_full_product_start. ff_u_be_odd_full_product = ff_q_be_odd_full_product_start * S ((S (0)) * ff_v_be_odd_full_product) + (1))) /\ ((((exists ff_h_be_odd_full_product_terminal. ff_h_be_odd_full_product_terminal + S (y) = S ((S (e)) * ff_v_be_odd_full_product)) /\ exists ff_q_be_odd_full_product_terminal. ff_u_be_odd_full_product = ff_q_be_odd_full_product_terminal * S ((S (e)) * ff_v_be_odd_full_product) + (y))) /\ forall ff_i_be_odd_full_product. (exists ff_lt_be_odd_full_product_bound. ff_lt_be_odd_full_product_bound + S ff_i_be_odd_full_product = e) -> exists ff_p_be_odd_full_product ff_r_be_odd_full_product ff_s_be_odd_full_product. ((((exists ff_h_be_odd_full_product_factor. ff_h_be_odd_full_product_factor + S (ff_p_be_odd_full_product) = S ((S (ff_i_be_odd_full_product)) * ff_c_be_odd_full)) /\ exists ff_q_be_odd_full_product_factor. ff_b_be_odd_full = ff_q_be_odd_full_product_factor * S ((S (ff_i_be_odd_full_product)) * ff_c_be_odd_full) + (ff_p_be_odd_full_product))) /\ ((((exists ff_h_be_odd_full_product_partial. ff_h_be_odd_full_product_partial + S (ff_r_be_odd_full_product) = S ((S (ff_i_be_odd_full_product)) * ff_v_be_odd_full_product)) /\ exists ff_q_be_odd_full_product_partial. ff_u_be_odd_full_product = ff_q_be_odd_full_product_partial * S ((S (ff_i_be_odd_full_product)) * ff_v_be_odd_full_product) + (ff_r_be_odd_full_product))) /\ ((((exists ff_h_be_odd_full_product_successor. ff_h_be_odd_full_product_successor + S (ff_s_be_odd_full_product) = S ((S (S ff_i_be_odd_full_product)) * ff_v_be_odd_full_product)) /\ exists ff_q_be_odd_full_product_successor. ff_u_be_odd_full_product = ff_q_be_odd_full_product_successor * S ((S (S ff_i_be_odd_full_product)) * ff_v_be_odd_full_product) + (ff_s_be_odd_full_product))) /\ ff_s_be_odd_full_product = ff_r_be_odd_full_product * ff_p_be_odd_full_product))))))))
  15. 0015specialize pow_exists a
  16. 0016specialize pow_exists e
  17. 0017exact pow_exists
  18. 0018cases hpower
  19. 0019have hodd : x1 = (x * x) * a
  20. 0020specialize binary_exponent_odd_power a
  21. 0021specialize binary_exponent_odd_power h
  22. 0022specialize binary_exponent_odd_power e
  23. 0023specialize binary_exponent_odd_power x
  24. 0024specialize binary_exponent_odd_power x1
  25. 0025apply binary_exponent_odd_power
  26. 0026split
  27. 0027exact he
  28. 0028split
  29. 0029exact hprevious_witness_left
  30. 0030exact hpower_witness
  31. 0031have hsquare : exists ff_left_binary_execution_odd_square ff_right_binary_execution_odd_square. (x * x) + m * ff_left_binary_execution_odd_square = (r * r) + m * ff_right_binary_execution_odd_square
  32. 0032specialize binary_modular_square_congruence m
  33. 0033specialize binary_modular_square_congruence x
  34. 0034specialize binary_modular_square_congruence r
  35. 0035apply binary_modular_square_congruence
  36. 0036exact hprevious_witness_right_right
  37. 0037have hbase : exists ff_left_binary_execution_odd_base ff_right_binary_execution_odd_base. (a) + m * ff_left_binary_execution_odd_base = (a) + m * ff_right_binary_execution_odd_base
  38. 0038specialize mod_eq_refl m
  39. 0039specialize mod_eq_refl a
  40. 0040exact mod_eq_refl
  41. 0041have hproduct : exists ff_left_binary_execution_odd_product ff_right_binary_execution_odd_product. ((x * x) * a) + m * ff_left_binary_execution_odd_product = ((r * r) * a) + m * ff_right_binary_execution_odd_product
  42. 0042specialize mod_eq_mul m
  43. 0043specialize mod_eq_mul (x * x)
  44. 0044specialize mod_eq_mul (r * r)
  45. 0045specialize mod_eq_mul a
  46. 0046specialize mod_eq_mul a
  47. 0047apply mod_eq_mul
  48. 0048exact hsquare
  49. 0049exact hbase
  50. 0050have htotal : exists ff_left_binary_execution_odd_total ff_right_binary_execution_odd_total. ((x * x) * a) + m * ff_left_binary_execution_odd_total = (s) + m * ff_right_binary_execution_odd_total
  51. 0051specialize mod_eq_trans m
  52. 0052specialize mod_eq_trans ((x * x) * a)
  53. 0053specialize mod_eq_trans ((r * r) * a)
  54. 0054specialize mod_eq_trans s
  55. 0055apply mod_eq_trans
  56. 0056exact hproduct
  57. 0057exact hresidue_right
  58. 0058exists x1
  59. 0059split
  60. 0060exact hpower_witness
  61. 0061split
  62. 0062exact hresidue_left
  63. 0063rewrite hodd
  64. 0064exact htotal