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 PA statement
forall n m k. (n + m) + k = n + (m + k)Structural proof guide
Generated structural guide
Addition is associative.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA000A mul_add PA000G mul_succ_left PA000R le_trans PA0013 factor_difference PA001I add_permute_outer PA001J balanced_bezout_euclid_step PA001W bezout_mod_left PA001X bezout_mod_right PA0024 mod_eq_trans PA0025 mod_eq_predecessor_cancel PA002D positive_quotient_gap_impossible PA0033 lt_of_le_of_lt PA0034 beta_half_range_entry_bounds PA003J add_le_add_right PA003K add_le_add_left PA003P coprime_balanced_mod_inverse PA005D predecessor_square_mod_one PA005N square_decomp PA005O add_residue PA0068 antisymm_from_witnesses PA006D odd_mul_odd PA006F even_add_odd PA006I odd_add_odd PA006N division_block_upper PA006O lt_trans PA006Y odd_upper_remainder_reflection PA0070 gauss_pointwise_signed_half_representative PA0090 euler_pair_iteration_previous_balance PA00A2 prime_two_or_terminal_odd_shape PA00AC pair_order_iteration_previous_balance PA00AD pair_order_iteration_step_room PA00AG prime_bounded_square_one_cases PA00C2 odd_half_strictly_below_modulus PA00C3 odd_half_positive_complement_exists PA00C4 predecessor_multiple_mod_complement PA00CL odd_reflected_remainder_mod_two PA00CM signed_remainder_sum_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00CU beta_sum_replace_balance PA00D1 mod_eq_add_cancel_left PA00D2 mod_two_cancel_middle PA00DQ odd_half_cross_product_gap PA00EP beta_sum_pointwise_addFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
Read the argument
Proof checkpoints
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.