PA0001 — zero

Exact expanded PA statement

forall n. 0 + n = n

Structural proof guide

Generated structural guide

Zero is a left identity for addition; unlike PA3, this needs induction.

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

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0002 mul_one PA000F add_comm PA000Q le_succ_self PA000W le_eq_or_lt PA0013 factor_difference PA0017 common_divisor_beta_moduli_divides_gap_times_c PA001A le_refl PA001C division_remainder_succ PA001K gcd_balanced_bezout_exists_up_to PA0021 dvd_to_mod_zero PA0026 binary_crt PA002E division_remainder_unique PA0034 beta_half_range_entry_bounds PA003E beta_at_self_of_bound PA005D predecessor_square_mod_one PA005L quadratic_residue_search_up_to PA005R quadratic_residue_bounded_equiv PA0065 factorial_succ_decompose PA0067 drop_add_prefix_from_fixed PA006Y odd_upper_remainder_reflection PA007C gauss_signed_half_magnitude_injective PA007V gauss_predecessor_half_range_aligned PA008F beta_range_one_entry_eq_succ PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00A2 prime_two_or_terminal_odd_shape PA00AP inverse_prefix_last_fixed PA00B2 prime_pair_order_paired_terminal_state_exists PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BG beta_range_two_product_is_factorial_succ PA00BN bounded_euler_criterion_dichotomy PA00BO double_predecessor_ne_one PA00BP odd_prime_one_not_mod_predecessor PA00BV arbitrary_gauss_lemma_complete PA00C2 odd_half_strictly_below_modulus PA00C3 odd_half_positive_complement_exists PA00CL odd_reflected_remainder_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient

Formal 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.