PA0027

mod_eq_of_mod_eq_multiple

Stable checked-use theorem · independently closed

Balanced congruence descends from a multiple modulus to every divisor modulus.

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

Structural proof guide

Generated structural guide

Balanced congruence descends from a multiple modulus to every divisor modulus.

Use the direct prerequisites mul_assoc as previously established PA formulas.

The proof proceeds by case analysis (3), equality transport (2).

Referenced ingredients

PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA000B mul_assoc

Direct dependents

PA0028 binary_crt_fold_step

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

23 script commands · 10 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.

Named ingredients (1)
mul assoc
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro P
  3. L3
    intro x
  4. L4
    intro a
  5. L5
    intro hdiv
  6. L6
    intro hmod
02Separate the logical casesL7–9

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

  1. L7
    cases hdiv
  2. L8
    cases hmod
  3. L9
    cases hmod_witness
03Calculate and transport equalitiesL10–11

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

  1. L10
    rewrite hdiv_witness at hmod_witness_witness
  2. L11
    rewrite hdiv_witness at hmod_witness_witness
04Construct an explicit witnessL12–13

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

  1. L12
    exists x1 * x2
  2. L13
    exists x1 * x3
05Calculate and transport equalitiesL14–17

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

  1. L14
    trans x + (m * x1) * x2
  2. L15
    congr
  3. L16
    refl
  4. L17
    symm
06Use earlier factsL18–18

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

  1. L18
    apply mul_assoc
07Calculate and transport equalitiesL19–19

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

  1. L19
    trans a + (m * x1) * x3
08Use earlier factsL20–20

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

  1. L20
    exact hmod_witness_witness
09Calculate and transport equalitiesL21–22

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

  1. L21
    congr
  2. L22
    refl
10Use earlier factsL23–23

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

  1. L23
    apply mul_assoc

Library-wide reading audit

Original exact command ledger · 23 lines
  1. 0001intro m
  2. 0002intro P
  3. 0003intro x
  4. 0004intro a
  5. 0005intro hdiv
  6. 0006intro hmod
  7. 0007cases hdiv
  8. 0008cases hmod
  9. 0009cases hmod_witness
  10. 0010rewrite hdiv_witness at hmod_witness_witness
  11. 0011rewrite hdiv_witness at hmod_witness_witness
  12. 0012exists x1 * x2
  13. 0013exists x1 * x3
  14. 0014trans x + (m * x1) * x2
  15. 0015congr
  16. 0016refl
  17. 0017symm
  18. 0018apply mul_assoc
  19. 0019trans a + (m * x1) * x3
  20. 0020exact hmod_witness_witness
  21. 0021congr
  22. 0022refl
  23. 0023apply mul_assoc