PA0004

add_eq_zero_right

Stable checked-use theorem · independently closed

A sum equal to zero has zero as its right addend.

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 a b. a + b = 0 -> b = 0

Structural proof guide

Generated structural guide

A sum equal to zero has zero as its right addend.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (1), equality transport (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0006 beta_range_empty PA0007 mul_eq_zero PA000J add_eq_zero_left PA000N mul_eq_one_components PA0013 factor_difference PA001B le_zero PA002I bounded_beta_exclusive_recode_invariant PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0043 beta_repeat_empty PA004F finite_surjective_zero PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA0052 beta_product_replace_balance PA005L quadratic_residue_search_up_to PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007G beta_sign_factor_prefix_exists PA007L beta_pointwise_mul_prefix_exists PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008S prime_scaled_inverse_prefix_exists_bounded PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero PA008Y adjacent_scaled_orbit_history_zero PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA00A6 prime_inverse_prefix_exists_bounded PA00A8 orbit_closed_prefix_zero PA00A9 nonendpoint_prefix_zero PA00AB paired_inverse_witness_zero PA00BY beta_division_prefix_exists PA00CU beta_sum_replace_balance PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00E9 eisenstein_transposed_column_prefix_exists PA00EI eisenstein_transposed_column_count_prefix_exists PA00EX eisenstein_successor_row_split_prefix_exists

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.

Read the argument

Proof checkpoints

9 script commands · 6 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–1

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
02Induction on bL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction b
  2. L3
    intro h
  3. L4
    refl
  4. L5
    intro h
03Separate the logical casesL6–6

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

  1. L6
    exfalso
04Use earlier factsL7–7

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

  1. L7
    apply PA1
05Calculate and transport equalitiesL8–8

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L8
    rewrite PA4 at h
06Use earlier factsL9–9

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

  1. L9
    exact h

Library-wide reading audit

Original exact command ledger · 9 lines
  1. 0001intro a
  2. 0002induction b
  3. 0003intro h
  4. 0004refl
  5. 0005intro h
  6. 0006exfalso
  7. 0007apply PA1
  8. 0008rewrite PA4 at h
  9. 0009exact h