BT004U

binary_crt_fold_step

Stable checked-use theorem · independently kernel verified

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

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 P n x b. ~(P = 0) -> ~(n = 0) -> (forall d. (exists u. P = d * u) -> (exists v. n = d * v) -> d = 1) -> exists z. ((forall m a. (exists k. P = m * k) -> (exists u v. x + m * u = a + m * v) -> exists r s. z + m * r = a + m * s) /\ exists q r. z + n * q = b + n * r)

Structural proof guide

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

Direct prerequisites: binary_crt, mod_eq_of_mod_eq_multiple, mod_eq_trans. The authored body proceeds by case analysis (2), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT004F binary_crt BT004T mod_eq_of_mod_eq_multiple BT003Q mod_eq_trans

Direct dependents

BT005A beta_exclusive_recode_congruence_step BT005D beta_prefix_extend

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

40 script commands · 8 reading checkpoints · 2 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 (3)
binary crtmod eq of mod eq multiplemod eq trans
01Fix variables and assumptionsL1–7

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

  1. L1
    intro P
  2. L2
    intro n
  3. L3
    intro x
  4. L4
    intro b
  5. L5
    intro hP
  6. L6
    intro hn
  7. L7
    intro hcop
02Establish hcrtL8–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary crt.

  1. L8
    have hcrt : exists z. (exists u v. z + P * u = x + P * v) /\ (exists q r. z + n * q = b + n * r)
  2. L9
    specialize binary_crt P
  3. L10
    specialize binary_crt n
  4. L11
    specialize binary_crt x
  5. L12
    specialize binary_crt b
  6. L13
    apply binary_crt
  7. L14
    exact hP
  8. L15
    exact hn
  9. L16
    exact hcop
03Separate the logical casesL17–18

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

  1. L17
    cases hcrt
  2. L18
    cases hcrt_witness
04Construct an explicit witnessL19–19

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

  1. L19
    exists x1
05Separate the logical casesL20–20

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

  1. L20
    split
06Fix variables and assumptionsL21–24

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

  1. L21
    intro m
  2. L22
    intro a
  3. L23
    intro hmP
  4. L24
    intro hxa
07Establish hzxL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq of mod eq multiple.

  1. L25
    have hzx : exists u v. x1 + m * u = x + m * v
  2. L26
    specialize mod_eq_of_mod_eq_multiple m
  3. L27
    specialize mod_eq_of_mod_eq_multiple P
  4. L28
    specialize mod_eq_of_mod_eq_multiple x1
  5. L29
    specialize mod_eq_of_mod_eq_multiple x
  6. L30
    apply mod_eq_of_mod_eq_multiple
  7. L31
    exact hmP
  8. L32
    exact hcrt_witness_left
  9. L33
    specialize mod_eq_trans m
  10. L34
    specialize mod_eq_trans x1
08Use earlier factsL35–40

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

  1. L35
    specialize mod_eq_trans x
  2. L36
    specialize mod_eq_trans a
  3. L37
    apply mod_eq_trans
  4. L38
    exact hzx
  5. L39
    exact hxa
  6. L40
    exact hcrt_witness_right

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001intro P
  2. 0002intro n
  3. 0003intro x
  4. 0004intro b
  5. 0005intro hP
  6. 0006intro hn
  7. 0007intro hcop
  8. 0008have hcrt : exists z. (exists u v. z + P * u = x + P * v) /\ (exists q r. z + n * q = b + n * r)
  9. 0009specialize binary_crt P
  10. 0010specialize binary_crt n
  11. 0011specialize binary_crt x
  12. 0012specialize binary_crt b
  13. 0013apply binary_crt
  14. 0014exact hP
  15. 0015exact hn
  16. 0016exact hcop
  17. 0017cases hcrt
  18. 0018cases hcrt_witness
  19. 0019exists x1
  20. 0020split
  21. 0021intro m
  22. 0022intro a
  23. 0023intro hmP
  24. 0024intro hxa
  25. 0025have hzx : exists u v. x1 + m * u = x + m * v
  26. 0026specialize mod_eq_of_mod_eq_multiple m
  27. 0027specialize mod_eq_of_mod_eq_multiple P
  28. 0028specialize mod_eq_of_mod_eq_multiple x1
  29. 0029specialize mod_eq_of_mod_eq_multiple x
  30. 0030apply mod_eq_of_mod_eq_multiple
  31. 0031exact hmP
  32. 0032exact hcrt_witness_left
  33. 0033specialize mod_eq_trans m
  34. 0034specialize mod_eq_trans x1
  35. 0035specialize mod_eq_trans x
  36. 0036specialize mod_eq_trans a
  37. 0037apply mod_eq_trans
  38. 0038exact hzx
  39. 0039exact hxa
  40. 0040exact hcrt_witness_right