CR0014

crt_prefix_solutions_pointwise_congruent

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Two simultaneous solutions are congruent modulo every actually decoded list 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 first-order arithmetic statement

forall r s b c l x y i a m. (forall gcrt_solution_index_pointwise_solution_left gcrt_solution_residue_pointwise_solution_left gcrt_solution_modulus_pointwise_solution_left. (exists ff_lt_gcrt_pointwise_solution_left_bound. ff_lt_gcrt_pointwise_solution_left_bound + S gcrt_solution_index_pointwise_solution_left = l) -> (((exists ff_h_gcrt_pointwise_solution_left_residue. ff_h_gcrt_pointwise_solution_left_residue + S (gcrt_solution_residue_pointwise_solution_left) = S ((S (gcrt_solution_index_pointwise_solution_left)) * s)) /\ exists ff_q_gcrt_pointwise_solution_left_residue. r = ff_q_gcrt_pointwise_solution_left_residue * S ((S (gcrt_solution_index_pointwise_solution_left)) * s) + (gcrt_solution_residue_pointwise_solution_left))) -> (((exists ff_h_gcrt_pointwise_solution_left_modulus. ff_h_gcrt_pointwise_solution_left_modulus + S (gcrt_solution_modulus_pointwise_solution_left) = S ((S (gcrt_solution_index_pointwise_solution_left)) * c)) /\ exists ff_q_gcrt_pointwise_solution_left_modulus. b = ff_q_gcrt_pointwise_solution_left_modulus * S ((S (gcrt_solution_index_pointwise_solution_left)) * c) + (gcrt_solution_modulus_pointwise_solution_left))) -> (exists hgcrt_mod_left_gcrt_pointwise_solution_left_congruence hgcrt_mod_right_gcrt_pointwise_solution_left_congruence. x + gcrt_solution_modulus_pointwise_solution_left * hgcrt_mod_left_gcrt_pointwise_solution_left_congruence = gcrt_solution_residue_pointwise_solution_left + gcrt_solution_modulus_pointwise_solution_left * hgcrt_mod_right_gcrt_pointwise_solution_left_congruence)) -> (forall gcrt_solution_index_pointwise_solution_right gcrt_solution_residue_pointwise_solution_right gcrt_solution_modulus_pointwise_solution_right. (exists ff_lt_gcrt_pointwise_solution_right_bound. ff_lt_gcrt_pointwise_solution_right_bound + S gcrt_solution_index_pointwise_solution_right = l) -> (((exists ff_h_gcrt_pointwise_solution_right_residue. ff_h_gcrt_pointwise_solution_right_residue + S (gcrt_solution_residue_pointwise_solution_right) = S ((S (gcrt_solution_index_pointwise_solution_right)) * s)) /\ exists ff_q_gcrt_pointwise_solution_right_residue. r = ff_q_gcrt_pointwise_solution_right_residue * S ((S (gcrt_solution_index_pointwise_solution_right)) * s) + (gcrt_solution_residue_pointwise_solution_right))) -> (((exists ff_h_gcrt_pointwise_solution_right_modulus. ff_h_gcrt_pointwise_solution_right_modulus + S (gcrt_solution_modulus_pointwise_solution_right) = S ((S (gcrt_solution_index_pointwise_solution_right)) * c)) /\ exists ff_q_gcrt_pointwise_solution_right_modulus. b = ff_q_gcrt_pointwise_solution_right_modulus * S ((S (gcrt_solution_index_pointwise_solution_right)) * c) + (gcrt_solution_modulus_pointwise_solution_right))) -> (exists hgcrt_mod_left_gcrt_pointwise_solution_right_congruence hgcrt_mod_right_gcrt_pointwise_solution_right_congruence. y + gcrt_solution_modulus_pointwise_solution_right * hgcrt_mod_left_gcrt_pointwise_solution_right_congruence = gcrt_solution_residue_pointwise_solution_right + gcrt_solution_modulus_pointwise_solution_right * hgcrt_mod_right_gcrt_pointwise_solution_right_congruence)) -> (exists ff_lt_gcrt_pointwise_index. ff_lt_gcrt_pointwise_index + S i = l) -> (((exists ff_h_gcrt_pointwise_residue. ff_h_gcrt_pointwise_residue + S (a) = S ((S (i)) * s)) /\ exists ff_q_gcrt_pointwise_residue. r = ff_q_gcrt_pointwise_residue * S ((S (i)) * s) + (a))) -> (((exists ff_h_gcrt_pointwise_modulus. ff_h_gcrt_pointwise_modulus + S (m) = S ((S (i)) * c)) /\ exists ff_q_gcrt_pointwise_modulus. b = ff_q_gcrt_pointwise_modulus * S ((S (i)) * c) + (m))) -> (exists hgcrt_mod_left_gcrt_pointwise_result hgcrt_mod_right_gcrt_pointwise_result. x + m * hgcrt_mod_left_gcrt_pointwise_result = y + m * hgcrt_mod_right_gcrt_pointwise_result)

Constructive proof overview

Generated structural guide

Two simultaneous solutions are congruent modulo every actually decoded list modulus.

The unchanged tactic script uses 2 declared prerequisites and contains 38 exact native proof lines.

Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

mod_eq_symm Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized

Direct dependents

CR0016 crt_prefix_ordered_solutions_gap_multiple

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

38 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–10

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro l
  6. L6
    intro x
  7. L7
    intro y
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro m
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hx
  2. L12
    intro hy
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hm
03Use earlier factsL16–25

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

  1. L16
    specialize mod_eq_trans m
  2. L17
    specialize mod_eq_trans x
  3. L18
    specialize mod_eq_trans a
  4. L19
    specialize mod_eq_trans y
  5. L20
    apply mod_eq_trans
  6. L21
    specialize hx i
  7. L22
    specialize hx a
  8. L23
    specialize hx m
  9. L24
    apply hx
  10. L25
    exact hi
04Use earlier factsL26–35

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

  1. L26
    exact ha
  2. L27
    exact hm
  3. L28
    specialize mod_eq_symm m
  4. L29
    specialize mod_eq_symm y
  5. L30
    specialize mod_eq_symm a
  6. L31
    apply mod_eq_symm
  7. L32
    specialize hy i
  8. L33
    specialize hy a
  9. L34
    specialize hy m
  10. L35
    apply hy
05Use earlier factsL36–38

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

  1. L36
    exact hi
  2. L37
    exact ha
  3. L38
    exact hm

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro x
  7. 0007intro y
  8. 0008intro i
  9. 0009intro a
  10. 0010intro m
  11. 0011intro hx
  12. 0012intro hy
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hm
  16. 0016specialize mod_eq_trans m
  17. 0017specialize mod_eq_trans x
  18. 0018specialize mod_eq_trans a
  19. 0019specialize mod_eq_trans y
  20. 0020apply mod_eq_trans
  21. 0021specialize hx i
  22. 0022specialize hx a
  23. 0023specialize hx m
  24. 0024apply hx
  25. 0025exact hi
  26. 0026exact ha
  27. 0027exact hm
  28. 0028specialize mod_eq_symm m
  29. 0029specialize mod_eq_symm y
  30. 0030specialize mod_eq_symm a
  31. 0031apply mod_eq_symm
  32. 0032specialize hy i
  33. 0033specialize hy a
  34. 0034specialize hy m
  35. 0035apply hy
  36. 0036exact hi
  37. 0037exact ha
  38. 0038exact hm

Separate complete second-wave branches: Full G011 proof · Alpha v27.