BE000A

binary_execution_prefix_extend

Append one genuine beta-coded binary digit and canonical modular transition while preserving every previous execution state.

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. ∀ u. ∀ v. ∀ q. BinaryModulus(m) → q = 0 ∨ q = 1 → Beta(b,c,l,q) → BinaryExecutionTrace(b,c,a,m,l,u,v) → ∃ x. ∃ y. BinaryExecutionTrace(b,c,a,m,S l,x,y)

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

Definition DAG

Beta(b,c,i,x) · 1BinaryModulus(m) · 1BinaryExecutionTrace(d,s,a,m,n,h,t) · 2

Actual proof prerequisites

beta_at_exists · checked external prerequisitebinary_modular_step_exists · checked external prerequisitebeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisitezero_le · checked external prerequisitesucc_le_succ · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c a m l u v q. (exists ff_modulus_gap_binary_execution_guard. ff_modulus_gap_binary_execution_guard + S 1 = m) -> (q = 0 \/ q = 1) -> (((exists ff_h_be_extend_digit. ff_h_be_extend_digit + S (q) = S ((S (l)) * c)) /\ exists ff_q_be_extend_digit. b = ff_q_be_extend_digit * S ((S (l)) * c) + (q))) -> (((((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))))))))))) -> exists z e. (((((exists ff_h_be_extend_trace_start. ff_h_be_extend_trace_start + S (1) = S ((S (0)) * e)) /\ exists ff_q_be_extend_trace_start. z = ff_q_be_extend_trace_start * S ((S (0)) * e) + (1))) /\ forall ff_index_be_extend_trace. (exists ff_lt_be_extend_trace_bound. ff_lt_be_extend_trace_bound + S ff_index_be_extend_trace = S l) -> exists ff_digit_be_extend_trace ff_previous_be_extend_trace ff_current_be_extend_trace. ((((exists ff_h_be_extend_trace_source. ff_h_be_extend_trace_source + S (ff_digit_be_extend_trace) = S ((S (ff_index_be_extend_trace)) * c)) /\ exists ff_q_be_extend_trace_source. b = ff_q_be_extend_trace_source * S ((S (ff_index_be_extend_trace)) * c) + (ff_digit_be_extend_trace))) /\ ((((exists ff_h_be_extend_trace_before. ff_h_be_extend_trace_before + S (ff_previous_be_extend_trace) = S ((S (ff_index_be_extend_trace)) * e)) /\ exists ff_q_be_extend_trace_before. z = ff_q_be_extend_trace_before * S ((S (ff_index_be_extend_trace)) * e) + (ff_previous_be_extend_trace))) /\ ((((exists ff_h_be_extend_trace_after. ff_h_be_extend_trace_after + S (ff_current_be_extend_trace) = S ((S (S ff_index_be_extend_trace)) * e)) /\ exists ff_q_be_extend_trace_after. z = ff_q_be_extend_trace_after * S ((S (S ff_index_be_extend_trace)) * e) + (ff_current_be_extend_trace))) /\ ((((ff_digit_be_extend_trace = 0) /\ (((exists ff_gap_binary_be_extend_trace_transition_square. ff_gap_binary_be_extend_trace_transition_square + S (ff_current_be_extend_trace) = m) /\ (exists ff_left_binary_be_extend_trace_transition_square_congruence ff_right_binary_be_extend_trace_transition_square_congruence. (ff_previous_be_extend_trace * ff_previous_be_extend_trace) + m * ff_left_binary_be_extend_trace_transition_square_congruence = (ff_current_be_extend_trace) + m * ff_right_binary_be_extend_trace_transition_square_congruence)))) \/ ((ff_digit_be_extend_trace = 1) /\ (((exists ff_gap_binary_be_extend_trace_transition_multiply. ff_gap_binary_be_extend_trace_transition_multiply + S (ff_current_be_extend_trace) = m) /\ (exists ff_left_binary_be_extend_trace_transition_multiply_congruence ff_right_binary_be_extend_trace_transition_multiply_congruence. ((ff_previous_be_extend_trace * ff_previous_be_extend_trace) * a) + m * ff_left_binary_be_extend_trace_transition_multiply_congruence = (ff_current_be_extend_trace) + m * ff_right_binary_be_extend_trace_transition_multiply_congruence)))))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

109 script commands · 34 reading checkpoints · 5 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–10

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 u
  7. L7
    intro v
  8. L8
    intro q
  9. L9
    intro hmodulus
  10. L10
    intro hbit
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hdigit
  2. L12
    intro htrace
03Separate the logical casesL13–13

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

  1. L13
    cases htrace
04Establish hlastL14–18

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

  1. L14
    have hlast : exists r. (((exists ff_h_be_extend_last. ff_h_be_extend_last + S (r) = S ((S (l)) * v)) /\ exists ff_q_be_extend_last. u = ff_q_be_extend_last * S ((S (l)) * v) + (r)))
  2. L15
    specialize beta_at_exists u
  3. L16
    specialize beta_at_exists v
  4. L17
    specialize beta_at_exists l
  5. L18
    exact beta_at_exists
05Separate the logical casesL19–19

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

  1. L19
    cases hlast
06Establish hstepL20–27

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

  1. L20
    have hstep : ∃ s. BinaryModularStep(m,x,a,q,s)Definitions: BinaryModularStepOriginal native command in the exact edition
  2. L21
    specialize binary_modular_step_exists m
  3. L22
    specialize binary_modular_step_exists x
  4. L23
    specialize binary_modular_step_exists a
  5. L24
    specialize binary_modular_step_exists q
  6. L25
    apply binary_modular_step_exists
  7. L26
    exact hmodulus
  8. L27
    exact hbit
07Separate the logical casesL28–28

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

  1. L28
    cases hstep
08Establish hextL29–34

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

  1. L29
    have hext : ∃ z. ∃ e. Beta(z,e,S l,x1) ∧ (∀ x. ∀ y. Lt(x,S l) → Beta(u,v,x,y) → Beta(z,e,x,y))Definitions: BetaLtOriginal native command in the exact edition
  2. L30
    specialize beta_prefix_extend (S l)
  3. L31
    specialize beta_prefix_extend u
  4. L32
    specialize beta_prefix_extend v
  5. L33
    specialize beta_prefix_extend x1
  6. L34
    exact beta_prefix_extend
09Separate the logical casesL35–37

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

  1. L35
    cases hext
  2. L36
    cases hext_witness
  3. L37
    cases hext_witness_witness
10Construct an explicit witnessL38–39

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

  1. L38
    exists x2
  2. L39
    exists x3
11Separate the logical casesL40–40

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

  1. L40
    split
12Use earlier factsL41–49

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

  1. L41
    specialize hext_witness_witness_right 0
  2. L42
    specialize hext_witness_witness_right 1
  3. L43
    apply hext_witness_witness_right
  4. L44
    specialize succ_le_succ 0
  5. L45
    specialize succ_le_succ l
  6. L46
    apply succ_le_succ
  7. L47
    specialize zero_le l
  8. L48
    exact zero_le
  9. L49
    exact htrace_left
13Fix variables and assumptionsL50–51

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

  1. L50
    intro i
  2. L51
    intro hi
14Establish hsplitL52–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L52
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L53
    specialize finite_lt_succ_eq_or_lt l
  3. L54
    specialize finite_lt_succ_eq_or_lt i
  4. L55
    apply finite_lt_succ_eq_or_lt
  5. L56
    exact hi
15Separate the logical casesL57–57

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

  1. L57
    cases hsplit
16Construct an explicit witnessL58–60

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

  1. L58
    exists q
  2. L59
    exists x
  3. L60
    exists x1
17Separate the logical casesL61–61

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

  1. L61
    split
18Calculate and transport equalitiesL62–63

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

  1. L62
    rewrite hsplit_left
  2. L63
    rewrite hsplit_left
19Use earlier factsL64–64

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

  1. L64
    exact hdigit
20Separate the logical casesL65–65

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

  1. L65
    split
21Calculate and transport equalitiesL66–67

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

  1. L66
    rewrite hsplit_left
  2. L67
    rewrite hsplit_left
22Use earlier factsL68–73

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

  1. L68
    specialize hext_witness_witness_right l
  2. L69
    specialize hext_witness_witness_right x
  3. L70
    apply hext_witness_witness_right
  4. L71
    specialize le_refl (S l)
  5. L72
    exact le_refl
  6. L73
    exact hlast_witness
23Separate the logical casesL74–74

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

  1. L74
    split
24Calculate and transport equalitiesL75–76

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

  1. L75
    rewrite hsplit_left
  2. L76
    rewrite hsplit_left
25Use earlier factsL77–78

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

  1. L77
    exact hext_witness_witness_left
  2. L78
    exact hstep_witness
26Establish holdL79–82

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

  1. L79
    have hold : ∃ digit. ∃ previous. ∃ current. Beta(b,c,i,digit) ∧ (Beta(u,v,i,previous) ∧ (Beta(u,v,S i,current) ∧ BinaryModularStep(m,previous,a,digit,current)))Definitions: BetaBinaryModularStepOriginal native command in the exact edition
  2. L80
    specialize htrace_right i
  3. L81
    apply htrace_right
  4. L82
    exact hsplit_right
27Separate the logical casesL83–88

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

  1. L83
    cases hold
  2. L84
    cases hold_witness
  3. L85
    cases hold_witness_witness
  4. L86
    cases hold_witness_witness_witness
  5. L87
    cases hold_witness_witness_witness_right
  6. L88
    cases hold_witness_witness_witness_right_right
28Construct an explicit witnessL89–91

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

  1. L89
    exists x4
  2. L90
    exists x5
  3. L91
    exists x6
29Separate the logical casesL92–92

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

  1. L92
    split
30Use earlier factsL93–93

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

  1. L93
    exact hold_witness_witness_witness_left
31Separate the logical casesL94–94

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

  1. L94
    split
32Use earlier factsL95–99

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

  1. L95
    specialize hext_witness_witness_right i
  2. L96
    specialize hext_witness_witness_right x5
  3. L97
    apply hext_witness_witness_right
  4. L98
    exact hi
  5. L99
    exact hold_witness_witness_witness_right_left
33Separate the logical casesL100–100

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

  1. L100
    split
34Use earlier factsL101–109

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

  1. L101
    specialize hext_witness_witness_right (S i)
  2. L102
    specialize hext_witness_witness_right x6
  3. L103
    apply hext_witness_witness_right
  4. L104
    specialize succ_le_succ (S i)
  5. L105
    specialize succ_le_succ l
  6. L106
    apply succ_le_succ
  7. L107
    exact hsplit_right
  8. L108
    exact hold_witness_witness_witness_right_right_left
  9. L109
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 109 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005intro l
  6. 0006intro u
  7. 0007intro v
  8. 0008intro q
  9. 0009intro hmodulus
  10. 0010intro hbit
  11. 0011intro hdigit
  12. 0012intro htrace
  13. 0013cases htrace
  14. 0014have hlast : exists r. (((exists ff_h_be_extend_last. ff_h_be_extend_last + S (r) = S ((S (l)) * v)) /\ exists ff_q_be_extend_last. u = ff_q_be_extend_last * S ((S (l)) * v) + (r)))
  15. 0015specialize beta_at_exists u
  16. 0016specialize beta_at_exists v
  17. 0017specialize beta_at_exists l
  18. 0018exact beta_at_exists
  19. 0019cases hlast
  20. 0020have hstep : exists s. ((((q = 0) /\ (((exists ff_gap_binary_extend_step_square. ff_gap_binary_extend_step_square + S (s) = m) /\ (exists ff_left_binary_extend_step_square_congruence ff_right_binary_extend_step_square_congruence. (x * x) + m * ff_left_binary_extend_step_square_congruence = (s) + m * ff_right_binary_extend_step_square_congruence)))) \/ ((q = 1) /\ (((exists ff_gap_binary_extend_step_multiply. ff_gap_binary_extend_step_multiply + S (s) = m) /\ (exists ff_left_binary_extend_step_multiply_congruence ff_right_binary_extend_step_multiply_congruence. ((x * x) * a) + m * ff_left_binary_extend_step_multiply_congruence = (s) + m * ff_right_binary_extend_step_multiply_congruence))))))
  21. 0021specialize binary_modular_step_exists m
  22. 0022specialize binary_modular_step_exists x
  23. 0023specialize binary_modular_step_exists a
  24. 0024specialize binary_modular_step_exists q
  25. 0025apply binary_modular_step_exists
  26. 0026exact hmodulus
  27. 0027exact hbit
  28. 0028cases hstep
  29. 0029have hext : exists z e. ((((exists ff_h_be_extend_new_terminal. ff_h_be_extend_new_terminal + S (x1) = S ((S (S l)) * e)) /\ exists ff_q_be_extend_new_terminal. z = ff_q_be_extend_new_terminal * S ((S (S l)) * e) + (x1))) /\ forall i y. (exists gap. gap + S i = S l) -> (((exists ff_h_be_extend_old_entry. ff_h_be_extend_old_entry + S (y) = S ((S (i)) * v)) /\ exists ff_q_be_extend_old_entry. u = ff_q_be_extend_old_entry * S ((S (i)) * v) + (y))) -> (((exists ff_h_be_extend_new_entry. ff_h_be_extend_new_entry + S (y) = S ((S (i)) * e)) /\ exists ff_q_be_extend_new_entry. z = ff_q_be_extend_new_entry * S ((S (i)) * e) + (y))))
  30. 0030specialize beta_prefix_extend (S l)
  31. 0031specialize beta_prefix_extend u
  32. 0032specialize beta_prefix_extend v
  33. 0033specialize beta_prefix_extend x1
  34. 0034exact beta_prefix_extend
  35. 0035cases hext
  36. 0036cases hext_witness
  37. 0037cases hext_witness_witness
  38. 0038exists x2
  39. 0039exists x3
  40. 0040split
  41. 0041specialize hext_witness_witness_right 0
  42. 0042specialize hext_witness_witness_right 1
  43. 0043apply hext_witness_witness_right
  44. 0044specialize succ_le_succ 0
  45. 0045specialize succ_le_succ l
  46. 0046apply succ_le_succ
  47. 0047specialize zero_le l
  48. 0048exact zero_le
  49. 0049exact htrace_left
  50. 0050intro i
  51. 0051intro hi
  52. 0052have hsplit : i = l \/ exists gap. gap + S i = l
  53. 0053specialize finite_lt_succ_eq_or_lt l
  54. 0054specialize finite_lt_succ_eq_or_lt i
  55. 0055apply finite_lt_succ_eq_or_lt
  56. 0056exact hi
  57. 0057cases hsplit
  58. 0058exists q
  59. 0059exists x
  60. 0060exists x1
  61. 0061split
  62. 0062rewrite hsplit_left
  63. 0063rewrite hsplit_left
  64. 0064exact hdigit
  65. 0065split
  66. 0066rewrite hsplit_left
  67. 0067rewrite hsplit_left
  68. 0068specialize hext_witness_witness_right l
  69. 0069specialize hext_witness_witness_right x
  70. 0070apply hext_witness_witness_right
  71. 0071specialize le_refl (S l)
  72. 0072exact le_refl
  73. 0073exact hlast_witness
  74. 0074split
  75. 0075rewrite hsplit_left
  76. 0076rewrite hsplit_left
  77. 0077exact hext_witness_witness_left
  78. 0078exact hstep_witness
  79. 0079have hold : exists digit previous current. ((((exists ff_h_be_extend_hold_digit. ff_h_be_extend_hold_digit + S (digit) = S ((S (i)) * c)) /\ exists ff_q_be_extend_hold_digit. b = ff_q_be_extend_hold_digit * S ((S (i)) * c) + (digit))) /\ ((((exists ff_h_be_extend_hold_previous. ff_h_be_extend_hold_previous + S (previous) = S ((S (i)) * v)) /\ exists ff_q_be_extend_hold_previous. u = ff_q_be_extend_hold_previous * S ((S (i)) * v) + (previous))) /\ ((((exists ff_h_be_extend_hold_current. ff_h_be_extend_hold_current + S (current) = S ((S (S i)) * v)) /\ exists ff_q_be_extend_hold_current. u = ff_q_be_extend_hold_current * S ((S (S i)) * v) + (current))) /\ ((((digit = 0) /\ (((exists ff_gap_binary_extend_hold_step_square. ff_gap_binary_extend_hold_step_square + S (current) = m) /\ (exists ff_left_binary_extend_hold_step_square_congruence ff_right_binary_extend_hold_step_square_congruence. (previous * previous) + m * ff_left_binary_extend_hold_step_square_congruence = (current) + m * ff_right_binary_extend_hold_step_square_congruence)))) \/ ((digit = 1) /\ (((exists ff_gap_binary_extend_hold_step_multiply. ff_gap_binary_extend_hold_step_multiply + S (current) = m) /\ (exists ff_left_binary_extend_hold_step_multiply_congruence ff_right_binary_extend_hold_step_multiply_congruence. ((previous * previous) * a) + m * ff_left_binary_extend_hold_step_multiply_congruence = (current) + m * ff_right_binary_extend_hold_step_multiply_congruence)))))))))
  80. 0080specialize htrace_right i
  81. 0081apply htrace_right
  82. 0082exact hsplit_right
  83. 0083cases hold
  84. 0084cases hold_witness
  85. 0085cases hold_witness_witness
  86. 0086cases hold_witness_witness_witness
  87. 0087cases hold_witness_witness_witness_right
  88. 0088cases hold_witness_witness_witness_right_right
  89. 0089exists x4
  90. 0090exists x5
  91. 0091exists x6
  92. 0092split
  93. 0093exact hold_witness_witness_witness_left
  94. 0094split
  95. 0095specialize hext_witness_witness_right i
  96. 0096specialize hext_witness_witness_right x5
  97. 0097apply hext_witness_witness_right
  98. 0098exact hi
  99. 0099exact hold_witness_witness_witness_right_left
  100. 0100split
  101. 0101specialize hext_witness_witness_right (S i)
  102. 0102specialize hext_witness_witness_right x6
  103. 0103apply hext_witness_witness_right
  104. 0104specialize succ_le_succ (S i)
  105. 0105specialize succ_le_succ l
  106. 0106apply succ_le_succ
  107. 0107exact hsplit_right
  108. 0108exact hold_witness_witness_witness_right_right_left
  109. 0109exact hold_witness_witness_witness_right_right_right