BE000C

binary_modular_execution_exists

Every guarded valid coded binary digit prefix has a genuine witnessed modular execution and decoded terminal 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)

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) · 1

Actual proof prerequisites

binary_execution_prefix_existsbeta_at_exists · checked external prerequisite
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)))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

30 script commands · 8 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.

Named ingredients (1)
binary execution prefix exists

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

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

  1. L8
    have htrace : ∃ u. ∃ v. BinaryExecutionTrace(b,c,a,m,l,u,v)Definitions: BinaryExecutionTraceOriginal native command in the exact edition
  2. L9
    specialize binary_execution_prefix_exists b
  3. L10
    specialize binary_execution_prefix_exists c
  4. L11
    specialize binary_execution_prefix_exists a
  5. L12
    specialize binary_execution_prefix_exists m
  6. L13
    specialize binary_execution_prefix_exists l
  7. L14
    apply binary_execution_prefix_exists
  8. L15
    exact hmodulus
  9. L16
    exact hdigits
03Separate the logical casesL17–18

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

  1. L17
    cases htrace
  2. L18
    cases htrace_witness
04Establish hterminalL19–23

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

  1. L19
    have hterminal : exists r. (((exists ff_h_be_execution_terminal. ff_h_be_execution_terminal + S (r) = S ((S (l)) * x1)) /\ exists ff_q_be_execution_terminal. x = ff_q_be_execution_terminal * S ((S (l)) * x1) + (r)))
  2. L20
    specialize beta_at_exists x
  3. L21
    specialize beta_at_exists x1
  4. L22
    specialize beta_at_exists l
  5. L23
    exact beta_at_exists
05Separate the logical casesL24–24

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

  1. L24
    cases hterminal
06Construct an explicit witnessL25–27

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

  1. L25
    exists x2
  2. L26
    exists x
  3. L27
    exists x1
07Separate the logical casesL28–28

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

  1. L28
    split
08Use earlier factsL29–30

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

  1. L29
    exact htrace_witness_witness
  2. L30
    exact hterminal_witness

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro m
  5. 0005intro l
  6. 0006intro hmodulus
  7. 0007intro hdigits
  8. 0008have 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)))))))))))
  9. 0009specialize binary_execution_prefix_exists b
  10. 0010specialize binary_execution_prefix_exists c
  11. 0011specialize binary_execution_prefix_exists a
  12. 0012specialize binary_execution_prefix_exists m
  13. 0013specialize binary_execution_prefix_exists l
  14. 0014apply binary_execution_prefix_exists
  15. 0015exact hmodulus
  16. 0016exact hdigits
  17. 0017cases htrace
  18. 0018cases htrace_witness
  19. 0019have hterminal : exists r. (((exists ff_h_be_execution_terminal. ff_h_be_execution_terminal + S (r) = S ((S (l)) * x1)) /\ exists ff_q_be_execution_terminal. x = ff_q_be_execution_terminal * S ((S (l)) * x1) + (r)))
  20. 0020specialize beta_at_exists x
  21. 0021specialize beta_at_exists x1
  22. 0022specialize beta_at_exists l
  23. 0023exact beta_at_exists
  24. 0024cases hterminal
  25. 0025exists x2
  26. 0026exists x
  27. 0027exists x1
  28. 0028split
  29. 0029exact htrace_witness_witness
  30. 0030exact hterminal_witness