BE0013

binary_modular_execution_result_exists_unique

Every supplied valid beta-coded binary prefix has exactly one genuine guarded square-and-multiply execution result.

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

∀ b. ∀ c. ∀ a. ∀ m. ∀ l. BinaryModulus(m) → BinaryDigitPrefix(b,c,l) → ∃ x. BinaryModularExecution(b,c,a,m,l,x) ∧ (∀ y. BinaryModularExecution(b,c,a,m,l,y) → x = y)

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

Definition DAG

BinaryModulus(m) · 1BinaryDigitPrefix(d,s,n) · 1BinaryModularExecution(d,s,a,m,n,r) · 2

Actual proof prerequisites

binary_modular_execution_existsbinary_modular_execution_result_functional
Original expanded first-order statement 
forall b c a m l. (exists ff_modulus_gap_binary_execution_guard. ff_modulus_gap_binary_execution_guard + S 1 = m) -> (forall ff_index_be_prefix ff_digit_be_prefix. (exists ff_lt_be_prefix_bound. ff_lt_be_prefix_bound + S ff_index_be_prefix = l) -> (((exists ff_h_be_prefix_digit. ff_h_be_prefix_digit + S (ff_digit_be_prefix) = S ((S (ff_index_be_prefix)) * c)) /\ exists ff_q_be_prefix_digit. b = ff_q_be_prefix_digit * S ((S (ff_index_be_prefix)) * c) + (ff_digit_be_prefix))) -> (ff_digit_be_prefix = 0 \/ ff_digit_be_prefix = 1)) -> exists r. ((exists ff_trace_code_be_execution ff_trace_scale_be_execution. ((((((exists ff_h_be_execution_trace_start. ff_h_be_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_start. ff_trace_code_be_execution = ff_q_be_execution_trace_start * S ((S (0)) * ff_trace_scale_be_execution) + (1))) /\ forall ff_index_be_execution_trace. (exists ff_lt_be_execution_trace_bound. ff_lt_be_execution_trace_bound + S ff_index_be_execution_trace = l) -> exists ff_digit_be_execution_trace ff_previous_be_execution_trace ff_current_be_execution_trace. ((((exists ff_h_be_execution_trace_source. ff_h_be_execution_trace_source + S (ff_digit_be_execution_trace) = S ((S (ff_index_be_execution_trace)) * c)) /\ exists ff_q_be_execution_trace_source. b = ff_q_be_execution_trace_source * S ((S (ff_index_be_execution_trace)) * c) + (ff_digit_be_execution_trace))) /\ ((((exists ff_h_be_execution_trace_before. ff_h_be_execution_trace_before + S (ff_previous_be_execution_trace) = S ((S (ff_index_be_execution_trace)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_before. ff_trace_code_be_execution = ff_q_be_execution_trace_before * S ((S (ff_index_be_execution_trace)) * ff_trace_scale_be_execution) + (ff_previous_be_execution_trace))) /\ ((((exists ff_h_be_execution_trace_after. ff_h_be_execution_trace_after + S (ff_current_be_execution_trace) = S ((S (S ff_index_be_execution_trace)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_after. ff_trace_code_be_execution = ff_q_be_execution_trace_after * S ((S (S ff_index_be_execution_trace)) * ff_trace_scale_be_execution) + (ff_current_be_execution_trace))) /\ ((((ff_digit_be_execution_trace = 0) /\ (((exists ff_gap_binary_be_execution_trace_transition_square. ff_gap_binary_be_execution_trace_transition_square + S (ff_current_be_execution_trace) = m) /\ (exists ff_left_binary_be_execution_trace_transition_square_congruence ff_right_binary_be_execution_trace_transition_square_congruence. (ff_previous_be_execution_trace * ff_previous_be_execution_trace) + m * ff_left_binary_be_execution_trace_transition_square_congruence = (ff_current_be_execution_trace) + m * ff_right_binary_be_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_execution_trace = 1) /\ (((exists ff_gap_binary_be_execution_trace_transition_multiply. ff_gap_binary_be_execution_trace_transition_multiply + S (ff_current_be_execution_trace) = m) /\ (exists ff_left_binary_be_execution_trace_transition_multiply_congruence ff_right_binary_be_execution_trace_transition_multiply_congruence. ((ff_previous_be_execution_trace * ff_previous_be_execution_trace) * a) + m * ff_left_binary_be_execution_trace_transition_multiply_congruence = (ff_current_be_execution_trace) + m * ff_right_binary_be_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_execution_terminal. ff_h_be_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_terminal. ff_trace_code_be_execution = ff_q_be_execution_terminal * S ((S (l)) * ff_trace_scale_be_execution) + (r))))) /\ forall s. (exists ff_trace_code_be_other_execution ff_trace_scale_be_other_execution. ((((((exists ff_h_be_other_execution_trace_start. ff_h_be_other_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_trace_start. ff_trace_code_be_other_execution = ff_q_be_other_execution_trace_start * S ((S (0)) * ff_trace_scale_be_other_execution) + (1))) /\ forall ff_index_be_other_execution_trace. (exists ff_lt_be_other_execution_trace_bound. ff_lt_be_other_execution_trace_bound + S ff_index_be_other_execution_trace = l) -> exists ff_digit_be_other_execution_trace ff_previous_be_other_execution_trace ff_current_be_other_execution_trace. ((((exists ff_h_be_other_execution_trace_source. ff_h_be_other_execution_trace_source + S (ff_digit_be_other_execution_trace) = S ((S (ff_index_be_other_execution_trace)) * c)) /\ exists ff_q_be_other_execution_trace_source. b = ff_q_be_other_execution_trace_source * S ((S (ff_index_be_other_execution_trace)) * c) + (ff_digit_be_other_execution_trace))) /\ ((((exists ff_h_be_other_execution_trace_before. ff_h_be_other_execution_trace_before + S (ff_previous_be_other_execution_trace) = S ((S (ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_trace_before. ff_trace_code_be_other_execution = ff_q_be_other_execution_trace_before * S ((S (ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution) + (ff_previous_be_other_execution_trace))) /\ ((((exists ff_h_be_other_execution_trace_after. ff_h_be_other_execution_trace_after + S (ff_current_be_other_execution_trace) = S ((S (S ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_trace_after. ff_trace_code_be_other_execution = ff_q_be_other_execution_trace_after * S ((S (S ff_index_be_other_execution_trace)) * ff_trace_scale_be_other_execution) + (ff_current_be_other_execution_trace))) /\ ((((ff_digit_be_other_execution_trace = 0) /\ (((exists ff_gap_binary_be_other_execution_trace_transition_square. ff_gap_binary_be_other_execution_trace_transition_square + S (ff_current_be_other_execution_trace) = m) /\ (exists ff_left_binary_be_other_execution_trace_transition_square_congruence ff_right_binary_be_other_execution_trace_transition_square_congruence. (ff_previous_be_other_execution_trace * ff_previous_be_other_execution_trace) + m * ff_left_binary_be_other_execution_trace_transition_square_congruence = (ff_current_be_other_execution_trace) + m * ff_right_binary_be_other_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_other_execution_trace = 1) /\ (((exists ff_gap_binary_be_other_execution_trace_transition_multiply. ff_gap_binary_be_other_execution_trace_transition_multiply + S (ff_current_be_other_execution_trace) = m) /\ (exists ff_left_binary_be_other_execution_trace_transition_multiply_congruence ff_right_binary_be_other_execution_trace_transition_multiply_congruence. ((ff_previous_be_other_execution_trace * ff_previous_be_other_execution_trace) * a) + m * ff_left_binary_be_other_execution_trace_transition_multiply_congruence = (ff_current_be_other_execution_trace) + m * ff_right_binary_be_other_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_other_execution_terminal. ff_h_be_other_execution_terminal + S (s) = S ((S (l)) * ff_trace_scale_be_other_execution)) /\ exists ff_q_be_other_execution_terminal. ff_trace_code_be_other_execution = ff_q_be_other_execution_terminal * S ((S (l)) * ff_trace_scale_be_other_execution) + (s))))) -> r = s)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

33 script commands · 9 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 modular execution existsbinary modular execution result functional

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

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro m
  5. L5
    intro l
  6. L6
    intro hmodulus
  7. L7
    intro hdigits
02Establish hrunL8–16

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

  1. L8
    have hrun : ∃ r. BinaryModularExecution(b,c,a,m,l,r)Definitions: BinaryModularExecutionOriginal native command in the exact edition
  2. L9
    specialize binary_modular_execution_exists b
  3. L10
    specialize binary_modular_execution_exists c
  4. L11
    specialize binary_modular_execution_exists a
  5. L12
    specialize binary_modular_execution_exists m
  6. L13
    specialize binary_modular_execution_exists l
  7. L14
    apply binary_modular_execution_exists
  8. L15
    exact hmodulus
  9. L16
    exact hdigits
03Separate the logical casesL17–17

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

  1. L17
    cases hrun
04Construct an explicit witnessL18–18

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

  1. L18
    exists x
05Separate the logical casesL19–19

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

  1. L19
    split
06Use earlier factsL20–20

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

  1. L20
    exact hrun_witness
07Fix variables and assumptionsL21–22

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

  1. L21
    intro s
  2. L22
    intro hother
08Use earlier factsL23–32

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

  1. L23
    specialize binary_modular_execution_result_functional b
  2. L24
    specialize binary_modular_execution_result_functional c
  3. L25
    specialize binary_modular_execution_result_functional a
  4. L26
    specialize binary_modular_execution_result_functional m
  5. L27
    specialize binary_modular_execution_result_functional l
  6. L28
    specialize binary_modular_execution_result_functional x
  7. L29
    specialize binary_modular_execution_result_functional s
  8. L30
    apply binary_modular_execution_result_functional
  9. L31
    exact hmodulus
  10. L32
    exact hrun_witness
09Use earlier factsL33–33

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

  1. L33
    exact hother

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005intro l
  6. 0006intro hmodulus
  7. 0007intro hdigits
  8. 0008have hrun : exists r. (exists ff_trace_code_be_execution ff_trace_scale_be_execution. ((((((exists ff_h_be_execution_trace_start. ff_h_be_execution_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_start. ff_trace_code_be_execution = ff_q_be_execution_trace_start * S ((S (0)) * ff_trace_scale_be_execution) + (1))) /\ forall ff_index_be_execution_trace. (exists ff_lt_be_execution_trace_bound. ff_lt_be_execution_trace_bound + S ff_index_be_execution_trace = l) -> exists ff_digit_be_execution_trace ff_previous_be_execution_trace ff_current_be_execution_trace. ((((exists ff_h_be_execution_trace_source. ff_h_be_execution_trace_source + S (ff_digit_be_execution_trace) = S ((S (ff_index_be_execution_trace)) * c)) /\ exists ff_q_be_execution_trace_source. b = ff_q_be_execution_trace_source * S ((S (ff_index_be_execution_trace)) * c) + (ff_digit_be_execution_trace))) /\ ((((exists ff_h_be_execution_trace_before. ff_h_be_execution_trace_before + S (ff_previous_be_execution_trace) = S ((S (ff_index_be_execution_trace)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_before. ff_trace_code_be_execution = ff_q_be_execution_trace_before * S ((S (ff_index_be_execution_trace)) * ff_trace_scale_be_execution) + (ff_previous_be_execution_trace))) /\ ((((exists ff_h_be_execution_trace_after. ff_h_be_execution_trace_after + S (ff_current_be_execution_trace) = S ((S (S ff_index_be_execution_trace)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_trace_after. ff_trace_code_be_execution = ff_q_be_execution_trace_after * S ((S (S ff_index_be_execution_trace)) * ff_trace_scale_be_execution) + (ff_current_be_execution_trace))) /\ ((((ff_digit_be_execution_trace = 0) /\ (((exists ff_gap_binary_be_execution_trace_transition_square. ff_gap_binary_be_execution_trace_transition_square + S (ff_current_be_execution_trace) = m) /\ (exists ff_left_binary_be_execution_trace_transition_square_congruence ff_right_binary_be_execution_trace_transition_square_congruence. (ff_previous_be_execution_trace * ff_previous_be_execution_trace) + m * ff_left_binary_be_execution_trace_transition_square_congruence = (ff_current_be_execution_trace) + m * ff_right_binary_be_execution_trace_transition_square_congruence)))) \/ ((ff_digit_be_execution_trace = 1) /\ (((exists ff_gap_binary_be_execution_trace_transition_multiply. ff_gap_binary_be_execution_trace_transition_multiply + S (ff_current_be_execution_trace) = m) /\ (exists ff_left_binary_be_execution_trace_transition_multiply_congruence ff_right_binary_be_execution_trace_transition_multiply_congruence. ((ff_previous_be_execution_trace * ff_previous_be_execution_trace) * a) + m * ff_left_binary_be_execution_trace_transition_multiply_congruence = (ff_current_be_execution_trace) + m * ff_right_binary_be_execution_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_execution_terminal. ff_h_be_execution_terminal + S (r) = S ((S (l)) * ff_trace_scale_be_execution)) /\ exists ff_q_be_execution_terminal. ff_trace_code_be_execution = ff_q_be_execution_terminal * S ((S (l)) * ff_trace_scale_be_execution) + (r)))))
  9. 0009specialize binary_modular_execution_exists b
  10. 0010specialize binary_modular_execution_exists c
  11. 0011specialize binary_modular_execution_exists a
  12. 0012specialize binary_modular_execution_exists m
  13. 0013specialize binary_modular_execution_exists l
  14. 0014apply binary_modular_execution_exists
  15. 0015exact hmodulus
  16. 0016exact hdigits
  17. 0017cases hrun
  18. 0018exists x
  19. 0019split
  20. 0020exact hrun_witness
  21. 0021intro s
  22. 0022intro hother
  23. 0023specialize binary_modular_execution_result_functional b
  24. 0024specialize binary_modular_execution_result_functional c
  25. 0025specialize binary_modular_execution_result_functional a
  26. 0026specialize binary_modular_execution_result_functional m
  27. 0027specialize binary_modular_execution_result_functional l
  28. 0028specialize binary_modular_execution_result_functional x
  29. 0029specialize binary_modular_execution_result_functional s
  30. 0030apply binary_modular_execution_result_functional
  31. 0031exact hmodulus
  32. 0032exact hrun_witness
  33. 0033exact hother