TS001L · theorem body

equal_remainder_affine_values_balanced_congruent

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

Equal witnessed affine remainders produce an actual balanced affine-congruence certificate.

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.

Statement with defined notation

∀ p. ∀ r. ∀ i. ∀ j. ∀ q. ∀ i2. ∀ j2. ∀ q2. ∀ t. r · i + j = p · q + t → r · i2 + j2 = p · q2 + t → ModEq(p,r · i + j,r · i2 + j2)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

In local proof propositions

none
Exact expanded first-order statement
forall p r i j q i2 j2 q2 t. r * i + j = p * q + t -> r * i2 + j2 = p * q2 + t -> (exists ftcn_left_prime_affine ftcn_right_prime_affine. (r * i + j) + (p) * ftcn_left_prime_affine = (r * i2 + j2) + (p) * ftcn_right_prime_affine)

Proof neighborhood

Direct theorem prerequisites

TS0010 equal_affine_remainders_balanced

Direct theorem dependents

TS001N prime_floor_affine_grid_collision_represents_prime

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

25 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
equal affine remainders balanced
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro i
  4. L4
    intro j
  5. L5
    intro q
  6. L6
    intro i2
  7. L7
    intro j2
  8. L8
    intro q2
  9. L9
    intro t
  10. L10
    intro hfirst
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hsecond
03Construct an explicit witnessL12–13

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

  1. L12
    exists q2
  2. L13
    exists q
04Use earlier factsL14–23

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

  1. L14
    specialize equal_affine_remainders_balanced p
  2. L15
    specialize equal_affine_remainders_balanced r
  3. L16
    specialize equal_affine_remainders_balanced i
  4. L17
    specialize equal_affine_remainders_balanced j
  5. L18
    specialize equal_affine_remainders_balanced q
  6. L19
    specialize equal_affine_remainders_balanced i2
  7. L20
    specialize equal_affine_remainders_balanced j2
  8. L21
    specialize equal_affine_remainders_balanced q2
  9. L22
    specialize equal_affine_remainders_balanced t
  10. L23
    apply equal_affine_remainders_balanced
05Use earlier factsL24–25

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

  1. L24
    exact hfirst
  2. L25
    exact hsecond

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro i
  4. 0004intro j
  5. 0005intro q
  6. 0006intro i2
  7. 0007intro j2
  8. 0008intro q2
  9. 0009intro t
  10. 0010intro hfirst
  11. 0011intro hsecond
  12. 0012exists q2
  13. 0013exists q
  14. 0014specialize equal_affine_remainders_balanced p
  15. 0015specialize equal_affine_remainders_balanced r
  16. 0016specialize equal_affine_remainders_balanced i
  17. 0017specialize equal_affine_remainders_balanced j
  18. 0018specialize equal_affine_remainders_balanced q
  19. 0019specialize equal_affine_remainders_balanced i2
  20. 0020specialize equal_affine_remainders_balanced j2
  21. 0021specialize equal_affine_remainders_balanced q2
  22. 0022specialize equal_affine_remainders_balanced t
  23. 0023apply equal_affine_remainders_balanced
  24. 0024exact hfirst
  25. 0025exact hsecond