EL0005

euclidean_log_budget_weaken

Any actual complete Euclidean beta-history remains valid under one extra budget unit.

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. EuclideanBoundedTrace(a,b,B) → EuclideanBoundedTrace(a,b,S B)

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

Definition DAG

EuclideanBoundedTrace(a,b,B) · 2

Actual proof prerequisites

le_succ · checked external prerequisite
Original expanded first-order statement 
forall a b B. (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))) -> (exists elb_list_weakened elb_history_weakened elb_scale_weakened elb_steps_weakened. ((exists cf_gcd_elb_weakened_budget. ((((exists ff_h_cf_elb_weakened_budget_initial_state. ff_h_cf_elb_weakened_budget_initial_state + S (((cf_gcd_elb_weakened_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_weakened_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_weakened)) /\ exists ff_q_cf_elb_weakened_budget_initial_state. elb_history_weakened = ff_q_cf_elb_weakened_budget_initial_state * S ((S (0)) * elb_scale_weakened) + (((cf_gcd_elb_weakened_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_weakened_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_weakened_budget_terminal_state. ff_h_cf_elb_weakened_budget_terminal_state + S (((a) + (((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened)))) * S ((a) + (((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened)))) + ((((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened))) + (((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened))))) = S ((S (elb_steps_weakened)) * elb_scale_weakened)) /\ exists ff_q_cf_elb_weakened_budget_terminal_state. elb_history_weakened = ff_q_cf_elb_weakened_budget_terminal_state * S ((S (elb_steps_weakened)) * elb_scale_weakened) + (((a) + (((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened)))) * S ((a) + (((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened)))) + ((((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened))) + (((b) + (elb_list_weakened)) * S ((b) + (elb_list_weakened)) + ((elb_list_weakened) + (elb_list_weakened))))))) /\ forall cf_index_elb_weakened_budget. (exists ff_lt_cf_elb_weakened_budget_index. ff_lt_cf_elb_weakened_budget_index + S cf_index_elb_weakened_budget = elb_steps_weakened) -> exists cf_old_a_elb_weakened_budget cf_old_b_elb_weakened_budget cf_tail_elb_weakened_budget cf_new_a_elb_weakened_budget cf_new_b_elb_weakened_budget cf_head_elb_weakened_budget cf_quotient_elb_weakened_budget. ((((exists ff_h_cf_elb_weakened_budget_previous_state. ff_h_cf_elb_weakened_budget_previous_state + S (((cf_old_a_elb_weakened_budget) + (((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget)))) * S ((cf_old_a_elb_weakened_budget) + (((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget)))) + ((((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget))) + (((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget))))) = S ((S (cf_index_elb_weakened_budget)) * elb_scale_weakened)) /\ exists ff_q_cf_elb_weakened_budget_previous_state. elb_history_weakened = ff_q_cf_elb_weakened_budget_previous_state * S ((S (cf_index_elb_weakened_budget)) * elb_scale_weakened) + (((cf_old_a_elb_weakened_budget) + (((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget)))) * S ((cf_old_a_elb_weakened_budget) + (((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget)))) + ((((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget))) + (((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) * S ((cf_old_b_elb_weakened_budget) + (cf_tail_elb_weakened_budget)) + ((cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget))))))) /\ ((((exists ff_h_cf_elb_weakened_budget_following_state. ff_h_cf_elb_weakened_budget_following_state + S (((cf_new_a_elb_weakened_budget) + (((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget)))) * S ((cf_new_a_elb_weakened_budget) + (((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget)))) + ((((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget))) + (((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget))))) = S ((S (S cf_index_elb_weakened_budget)) * elb_scale_weakened)) /\ exists ff_q_cf_elb_weakened_budget_following_state. elb_history_weakened = ff_q_cf_elb_weakened_budget_following_state * S ((S (S cf_index_elb_weakened_budget)) * elb_scale_weakened) + (((cf_new_a_elb_weakened_budget) + (((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget)))) * S ((cf_new_a_elb_weakened_budget) + (((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget)))) + ((((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget))) + (((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) * S ((cf_new_b_elb_weakened_budget) + (cf_head_elb_weakened_budget)) + ((cf_head_elb_weakened_budget) + (cf_head_elb_weakened_budget))))))) /\ (cf_new_b_elb_weakened_budget = cf_old_a_elb_weakened_budget /\ (cf_new_a_elb_weakened_budget = cf_new_b_elb_weakened_budget * cf_quotient_elb_weakened_budget + cf_old_b_elb_weakened_budget /\ ((exists ff_lt_cf_elb_weakened_budget_remainder. ff_lt_cf_elb_weakened_budget_remainder + S cf_old_b_elb_weakened_budget = cf_new_b_elb_weakened_budget) /\ (cf_head_elb_weakened_budget = S ((cf_quotient_elb_weakened_budget + cf_tail_elb_weakened_budget) * S (cf_quotient_elb_weakened_budget + cf_tail_elb_weakened_budget) + (cf_tail_elb_weakened_budget + cf_tail_elb_weakened_budget))))))))))) /\ exists elb_gap_weakened. elb_gap_weakened + elb_steps_weakened = (S B)))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

19 script commands · 5 reading checkpoints · 0 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 htrace
02Separate the logical casesL5–9

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

  1. L5
    cases htrace
  2. L6
    cases htrace_witness
  3. L7
    cases htrace_witness_witness
  4. L8
    cases htrace_witness_witness_witness
  5. L9
    cases htrace_witness_witness_witness_witness
03Construct an explicit witnessL10–13

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

  1. L10
    exists x
  2. L11
    exists x1
  3. L12
    exists x2
  4. L13
    exists x3
04Separate the logical casesL14–14

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

  1. L14
    split
05Use earlier factsL15–19

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

  1. L15
    exact htrace_witness_witness_witness_witness_left
  2. L16
    specialize le_succ x3
  3. L17
    specialize le_succ B
  4. L18
    apply le_succ
  5. L19
    exact htrace_witness_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro B
  4. 0004intro htrace
  5. 0005cases htrace
  6. 0006cases htrace_witness
  7. 0007cases htrace_witness_witness
  8. 0008cases htrace_witness_witness_witness
  9. 0009cases htrace_witness_witness_witness_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012exists x2
  13. 0013exists x3
  14. 0014split
  15. 0015exact htrace_witness_witness_witness_witness_left
  16. 0016specialize le_succ x3
  17. 0017specialize le_succ B
  18. 0018apply le_succ
  19. 0019exact htrace_witness_witness_witness_witness_right