BE000E

binary_modular_execution_successor_decompose

Every nonempty actual binary execution decomposes into its exact valid predecessor and final modular transition.

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. ∀ r. BinaryModularExecution(b,c,a,m,S l,r) → ∃ x. ∃ y. Beta(b,c,l,x) ∧ (BinaryModularExecution(b,c,a,m,l,y) ∧ BinaryModularStep(m,y,a,x,r))

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

Definition DAG

Beta(b,c,i,x) · 1BinaryModularStep(m,u,a,b,r) · 1BinaryModularExecution(d,s,a,m,n,r) · 2

Actual proof prerequisites

le_refl · checked external prerequisitele_succ · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall b c a m l r. (exists ff_trace_code_be_successor ff_trace_scale_be_successor. ((((((exists ff_h_be_successor_trace_start. ff_h_be_successor_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_successor)) /\ exists ff_q_be_successor_trace_start. ff_trace_code_be_successor = ff_q_be_successor_trace_start * S ((S (0)) * ff_trace_scale_be_successor) + (1))) /\ forall ff_index_be_successor_trace. (exists ff_lt_be_successor_trace_bound. ff_lt_be_successor_trace_bound + S ff_index_be_successor_trace = S l) -> exists ff_digit_be_successor_trace ff_previous_be_successor_trace ff_current_be_successor_trace. ((((exists ff_h_be_successor_trace_source. ff_h_be_successor_trace_source + S (ff_digit_be_successor_trace) = S ((S (ff_index_be_successor_trace)) * c)) /\ exists ff_q_be_successor_trace_source. b = ff_q_be_successor_trace_source * S ((S (ff_index_be_successor_trace)) * c) + (ff_digit_be_successor_trace))) /\ ((((exists ff_h_be_successor_trace_before. ff_h_be_successor_trace_before + S (ff_previous_be_successor_trace) = S ((S (ff_index_be_successor_trace)) * ff_trace_scale_be_successor)) /\ exists ff_q_be_successor_trace_before. ff_trace_code_be_successor = ff_q_be_successor_trace_before * S ((S (ff_index_be_successor_trace)) * ff_trace_scale_be_successor) + (ff_previous_be_successor_trace))) /\ ((((exists ff_h_be_successor_trace_after. ff_h_be_successor_trace_after + S (ff_current_be_successor_trace) = S ((S (S ff_index_be_successor_trace)) * ff_trace_scale_be_successor)) /\ exists ff_q_be_successor_trace_after. ff_trace_code_be_successor = ff_q_be_successor_trace_after * S ((S (S ff_index_be_successor_trace)) * ff_trace_scale_be_successor) + (ff_current_be_successor_trace))) /\ ((((ff_digit_be_successor_trace = 0) /\ (((exists ff_gap_binary_be_successor_trace_transition_square. ff_gap_binary_be_successor_trace_transition_square + S (ff_current_be_successor_trace) = m) /\ (exists ff_left_binary_be_successor_trace_transition_square_congruence ff_right_binary_be_successor_trace_transition_square_congruence. (ff_previous_be_successor_trace * ff_previous_be_successor_trace) + m * ff_left_binary_be_successor_trace_transition_square_congruence = (ff_current_be_successor_trace) + m * ff_right_binary_be_successor_trace_transition_square_congruence)))) \/ ((ff_digit_be_successor_trace = 1) /\ (((exists ff_gap_binary_be_successor_trace_transition_multiply. ff_gap_binary_be_successor_trace_transition_multiply + S (ff_current_be_successor_trace) = m) /\ (exists ff_left_binary_be_successor_trace_transition_multiply_congruence ff_right_binary_be_successor_trace_transition_multiply_congruence. ((ff_previous_be_successor_trace * ff_previous_be_successor_trace) * a) + m * ff_left_binary_be_successor_trace_transition_multiply_congruence = (ff_current_be_successor_trace) + m * ff_right_binary_be_successor_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_successor_terminal. ff_h_be_successor_terminal + S (r) = S ((S (S l)) * ff_trace_scale_be_successor)) /\ exists ff_q_be_successor_terminal. ff_trace_code_be_successor = ff_q_be_successor_terminal * S ((S (S l)) * ff_trace_scale_be_successor) + (r))))) -> exists d s. ((((exists ff_h_be_successor_digit. ff_h_be_successor_digit + S (d) = S ((S (l)) * c)) /\ exists ff_q_be_successor_digit. b = ff_q_be_successor_digit * S ((S (l)) * c) + (d))) /\ ((exists ff_trace_code_be_prefix_result ff_trace_scale_be_prefix_result. ((((((exists ff_h_be_prefix_result_trace_start. ff_h_be_prefix_result_trace_start + S (1) = S ((S (0)) * ff_trace_scale_be_prefix_result)) /\ exists ff_q_be_prefix_result_trace_start. ff_trace_code_be_prefix_result = ff_q_be_prefix_result_trace_start * S ((S (0)) * ff_trace_scale_be_prefix_result) + (1))) /\ forall ff_index_be_prefix_result_trace. (exists ff_lt_be_prefix_result_trace_bound. ff_lt_be_prefix_result_trace_bound + S ff_index_be_prefix_result_trace = l) -> exists ff_digit_be_prefix_result_trace ff_previous_be_prefix_result_trace ff_current_be_prefix_result_trace. ((((exists ff_h_be_prefix_result_trace_source. ff_h_be_prefix_result_trace_source + S (ff_digit_be_prefix_result_trace) = S ((S (ff_index_be_prefix_result_trace)) * c)) /\ exists ff_q_be_prefix_result_trace_source. b = ff_q_be_prefix_result_trace_source * S ((S (ff_index_be_prefix_result_trace)) * c) + (ff_digit_be_prefix_result_trace))) /\ ((((exists ff_h_be_prefix_result_trace_before. ff_h_be_prefix_result_trace_before + S (ff_previous_be_prefix_result_trace) = S ((S (ff_index_be_prefix_result_trace)) * ff_trace_scale_be_prefix_result)) /\ exists ff_q_be_prefix_result_trace_before. ff_trace_code_be_prefix_result = ff_q_be_prefix_result_trace_before * S ((S (ff_index_be_prefix_result_trace)) * ff_trace_scale_be_prefix_result) + (ff_previous_be_prefix_result_trace))) /\ ((((exists ff_h_be_prefix_result_trace_after. ff_h_be_prefix_result_trace_after + S (ff_current_be_prefix_result_trace) = S ((S (S ff_index_be_prefix_result_trace)) * ff_trace_scale_be_prefix_result)) /\ exists ff_q_be_prefix_result_trace_after. ff_trace_code_be_prefix_result = ff_q_be_prefix_result_trace_after * S ((S (S ff_index_be_prefix_result_trace)) * ff_trace_scale_be_prefix_result) + (ff_current_be_prefix_result_trace))) /\ ((((ff_digit_be_prefix_result_trace = 0) /\ (((exists ff_gap_binary_be_prefix_result_trace_transition_square. ff_gap_binary_be_prefix_result_trace_transition_square + S (ff_current_be_prefix_result_trace) = m) /\ (exists ff_left_binary_be_prefix_result_trace_transition_square_congruence ff_right_binary_be_prefix_result_trace_transition_square_congruence. (ff_previous_be_prefix_result_trace * ff_previous_be_prefix_result_trace) + m * ff_left_binary_be_prefix_result_trace_transition_square_congruence = (ff_current_be_prefix_result_trace) + m * ff_right_binary_be_prefix_result_trace_transition_square_congruence)))) \/ ((ff_digit_be_prefix_result_trace = 1) /\ (((exists ff_gap_binary_be_prefix_result_trace_transition_multiply. ff_gap_binary_be_prefix_result_trace_transition_multiply + S (ff_current_be_prefix_result_trace) = m) /\ (exists ff_left_binary_be_prefix_result_trace_transition_multiply_congruence ff_right_binary_be_prefix_result_trace_transition_multiply_congruence. ((ff_previous_be_prefix_result_trace * ff_previous_be_prefix_result_trace) * a) + m * ff_left_binary_be_prefix_result_trace_transition_multiply_congruence = (ff_current_be_prefix_result_trace) + m * ff_right_binary_be_prefix_result_trace_transition_multiply_congruence))))))))))) /\ (((exists ff_h_be_prefix_result_terminal. ff_h_be_prefix_result_terminal + S (s) = S ((S (l)) * ff_trace_scale_be_prefix_result)) /\ exists ff_q_be_prefix_result_terminal. ff_trace_code_be_prefix_result = ff_q_be_prefix_result_terminal * S ((S (l)) * ff_trace_scale_be_prefix_result) + (s))))) /\ ((((d = 0) /\ (((exists ff_gap_binary_successor_step_square. ff_gap_binary_successor_step_square + S (r) = m) /\ (exists ff_left_binary_successor_step_square_congruence ff_right_binary_successor_step_square_congruence. (s * s) + m * ff_left_binary_successor_step_square_congruence = (r) + m * ff_right_binary_successor_step_square_congruence)))) \/ ((d = 1) /\ (((exists ff_gap_binary_successor_step_multiply. ff_gap_binary_successor_step_multiply + S (r) = m) /\ (exists ff_left_binary_successor_step_multiply_congruence ff_right_binary_successor_step_multiply_congruence. ((s * s) * a) + m * ff_left_binary_successor_step_multiply_congruence = (r) + m * ff_right_binary_successor_step_multiply_congruence))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

55 script commands · 16 reading checkpoints · 2 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–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 r
  7. L7
    intro hexecution
02Separate the logical casesL8–11

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

  1. L8
    cases hexecution
  2. L9
    cases hexecution_witness
  3. L10
    cases hexecution_witness_witness
  4. L11
    cases hexecution_witness_witness_left
03Establish hlastL12–16

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

  1. L12
    have hlast : ∃ d. ∃ s. ∃ t. Beta(b,c,l,d) ∧ (Beta(x,x1,l,s) ∧ (Beta(x,x1,S l,t) ∧ BinaryModularStep(m,s,a,d,t)))Definitions: BetaBinaryModularStepOriginal native command in the exact edition
  2. L13
    specialize hexecution_witness_witness_left_right l
  3. L14
    apply hexecution_witness_witness_left_right
  4. L15
    specialize le_refl (S l)
  5. L16
    exact le_refl
04Separate the logical casesL17–22

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

  1. L17
    cases hlast
  2. L18
    cases hlast_witness
  3. L19
    cases hlast_witness_witness
  4. L20
    cases hlast_witness_witness_witness
  5. L21
    cases hlast_witness_witness_witness_right
  6. L22
    cases hlast_witness_witness_witness_right_right
05Establish hterminalL23–31

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

  1. L23
    have hterminal : x4 = r
  2. L24
    specialize beta_at_unique x
  3. L25
    specialize beta_at_unique x1
  4. L26
    specialize beta_at_unique (S l)
  5. L27
    specialize beta_at_unique x4
  6. L28
    specialize beta_at_unique r
  7. L29
    apply beta_at_unique
  8. L30
    exact hlast_witness_witness_witness_right_right_left
  9. L31
    exact hexecution_witness_witness_right
06Construct an explicit witnessL32–33

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

  1. L32
    exists x2
  2. L33
    exists x3
07Separate the logical casesL34–34

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

  1. L34
    split
08Use earlier factsL35–35

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

  1. L35
    exact hlast_witness_witness_witness_left
09Separate the logical casesL36–36

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

  1. L36
    split
10Construct an explicit witnessL37–38

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

  1. L37
    exists x
  2. L38
    exists x1
11Separate the logical casesL39–40

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

  1. L39
    split
  2. L40
    split
12Use earlier factsL41–41

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

  1. L41
    exact hexecution_witness_witness_left_left
13Fix variables and assumptionsL42–43

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

  1. L42
    intro i
  2. L43
    intro hi
14Use earlier factsL44–50

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

  1. L44
    specialize hexecution_witness_witness_left_right i
  2. L45
    apply hexecution_witness_witness_left_right
  3. L46
    specialize le_succ (S i)
  4. L47
    specialize le_succ l
  5. L48
    apply le_succ
  6. L49
    exact hi
  7. L50
    exact hlast_witness_witness_witness_right_left
15Calculate and transport equalitiesL51–54

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

  1. L51
    rewrite <- hterminal
  2. L52
    rewrite <- hterminal
  3. L53
    rewrite <- hterminal
  4. L54
    rewrite <- hterminal
16Use earlier factsL55–55

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

  1. L55
    exact hlast_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005intro l
  6. 0006intro r
  7. 0007intro hexecution
  8. 0008cases hexecution
  9. 0009cases hexecution_witness
  10. 0010cases hexecution_witness_witness
  11. 0011cases hexecution_witness_witness_left
  12. 0012have hlast : exists d s t. ((((exists ff_h_be_successor_last_digit. ff_h_be_successor_last_digit + S (d) = S ((S (l)) * c)) /\ exists ff_q_be_successor_last_digit. b = ff_q_be_successor_last_digit * S ((S (l)) * c) + (d))) /\ ((((exists ff_h_be_successor_last_previous. ff_h_be_successor_last_previous + S (s) = S ((S (l)) * x1)) /\ exists ff_q_be_successor_last_previous. x = ff_q_be_successor_last_previous * S ((S (l)) * x1) + (s))) /\ ((((exists ff_h_be_successor_last_current. ff_h_be_successor_last_current + S (t) = S ((S (S l)) * x1)) /\ exists ff_q_be_successor_last_current. x = ff_q_be_successor_last_current * S ((S (S l)) * x1) + (t))) /\ ((((d = 0) /\ (((exists ff_gap_binary_successor_last_step_square. ff_gap_binary_successor_last_step_square + S (t) = m) /\ (exists ff_left_binary_successor_last_step_square_congruence ff_right_binary_successor_last_step_square_congruence. (s * s) + m * ff_left_binary_successor_last_step_square_congruence = (t) + m * ff_right_binary_successor_last_step_square_congruence)))) \/ ((d = 1) /\ (((exists ff_gap_binary_successor_last_step_multiply. ff_gap_binary_successor_last_step_multiply + S (t) = m) /\ (exists ff_left_binary_successor_last_step_multiply_congruence ff_right_binary_successor_last_step_multiply_congruence. ((s * s) * a) + m * ff_left_binary_successor_last_step_multiply_congruence = (t) + m * ff_right_binary_successor_last_step_multiply_congruence)))))))))
  13. 0013specialize hexecution_witness_witness_left_right l
  14. 0014apply hexecution_witness_witness_left_right
  15. 0015specialize le_refl (S l)
  16. 0016exact le_refl
  17. 0017cases hlast
  18. 0018cases hlast_witness
  19. 0019cases hlast_witness_witness
  20. 0020cases hlast_witness_witness_witness
  21. 0021cases hlast_witness_witness_witness_right
  22. 0022cases hlast_witness_witness_witness_right_right
  23. 0023have hterminal : x4 = r
  24. 0024specialize beta_at_unique x
  25. 0025specialize beta_at_unique x1
  26. 0026specialize beta_at_unique (S l)
  27. 0027specialize beta_at_unique x4
  28. 0028specialize beta_at_unique r
  29. 0029apply beta_at_unique
  30. 0030exact hlast_witness_witness_witness_right_right_left
  31. 0031exact hexecution_witness_witness_right
  32. 0032exists x2
  33. 0033exists x3
  34. 0034split
  35. 0035exact hlast_witness_witness_witness_left
  36. 0036split
  37. 0037exists x
  38. 0038exists x1
  39. 0039split
  40. 0040split
  41. 0041exact hexecution_witness_witness_left_left
  42. 0042intro i
  43. 0043intro hi
  44. 0044specialize hexecution_witness_witness_left_right i
  45. 0045apply hexecution_witness_witness_left_right
  46. 0046specialize le_succ (S i)
  47. 0047specialize le_succ l
  48. 0048apply le_succ
  49. 0049exact hi
  50. 0050exact hlast_witness_witness_witness_right_left
  51. 0051rewrite <- hterminal
  52. 0052rewrite <- hterminal
  53. 0053rewrite <- hterminal
  54. 0054rewrite <- hterminal
  55. 0055exact hlast_witness_witness_witness_right_right_right