BE000B

binary_execution_prefix_exists

Natural induction constructs a complete genuine beta-coded square-and-multiply trace for every supplied valid finite binary digit prefix.

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. ∃ y. BinaryExecutionTrace(b,c,a,m,l,x,y)

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

Definition DAG

BinaryModulus(m) · 1BinaryDigitPrefix(d,s,n) · 1BinaryExecutionTrace(d,s,a,m,n,h,t) · 1

Actual proof prerequisites

binary_execution_initial_stateadd_eq_zero_right · checked external prerequisitesucc_ne_zero · checked external prerequisitebinary_digit_prefix_restrictbinary_digit_prefix_terminal_bitbinary_execution_prefix_extend
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 u v. (((((exists ff_h_be_trace_start. ff_h_be_trace_start + S (1) = S ((S (0)) * v)) /\ exists ff_q_be_trace_start. u = ff_q_be_trace_start * S ((S (0)) * v) + (1))) /\ forall ff_index_be_trace. (exists ff_lt_be_trace_bound. ff_lt_be_trace_bound + S ff_index_be_trace = l) -> exists ff_digit_be_trace ff_previous_be_trace ff_current_be_trace. ((((exists ff_h_be_trace_source. ff_h_be_trace_source + S (ff_digit_be_trace) = S ((S (ff_index_be_trace)) * c)) /\ exists ff_q_be_trace_source. b = ff_q_be_trace_source * S ((S (ff_index_be_trace)) * c) + (ff_digit_be_trace))) /\ ((((exists ff_h_be_trace_before. ff_h_be_trace_before + S (ff_previous_be_trace) = S ((S (ff_index_be_trace)) * v)) /\ exists ff_q_be_trace_before. u = ff_q_be_trace_before * S ((S (ff_index_be_trace)) * v) + (ff_previous_be_trace))) /\ ((((exists ff_h_be_trace_after. ff_h_be_trace_after + S (ff_current_be_trace) = S ((S (S ff_index_be_trace)) * v)) /\ exists ff_q_be_trace_after. u = ff_q_be_trace_after * S ((S (S ff_index_be_trace)) * v) + (ff_current_be_trace))) /\ ((((ff_digit_be_trace = 0) /\ (((exists ff_gap_binary_be_trace_transition_square. ff_gap_binary_be_trace_transition_square + S (ff_current_be_trace) = m) /\ (exists ff_left_binary_be_trace_transition_square_congruence ff_right_binary_be_trace_transition_square_congruence. (ff_previous_be_trace * ff_previous_be_trace) + m * ff_left_binary_be_trace_transition_square_congruence = (ff_current_be_trace) + m * ff_right_binary_be_trace_transition_square_congruence)))) \/ ((ff_digit_be_trace = 1) /\ (((exists ff_gap_binary_be_trace_transition_multiply. ff_gap_binary_be_trace_transition_multiply + S (ff_current_be_trace) = m) /\ (exists ff_left_binary_be_trace_transition_multiply_congruence ff_right_binary_be_trace_transition_multiply_congruence. ((ff_previous_be_trace * ff_previous_be_trace) * a) + m * ff_left_binary_be_trace_transition_multiply_congruence = (ff_current_be_trace) + m * ff_right_binary_be_trace_transition_multiply_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 · 16 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.

Named ingredients (3)
binary digit prefix restrictbinary digit prefix terminal bitbinary execution prefix extend

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

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
02Induction on lL5–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction l
  2. L6
    intro hmodulus
  3. L7
    intro hdigits
03Separate the logical casesL8–9

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

  1. L8
    cases binary_execution_initial_state
  2. L9
    cases binary_execution_initial_state_witness
04Construct an explicit witnessL10–11

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

  1. L10
    exists x
  2. L11
    exists x1
05Separate the logical casesL12–12

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

  1. L12
    split
06Use earlier factsL13–13

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

  1. L13
    exact binary_execution_initial_state_witness_witness
07Fix variables and assumptionsL14–15

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

  1. L14
    intro i
  2. L15
    intro hi
08Separate the logical casesL16–17

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

  1. L16
    exfalso
  2. L17
    cases hi
09Establish hzeroL18–27

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

  1. L18
    have hzero : S i = 0
  2. L19
    specialize add_eq_zero_right x2
  3. L20
    specialize add_eq_zero_right (S i)
  4. L21
    apply add_eq_zero_right
  5. L22
    exact hi_witness
  6. L23
    specialize succ_ne_zero i
  7. L24
    apply succ_ne_zero
  8. L25
    exact hzero
  9. L26
    intro hmodulus
  10. L27
    intro hdigits
10Establish hprefixL28–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary digit prefix restrict.

  1. L28
    have hprefix : (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))
  2. L29
    specialize binary_digit_prefix_restrict b
  3. L30
    specialize binary_digit_prefix_restrict c
  4. L31
    specialize binary_digit_prefix_restrict l
  5. L32
    apply binary_digit_prefix_restrict
  6. L33
    exact hdigits
11Establish htraceL34–37

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

  1. L34
    have htrace : ∃ u. ∃ v. BinaryExecutionTrace(b,c,a,m,l,u,v)Definitions: BinaryExecutionTraceOriginal native command in the exact edition
  2. L35
    apply IH
  3. L36
    exact hmodulus
  4. L37
    exact hprefix
12Separate the logical casesL38–39

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

  1. L38
    cases htrace
  2. L39
    cases htrace_witness
13Establish hlastL40–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary digit prefix terminal bit.

  1. L40
    have hlast : exists x. ((((exists ff_h_be_terminal_digit. ff_h_be_terminal_digit + S (x) = S ((S (l)) * c)) /\ exists ff_q_be_terminal_digit. b = ff_q_be_terminal_digit * S ((S (l)) * c) + (x))) /\ (x = 0 \/ x = 1))
  2. L41
    specialize binary_digit_prefix_terminal_bit b
  3. L42
    specialize binary_digit_prefix_terminal_bit c
  4. L43
    specialize binary_digit_prefix_terminal_bit l
  5. L44
    apply binary_digit_prefix_terminal_bit
  6. L45
    exact hdigits
14Separate the logical casesL46–47

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

  1. L46
    cases hlast
  2. L47
    cases hlast_witness
15Use earlier factsL48–57

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

  1. L48
    specialize binary_execution_prefix_extend b
  2. L49
    specialize binary_execution_prefix_extend c
  3. L50
    specialize binary_execution_prefix_extend a
  4. L51
    specialize binary_execution_prefix_extend m
  5. L52
    specialize binary_execution_prefix_extend l
  6. L53
    specialize binary_execution_prefix_extend x
  7. L54
    specialize binary_execution_prefix_extend x1
  8. L55
    specialize binary_execution_prefix_extend x2
  9. L56
    apply binary_execution_prefix_extend
  10. L57
    exact hmodulus
16Use earlier factsL58–60

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

  1. L58
    exact hlast_witness_right
  2. L59
    exact hlast_witness_left
  3. L60
    exact htrace_witness_witness

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005induction l
  6. 0006intro hmodulus
  7. 0007intro hdigits
  8. 0008cases binary_execution_initial_state
  9. 0009cases binary_execution_initial_state_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012split
  13. 0013exact binary_execution_initial_state_witness_witness
  14. 0014intro i
  15. 0015intro hi
  16. 0016exfalso
  17. 0017cases hi
  18. 0018have hzero : S i = 0
  19. 0019specialize add_eq_zero_right x2
  20. 0020specialize add_eq_zero_right (S i)
  21. 0021apply add_eq_zero_right
  22. 0022exact hi_witness
  23. 0023specialize succ_ne_zero i
  24. 0024apply succ_ne_zero
  25. 0025exact hzero
  26. 0026intro hmodulus
  27. 0027intro hdigits
  28. 0028have hprefix : (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))
  29. 0029specialize binary_digit_prefix_restrict b
  30. 0030specialize binary_digit_prefix_restrict c
  31. 0031specialize binary_digit_prefix_restrict l
  32. 0032apply binary_digit_prefix_restrict
  33. 0033exact hdigits
  34. 0034have htrace : exists u v. (((((exists ff_h_be_trace_start. ff_h_be_trace_start + S (1) = S ((S (0)) * v)) /\ exists ff_q_be_trace_start. u = ff_q_be_trace_start * S ((S (0)) * v) + (1))) /\ forall ff_index_be_trace. (exists ff_lt_be_trace_bound. ff_lt_be_trace_bound + S ff_index_be_trace = l) -> exists ff_digit_be_trace ff_previous_be_trace ff_current_be_trace. ((((exists ff_h_be_trace_source. ff_h_be_trace_source + S (ff_digit_be_trace) = S ((S (ff_index_be_trace)) * c)) /\ exists ff_q_be_trace_source. b = ff_q_be_trace_source * S ((S (ff_index_be_trace)) * c) + (ff_digit_be_trace))) /\ ((((exists ff_h_be_trace_before. ff_h_be_trace_before + S (ff_previous_be_trace) = S ((S (ff_index_be_trace)) * v)) /\ exists ff_q_be_trace_before. u = ff_q_be_trace_before * S ((S (ff_index_be_trace)) * v) + (ff_previous_be_trace))) /\ ((((exists ff_h_be_trace_after. ff_h_be_trace_after + S (ff_current_be_trace) = S ((S (S ff_index_be_trace)) * v)) /\ exists ff_q_be_trace_after. u = ff_q_be_trace_after * S ((S (S ff_index_be_trace)) * v) + (ff_current_be_trace))) /\ ((((ff_digit_be_trace = 0) /\ (((exists ff_gap_binary_be_trace_transition_square. ff_gap_binary_be_trace_transition_square + S (ff_current_be_trace) = m) /\ (exists ff_left_binary_be_trace_transition_square_congruence ff_right_binary_be_trace_transition_square_congruence. (ff_previous_be_trace * ff_previous_be_trace) + m * ff_left_binary_be_trace_transition_square_congruence = (ff_current_be_trace) + m * ff_right_binary_be_trace_transition_square_congruence)))) \/ ((ff_digit_be_trace = 1) /\ (((exists ff_gap_binary_be_trace_transition_multiply. ff_gap_binary_be_trace_transition_multiply + S (ff_current_be_trace) = m) /\ (exists ff_left_binary_be_trace_transition_multiply_congruence ff_right_binary_be_trace_transition_multiply_congruence. ((ff_previous_be_trace * ff_previous_be_trace) * a) + m * ff_left_binary_be_trace_transition_multiply_congruence = (ff_current_be_trace) + m * ff_right_binary_be_trace_transition_multiply_congruence)))))))))))
  35. 0035apply IH
  36. 0036exact hmodulus
  37. 0037exact hprefix
  38. 0038cases htrace
  39. 0039cases htrace_witness
  40. 0040have hlast : exists x. ((((exists ff_h_be_terminal_digit. ff_h_be_terminal_digit + S (x) = S ((S (l)) * c)) /\ exists ff_q_be_terminal_digit. b = ff_q_be_terminal_digit * S ((S (l)) * c) + (x))) /\ (x = 0 \/ x = 1))
  41. 0041specialize binary_digit_prefix_terminal_bit b
  42. 0042specialize binary_digit_prefix_terminal_bit c
  43. 0043specialize binary_digit_prefix_terminal_bit l
  44. 0044apply binary_digit_prefix_terminal_bit
  45. 0045exact hdigits
  46. 0046cases hlast
  47. 0047cases hlast_witness
  48. 0048specialize binary_execution_prefix_extend b
  49. 0049specialize binary_execution_prefix_extend c
  50. 0050specialize binary_execution_prefix_extend a
  51. 0051specialize binary_execution_prefix_extend m
  52. 0052specialize binary_execution_prefix_extend l
  53. 0053specialize binary_execution_prefix_extend x
  54. 0054specialize binary_execution_prefix_extend x1
  55. 0055specialize binary_execution_prefix_extend x2
  56. 0056apply binary_execution_prefix_extend
  57. 0057exact hmodulus
  58. 0058exact hlast_witness_right
  59. 0059exact hlast_witness_left
  60. 0060exact htrace_witness_witness