PA003L

mod_eq_symm

Stable checked-use theorem · independently closed

Balanced natural congruence is symmetric.

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 m a b. (exists u v. a + m * u = b + m * v) -> exists r s. b + m * r = a + m * s

Structural proof guide

Generated structural guide

Balanced natural congruence is symmetric.

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

The proof proceeds by case analysis (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA003R mod_eq_cancel_coprime PA005J mod_eq_decidable_from_remainders PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0079 prime_scaled_same_target_unique PA0087 quadratic_residue_mod_equiv PA008E prime_mul_index_map_injective PA008M quadratic_residue_half_power_mod_one PA008O scaled_inverse_transport_right PA009C prime_scaled_inverse_unique PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BV arbitrary_gauss_lemma_complete PA00C5 canonical_remainder_from_mod PA00CJ matching_parity_mod_two PA00D5 mod_two_zero_sum_to_congruent PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00FL mod_two_preserves_parity

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

10 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 m
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro h
02Separate the logical casesL5–6

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

  1. L5
    cases h
  2. L6
    cases h_witness
03Construct an explicit witnessL7–8

Supply the displayed value, then prove that it has the required property.

  1. L7
    exists x1
  2. L8
    exists x
04Calculate and transport equalitiesL9–9

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

  1. L9
    symm
05Use earlier factsL10–10

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

  1. L10
    exact h_witness_witness

Library-wide reading audit

Original exact command ledger · 10 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro h
  5. 0005cases h
  6. 0006cases h_witness
  7. 0007exists x1
  8. 0008exists x
  9. 0009symm
  10. 0010exact h_witness_witness