EL0005

euclidean_log_budget_weaken

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 19 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_succ Stable theorem; checked-use authorized

Direct dependents

EL000C euclidean_log_trace_below_power

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

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.

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

Separate complete second-wave branches: Full T13 proof · Alpha v27.