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. ∀ n. EuclideanBoundedTrace(a,b,S S (n + n)) → EuclideanBoundedTrace(a,b,S n + S n)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall a b n. (exists elb_list_doubled elb_history_doubled elb_scale_doubled elb_steps_doubled. ((exists cf_gcd_elb_doubled_budget. ((((exists ff_h_cf_elb_doubled_budget_initial_state. ff_h_cf_elb_doubled_budget_initial_state + S (((cf_gcd_elb_doubled_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_doubled_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_doubled)) /\ exists ff_q_cf_elb_doubled_budget_initial_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_initial_state * S ((S (0)) * elb_scale_doubled) + (((cf_gcd_elb_doubled_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_doubled_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_doubled_budget_terminal_state. ff_h_cf_elb_doubled_budget_terminal_state + S (((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) * S ((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) + ((((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))))) = S ((S (elb_steps_doubled)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_terminal_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_terminal_state * S ((S (elb_steps_doubled)) * elb_scale_doubled) + (((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) * S ((a) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled)))) + ((((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))) + (((b) + (elb_list_doubled)) * S ((b) + (elb_list_doubled)) + ((elb_list_doubled) + (elb_list_doubled))))))) /\ forall cf_index_elb_doubled_budget. (exists ff_lt_cf_elb_doubled_budget_index. ff_lt_cf_elb_doubled_budget_index + S cf_index_elb_doubled_budget = elb_steps_doubled) -> exists cf_old_a_elb_doubled_budget cf_old_b_elb_doubled_budget cf_tail_elb_doubled_budget cf_new_a_elb_doubled_budget cf_new_b_elb_doubled_budget cf_head_elb_doubled_budget cf_quotient_elb_doubled_budget. ((((exists ff_h_cf_elb_doubled_budget_previous_state. ff_h_cf_elb_doubled_budget_previous_state + S (((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) * S ((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) + ((((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))))) = S ((S (cf_index_elb_doubled_budget)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_previous_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_previous_state * S ((S (cf_index_elb_doubled_budget)) * elb_scale_doubled) + (((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) * S ((cf_old_a_elb_doubled_budget) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget)))) + ((((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))) + (((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) * S ((cf_old_b_elb_doubled_budget) + (cf_tail_elb_doubled_budget)) + ((cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget))))))) /\ ((((exists ff_h_cf_elb_doubled_budget_following_state. ff_h_cf_elb_doubled_budget_following_state + S (((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) * S ((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) + ((((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))))) = S ((S (S cf_index_elb_doubled_budget)) * elb_scale_doubled)) /\ exists ff_q_cf_elb_doubled_budget_following_state. elb_history_doubled = ff_q_cf_elb_doubled_budget_following_state * S ((S (S cf_index_elb_doubled_budget)) * elb_scale_doubled) + (((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) * S ((cf_new_a_elb_doubled_budget) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget)))) + ((((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))) + (((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) * S ((cf_new_b_elb_doubled_budget) + (cf_head_elb_doubled_budget)) + ((cf_head_elb_doubled_budget) + (cf_head_elb_doubled_budget))))))) /\ (cf_new_b_elb_doubled_budget = cf_old_a_elb_doubled_budget /\ (cf_new_a_elb_doubled_budget = cf_new_b_elb_doubled_budget * cf_quotient_elb_doubled_budget + cf_old_b_elb_doubled_budget /\ ((exists ff_lt_cf_elb_doubled_budget_remainder. ff_lt_cf_elb_doubled_budget_remainder + S cf_old_b_elb_doubled_budget = cf_new_b_elb_doubled_budget) /\ (cf_head_elb_doubled_budget = S ((cf_quotient_elb_doubled_budget + cf_tail_elb_doubled_budget) * S (cf_quotient_elb_doubled_budget + cf_tail_elb_doubled_budget) + (cf_tail_elb_doubled_budget + cf_tail_elb_doubled_budget))))))))))) /\ exists elb_gap_doubled. elb_gap_doubled + elb_steps_doubled = (S (S (n + n))))) -> (exists elb_list_successor elb_history_successor elb_scale_successor elb_steps_successor. ((exists cf_gcd_elb_successor_budget. ((((exists ff_h_cf_elb_successor_budget_initial_state. ff_h_cf_elb_successor_budget_initial_state + S (((cf_gcd_elb_successor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_successor_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_successor)) /\ exists ff_q_cf_elb_successor_budget_initial_state. elb_history_successor = ff_q_cf_elb_successor_budget_initial_state * S ((S (0)) * elb_scale_successor) + (((cf_gcd_elb_successor_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_successor_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_successor_budget_terminal_state. ff_h_cf_elb_successor_budget_terminal_state + S (((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) * S ((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) + ((((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))))) = S ((S (elb_steps_successor)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_terminal_state. elb_history_successor = ff_q_cf_elb_successor_budget_terminal_state * S ((S (elb_steps_successor)) * elb_scale_successor) + (((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) * S ((a) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor)))) + ((((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))) + (((b) + (elb_list_successor)) * S ((b) + (elb_list_successor)) + ((elb_list_successor) + (elb_list_successor))))))) /\ forall cf_index_elb_successor_budget. (exists ff_lt_cf_elb_successor_budget_index. ff_lt_cf_elb_successor_budget_index + S cf_index_elb_successor_budget = elb_steps_successor) -> exists cf_old_a_elb_successor_budget cf_old_b_elb_successor_budget cf_tail_elb_successor_budget cf_new_a_elb_successor_budget cf_new_b_elb_successor_budget cf_head_elb_successor_budget cf_quotient_elb_successor_budget. ((((exists ff_h_cf_elb_successor_budget_previous_state. ff_h_cf_elb_successor_budget_previous_state + S (((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) * S ((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) + ((((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))))) = S ((S (cf_index_elb_successor_budget)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_previous_state. elb_history_successor = ff_q_cf_elb_successor_budget_previous_state * S ((S (cf_index_elb_successor_budget)) * elb_scale_successor) + (((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) * S ((cf_old_a_elb_successor_budget) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget)))) + ((((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))) + (((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) * S ((cf_old_b_elb_successor_budget) + (cf_tail_elb_successor_budget)) + ((cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget))))))) /\ ((((exists ff_h_cf_elb_successor_budget_following_state. ff_h_cf_elb_successor_budget_following_state + S (((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) * S ((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) + ((((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))))) = S ((S (S cf_index_elb_successor_budget)) * elb_scale_successor)) /\ exists ff_q_cf_elb_successor_budget_following_state. elb_history_successor = ff_q_cf_elb_successor_budget_following_state * S ((S (S cf_index_elb_successor_budget)) * elb_scale_successor) + (((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) * S ((cf_new_a_elb_successor_budget) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget)))) + ((((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))) + (((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) * S ((cf_new_b_elb_successor_budget) + (cf_head_elb_successor_budget)) + ((cf_head_elb_successor_budget) + (cf_head_elb_successor_budget))))))) /\ (cf_new_b_elb_successor_budget = cf_old_a_elb_successor_budget /\ (cf_new_a_elb_successor_budget = cf_new_b_elb_successor_budget * cf_quotient_elb_successor_budget + cf_old_b_elb_successor_budget /\ ((exists ff_lt_cf_elb_successor_budget_remainder. ff_lt_cf_elb_successor_budget_remainder + S cf_old_b_elb_successor_budget = cf_new_b_elb_successor_budget) /\ (cf_head_elb_successor_budget = S ((cf_quotient_elb_successor_budget + cf_tail_elb_successor_budget) * S (cf_quotient_elb_successor_budget + cf_tail_elb_successor_budget) + (cf_tail_elb_successor_budget + cf_tail_elb_successor_budget))))))))))) /\ exists elb_gap_successor. elb_gap_successor + elb_steps_successor = ((S n + S n))))Complete unchanged native tactic proof
All 7 lines are the exact independently kernel-checked original script.
Read the argument
Proof checkpoints
7 script commands · 4 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.
Named ingredients (1)
01Fix variables and assumptionsL1–4
02Use earlier factsL5–5
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L5
specialize euclidean_log_double_successor n
03Calculate and transport equalitiesL6–6
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L6
rewrite euclidean_log_double_successor
04Use earlier factsL7–7
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L7
exact htrace
Original defined command ledger · 7 lines
- 0001
intro a - 0002
intro b - 0003
intro n - 0004
intro htrace - 0005
specialize euclidean_log_double_successor n - 0006
rewrite euclidean_log_double_successor - 0007
exact htrace