BE000C

binary_modular_execution_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every guarded valid coded binary digit prefix has a genuine witnessed modular execution and decoded terminal result.

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.

Exact expanded first-order arithmetic 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)))))

Constructive proof overview

Generated structural guide

Every guarded valid coded binary digit prefix has a genuine witnessed modular execution and decoded terminal result.

The unchanged tactic script uses 2 declared prerequisites and contains 30 exact native proof lines.

Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

BE000B binary_execution_prefix_exists beta_at_exists Stable theorem; checked-use authorized

Direct dependents

BE0011 binary_modular_execution_horner_exists BE0013 binary_modular_execution_result_exists_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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: BinaryExecutionTrace
  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 exact 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