BE0007

binary_execution_even_power_invariant

One exact binary zero 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 = h + h → BinaryModularPower(a,h,m,r) → CanonicalModularResidue(m,r · r,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_doubled_power · checked external prerequisitebinary_modular_square_congruence · checked external prerequisitemod_eq_trans · checked external prerequisite
Original expanded first-order statement 
forall a h e m r s. e = 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_even. ff_gap_binary_execution_even + S (s) = m) /\ (exists ff_left_binary_execution_even_congruence ff_right_binary_execution_even_congruence. (r * r) + m * ff_left_binary_execution_even_congruence = (s) + m * ff_right_binary_execution_even_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 51 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

51 script commands · 18 reading checkpoints · 4 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 hsquareL19–25

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

  1. L19
    have hsquare : x1 = x * x
  2. L20
    specialize binary_exponent_doubled_power a
  3. L21
    specialize binary_exponent_doubled_power h
  4. L22
    specialize binary_exponent_doubled_power e
  5. L23
    specialize binary_exponent_doubled_power x
  6. L24
    specialize binary_exponent_doubled_power x1
  7. L25
    apply binary_exponent_doubled_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 hsquare_congruenceL31–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_congruence : exists ff_left_binary_execution_square ff_right_binary_execution_square. (x * x) + m * ff_left_binary_execution_square = (r * r) + m * ff_right_binary_execution_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 htotalL37–44

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

  1. L37
    have htotal : exists ff_left_binary_execution_square_total ff_right_binary_execution_square_total. (x * x) + m * ff_left_binary_execution_square_total = (s) + m * ff_right_binary_execution_square_total
  2. L38
    specialize mod_eq_trans m
  3. L39
    specialize mod_eq_trans (x * x)
  4. L40
    specialize mod_eq_trans (r * r)
  5. L41
    specialize mod_eq_trans s
  6. L42
    apply mod_eq_trans
  7. L43
    exact hsquare_congruence
  8. L44
    exact hresidue_right
12Construct an explicit witnessL45–45

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

  1. L45
    exists x1
13Separate the logical casesL46–46

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

  1. L46
    split
14Use earlier factsL47–47

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

  1. L47
    exact hpower_witness
15Separate the logical casesL48–48

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

  1. L48
    split
16Use earlier factsL49–49

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

  1. L49
    exact hresidue_left
17Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite hsquare
18Use earlier factsL51–51

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

  1. L51
    exact htotal

Library-wide reading audit

Original defined command ledger · 51 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_even_full ff_c_be_even_full. ((forall ff_i_be_even_full_repeat. (exists ff_lt_be_even_full_repeat_bound. ff_lt_be_even_full_repeat_bound + S ff_i_be_even_full_repeat = e) -> (((exists ff_h_be_even_full_repeat_decoded. ff_h_be_even_full_repeat_decoded + S (a) = S ((S (ff_i_be_even_full_repeat)) * ff_c_be_even_full)) /\ exists ff_q_be_even_full_repeat_decoded. ff_b_be_even_full = ff_q_be_even_full_repeat_decoded * S ((S (ff_i_be_even_full_repeat)) * ff_c_be_even_full) + (a)))) /\ (exists ff_u_be_even_full_product ff_v_be_even_full_product. ((((exists ff_h_be_even_full_product_start. ff_h_be_even_full_product_start + S (1) = S ((S (0)) * ff_v_be_even_full_product)) /\ exists ff_q_be_even_full_product_start. ff_u_be_even_full_product = ff_q_be_even_full_product_start * S ((S (0)) * ff_v_be_even_full_product) + (1))) /\ ((((exists ff_h_be_even_full_product_terminal. ff_h_be_even_full_product_terminal + S (y) = S ((S (e)) * ff_v_be_even_full_product)) /\ exists ff_q_be_even_full_product_terminal. ff_u_be_even_full_product = ff_q_be_even_full_product_terminal * S ((S (e)) * ff_v_be_even_full_product) + (y))) /\ forall ff_i_be_even_full_product. (exists ff_lt_be_even_full_product_bound. ff_lt_be_even_full_product_bound + S ff_i_be_even_full_product = e) -> exists ff_p_be_even_full_product ff_r_be_even_full_product ff_s_be_even_full_product. ((((exists ff_h_be_even_full_product_factor. ff_h_be_even_full_product_factor + S (ff_p_be_even_full_product) = S ((S (ff_i_be_even_full_product)) * ff_c_be_even_full)) /\ exists ff_q_be_even_full_product_factor. ff_b_be_even_full = ff_q_be_even_full_product_factor * S ((S (ff_i_be_even_full_product)) * ff_c_be_even_full) + (ff_p_be_even_full_product))) /\ ((((exists ff_h_be_even_full_product_partial. ff_h_be_even_full_product_partial + S (ff_r_be_even_full_product) = S ((S (ff_i_be_even_full_product)) * ff_v_be_even_full_product)) /\ exists ff_q_be_even_full_product_partial. ff_u_be_even_full_product = ff_q_be_even_full_product_partial * S ((S (ff_i_be_even_full_product)) * ff_v_be_even_full_product) + (ff_r_be_even_full_product))) /\ ((((exists ff_h_be_even_full_product_successor. ff_h_be_even_full_product_successor + S (ff_s_be_even_full_product) = S ((S (S ff_i_be_even_full_product)) * ff_v_be_even_full_product)) /\ exists ff_q_be_even_full_product_successor. ff_u_be_even_full_product = ff_q_be_even_full_product_successor * S ((S (S ff_i_be_even_full_product)) * ff_v_be_even_full_product) + (ff_s_be_even_full_product))) /\ ff_s_be_even_full_product = ff_r_be_even_full_product * ff_p_be_even_full_product))))))))
  15. 0015specialize pow_exists a
  16. 0016specialize pow_exists e
  17. 0017exact pow_exists
  18. 0018cases hpower
  19. 0019have hsquare : x1 = x * x
  20. 0020specialize binary_exponent_doubled_power a
  21. 0021specialize binary_exponent_doubled_power h
  22. 0022specialize binary_exponent_doubled_power e
  23. 0023specialize binary_exponent_doubled_power x
  24. 0024specialize binary_exponent_doubled_power x1
  25. 0025apply binary_exponent_doubled_power
  26. 0026split
  27. 0027exact he
  28. 0028split
  29. 0029exact hprevious_witness_left
  30. 0030exact hpower_witness
  31. 0031have hsquare_congruence : exists ff_left_binary_execution_square ff_right_binary_execution_square. (x * x) + m * ff_left_binary_execution_square = (r * r) + m * ff_right_binary_execution_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 htotal : exists ff_left_binary_execution_square_total ff_right_binary_execution_square_total. (x * x) + m * ff_left_binary_execution_square_total = (s) + m * ff_right_binary_execution_square_total
  38. 0038specialize mod_eq_trans m
  39. 0039specialize mod_eq_trans (x * x)
  40. 0040specialize mod_eq_trans (r * r)
  41. 0041specialize mod_eq_trans s
  42. 0042apply mod_eq_trans
  43. 0043exact hsquare_congruence
  44. 0044exact hresidue_right
  45. 0045exists x1
  46. 0046split
  47. 0047exact hpower_witness
  48. 0048split
  49. 0049exact hresidue_left
  50. 0050rewrite hsquare
  51. 0051exact htotal