EL0008

euclidean_log_budget_zero_divisor

A zero-divisor input has a genuine zero-step Euclidean history within every supplied budget.

Alpha v34 checked-use · first admitted v23 · 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.

The exact G101 milestone is fully proved, including the stronger checked bound k≤2·BitLen(b), a real beta-coded execution, and its actual terminal gcd. The independent T13 determinant/rank/integer-span substrate is now closed in the separate Alpha-v27 integer-linear-algebra branch. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ B. b = 0 → EuclideanBoundedTrace(a,b,B)

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

Definition DAG

EuclideanBoundedTrace(a,b,B) · 1

Actual proof prerequisites

euclidean_trace_exists_linear · checked external prerequisitele_zero · checked external prerequisite
Original expanded first-order statement 
forall a b B. b = 0 -> (exists elb_list_base elb_history_base elb_scale_base elb_steps_base. ((exists cf_gcd_elb_base_budget. ((((exists ff_h_cf_elb_base_budget_initial_state. ff_h_cf_elb_base_budget_initial_state + S (((cf_gcd_elb_base_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_base_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_base)) /\ exists ff_q_cf_elb_base_budget_initial_state. elb_history_base = ff_q_cf_elb_base_budget_initial_state * S ((S (0)) * elb_scale_base) + (((cf_gcd_elb_base_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_base_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_elb_base_budget_terminal_state. ff_h_cf_elb_base_budget_terminal_state + S (((a) + (((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base)))) * S ((a) + (((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base)))) + ((((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base))) + (((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base))))) = S ((S (elb_steps_base)) * elb_scale_base)) /\ exists ff_q_cf_elb_base_budget_terminal_state. elb_history_base = ff_q_cf_elb_base_budget_terminal_state * S ((S (elb_steps_base)) * elb_scale_base) + (((a) + (((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base)))) * S ((a) + (((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base)))) + ((((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base))) + (((b) + (elb_list_base)) * S ((b) + (elb_list_base)) + ((elb_list_base) + (elb_list_base))))))) /\ forall cf_index_elb_base_budget. (exists ff_lt_cf_elb_base_budget_index. ff_lt_cf_elb_base_budget_index + S cf_index_elb_base_budget = elb_steps_base) -> exists cf_old_a_elb_base_budget cf_old_b_elb_base_budget cf_tail_elb_base_budget cf_new_a_elb_base_budget cf_new_b_elb_base_budget cf_head_elb_base_budget cf_quotient_elb_base_budget. ((((exists ff_h_cf_elb_base_budget_previous_state. ff_h_cf_elb_base_budget_previous_state + S (((cf_old_a_elb_base_budget) + (((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget)))) * S ((cf_old_a_elb_base_budget) + (((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget)))) + ((((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget))) + (((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget))))) = S ((S (cf_index_elb_base_budget)) * elb_scale_base)) /\ exists ff_q_cf_elb_base_budget_previous_state. elb_history_base = ff_q_cf_elb_base_budget_previous_state * S ((S (cf_index_elb_base_budget)) * elb_scale_base) + (((cf_old_a_elb_base_budget) + (((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget)))) * S ((cf_old_a_elb_base_budget) + (((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget)))) + ((((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget))) + (((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) * S ((cf_old_b_elb_base_budget) + (cf_tail_elb_base_budget)) + ((cf_tail_elb_base_budget) + (cf_tail_elb_base_budget))))))) /\ ((((exists ff_h_cf_elb_base_budget_following_state. ff_h_cf_elb_base_budget_following_state + S (((cf_new_a_elb_base_budget) + (((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget)))) * S ((cf_new_a_elb_base_budget) + (((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget)))) + ((((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget))) + (((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget))))) = S ((S (S cf_index_elb_base_budget)) * elb_scale_base)) /\ exists ff_q_cf_elb_base_budget_following_state. elb_history_base = ff_q_cf_elb_base_budget_following_state * S ((S (S cf_index_elb_base_budget)) * elb_scale_base) + (((cf_new_a_elb_base_budget) + (((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget)))) * S ((cf_new_a_elb_base_budget) + (((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget)))) + ((((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget))) + (((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) * S ((cf_new_b_elb_base_budget) + (cf_head_elb_base_budget)) + ((cf_head_elb_base_budget) + (cf_head_elb_base_budget))))))) /\ (cf_new_b_elb_base_budget = cf_old_a_elb_base_budget /\ (cf_new_a_elb_base_budget = cf_new_b_elb_base_budget * cf_quotient_elb_base_budget + cf_old_b_elb_base_budget /\ ((exists ff_lt_cf_elb_base_budget_remainder. ff_lt_cf_elb_base_budget_remainder + S cf_old_b_elb_base_budget = cf_new_b_elb_base_budget) /\ (cf_head_elb_base_budget = S ((cf_quotient_elb_base_budget + cf_tail_elb_base_budget) * S (cf_quotient_elb_base_budget + cf_tail_elb_base_budget) + (cf_tail_elb_base_budget + cf_tail_elb_base_budget))))))))))) /\ exists elb_gap_base. elb_gap_base + elb_steps_base = (B)))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

25 script commands · 9 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro B
  4. L4
    intro hzero
02Use earlier factsL5–6

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

  1. L5
    specialize euclidean_trace_exists_linear a
  2. L6
    specialize euclidean_trace_exists_linear b
03Separate the logical casesL7–11

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

  1. L7
    cases euclidean_trace_exists_linear
  2. L8
    cases euclidean_trace_exists_linear_witness
  3. L9
    cases euclidean_trace_exists_linear_witness_witness
  4. L10
    cases euclidean_trace_exists_linear_witness_witness_witness
  5. L11
    cases euclidean_trace_exists_linear_witness_witness_witness_witness
04Establish hstepsL12–16

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

  1. L12
    have hsteps : x3 = 0
  2. L13
    specialize le_zero x3
  3. L14
    apply le_zero
  4. L15
    rewrite hzero at euclidean_trace_exists_linear_witness_witness_witness_witness_right
  5. L16
    exact euclidean_trace_exists_linear_witness_witness_witness_witness_right
05Construct an explicit witnessL17–20

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

  1. L17
    exists x
  2. L18
    exists x1
  3. L19
    exists x2
  4. L20
    exists x3
06Separate the logical casesL21–21

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

  1. L21
    split
07Use earlier factsL22–22

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

  1. L22
    exact euclidean_trace_exists_linear_witness_witness_witness_witness_left
08Construct an explicit witnessL23–23

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

  1. L23
    exists B
09Calculate and transport equalitiesL24–25

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

  1. L24
    rewrite hsteps
  2. L25
    simp

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro B
  4. 0004intro hzero
  5. 0005specialize euclidean_trace_exists_linear a
  6. 0006specialize euclidean_trace_exists_linear b
  7. 0007cases euclidean_trace_exists_linear
  8. 0008cases euclidean_trace_exists_linear_witness
  9. 0009cases euclidean_trace_exists_linear_witness_witness
  10. 0010cases euclidean_trace_exists_linear_witness_witness_witness
  11. 0011cases euclidean_trace_exists_linear_witness_witness_witness_witness
  12. 0012have hsteps : x3 = 0
  13. 0013specialize le_zero x3
  14. 0014apply le_zero
  15. 0015rewrite hzero at euclidean_trace_exists_linear_witness_witness_witness_witness_right
  16. 0016exact euclidean_trace_exists_linear_witness_witness_witness_witness_right
  17. 0017exists x
  18. 0018exists x1
  19. 0019exists x2
  20. 0020exists x3
  21. 0021split
  22. 0022exact euclidean_trace_exists_linear_witness_witness_witness_witness_left
  23. 0023exists B
  24. 0024rewrite hsteps
  25. 0025simp