TS001D · theorem body

affine_collision_absolute_difference_norm_multiple

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

An actual balanced affine collision produces explicit natural absolute differences and an actual prime-divisible two-square norm.

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. ∀ a. ∀ b. ∀ c. ∀ d. Dvd(p,r · r + 1) → ModEq(p,r · a + b,r · c + d) → ∃ x. ∃ y. (a = c + x ∨ c = a + x) ∧ ((b = d + y ∨ d = b + y) ∧ Dvd(p,x · x + y · y))

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

PD0003 Dvd PD0008 ModEq

In local proof propositions

PD0008 ModEq
Exact expanded first-order statement
forall p r a b c d. (exists ftcn_factor_root. (r * r + 1) = (p) * ftcn_factor_root) -> (exists ftcn_left_collision ftcn_right_collision. (r * a + b) + (p) * ftcn_left_collision = (r * c + d) + (p) * ftcn_right_collision) -> exists x y. ((((a) = (c) + (x) \/ (c) = (a) + (x))) /\ ((((b) = (d) + (y) \/ (d) = (b) + (y))) /\ (exists ftcn_factor_norm. (x * x + y * y) = (p) * ftcn_factor_norm)))

Proof neighborhood

Direct theorem prerequisites

TS001A natural_absolute_difference_exists TS001C affine_collision_difference_linear_or_opposite TS0018 negative_one_linear_congruence_norm_multiple TS0019 negative_one_opposite_linear_congruence_norm_multiple

Direct theorem dependents

TS001M prime_floor_decoded_affine_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

52 script commands · 15 reading checkpoints · 3 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 (4)
natural absolute difference existsaffine collision difference linear or oppositenegative one linear congruence norm multiplenegative one opposite linear congruence norm multiple
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro d
  7. L7
    intro hroot
  8. L8
    intro hcollision
02Establish hfirstL9–12

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hfirst : exists x. (((a) = (c) + (x) \/ (c) = (a) + (x)))
  2. L10
    specialize natural_absolute_difference_exists a
  3. L11
    specialize natural_absolute_difference_exists c
  4. L12
    exact natural_absolute_difference_exists
03Separate the logical casesL13–13

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

  1. L13
    cases hfirst
04Establish hsecondL14–17

Establish this local claim before using it. It is not an additional assumption.

  1. L14
    have hsecond : exists y. (((b) = (d) + (y) \/ (d) = (b) + (y)))
  2. L15
    specialize natural_absolute_difference_exists b
  3. L16
    specialize natural_absolute_difference_exists d
  4. L17
    exact natural_absolute_difference_exists
05Separate the logical casesL18–18

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

  1. L18
    cases hsecond
06Construct an explicit witnessL19–20

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

  1. L19
    exists x
  2. L20
    exists x1
07Separate the logical casesL21–21

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

  1. L21
    split
08Use earlier factsL22–22

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

  1. L22
    exact hfirst_witness
09Separate the logical casesL23–23

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

  1. L23
    split
10Use earlier factsL24–24

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

  1. L24
    exact hsecond_witness
11Establish hsignL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply affine collision difference linear or opposite.

  1. L25
    have hsign : ModEq(p,r · x,x1) ∨ ModEq(p,r · x + x1,0)Definitions: ModEq(p,r · x,x1)ModEq(p,r · x + x1,0)Original native command in the exact edition
  2. L26
    specialize affine_collision_difference_linear_or_opposite p
  3. L27
    specialize affine_collision_difference_linear_or_opposite r
  4. L28
    specialize affine_collision_difference_linear_or_opposite a
  5. L29
    specialize affine_collision_difference_linear_or_opposite b
  6. L30
    specialize affine_collision_difference_linear_or_opposite c
  7. L31
    specialize affine_collision_difference_linear_or_opposite d
  8. L32
    specialize affine_collision_difference_linear_or_opposite x
  9. L33
    specialize affine_collision_difference_linear_or_opposite x1
  10. L34
    apply affine_collision_difference_linear_or_opposite
12Use earlier factsL35–37

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

  1. L35
    exact hcollision
  2. L36
    exact hfirst_witness
  3. L37
    exact hsecond_witness
13Separate the logical casesL38–38

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

  1. L38
    cases hsign
14Use earlier factsL39–48

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

  1. L39
    specialize negative_one_linear_congruence_norm_multiple p
  2. L40
    specialize negative_one_linear_congruence_norm_multiple r
  3. L41
    specialize negative_one_linear_congruence_norm_multiple x
  4. L42
    specialize negative_one_linear_congruence_norm_multiple x1
  5. L43
    apply negative_one_linear_congruence_norm_multiple
  6. L44
    exact hroot
  7. L45
    exact hsign_left
  8. L46
    specialize negative_one_opposite_linear_congruence_norm_multiple p
  9. L47
    specialize negative_one_opposite_linear_congruence_norm_multiple r
  10. L48
    specialize negative_one_opposite_linear_congruence_norm_multiple x
15Use earlier factsL49–52

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

  1. L49
    specialize negative_one_opposite_linear_congruence_norm_multiple x1
  2. L50
    apply negative_one_opposite_linear_congruence_norm_multiple
  3. L51
    exact hroot
  4. L52
    exact hsign_right

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro hroot
  8. 0008intro hcollision
  9. 0009have hfirst : exists x. (((a) = (c) + (x) \/ (c) = (a) + (x)))
  10. 0010specialize natural_absolute_difference_exists a
  11. 0011specialize natural_absolute_difference_exists c
  12. 0012exact natural_absolute_difference_exists
  13. 0013cases hfirst
  14. 0014have hsecond : exists y. (((b) = (d) + (y) \/ (d) = (b) + (y)))
  15. 0015specialize natural_absolute_difference_exists b
  16. 0016specialize natural_absolute_difference_exists d
  17. 0017exact natural_absolute_difference_exists
  18. 0018cases hsecond
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022exact hfirst_witness
  23. 0023split
  24. 0024exact hsecond_witness
  25. 0025have hsign : ModEq(p,r · x,x1) ∨ ModEq(p,r · x + x1,0)
    Exact native replay linehave hsign : (exists ftcn_left_collision_direct ftcn_right_collision_direct. (r * x) + (p) * ftcn_left_collision_direct = (x1) + (p) * ftcn_right_collision_direct) \/ (exists ftcn_left_collision_opposite ftcn_right_collision_opposite. (r * x + x1) + (p) * ftcn_left_collision_opposite = (0) + (p) * ftcn_right_collision_opposite)
  26. 0026specialize affine_collision_difference_linear_or_opposite p
  27. 0027specialize affine_collision_difference_linear_or_opposite r
  28. 0028specialize affine_collision_difference_linear_or_opposite a
  29. 0029specialize affine_collision_difference_linear_or_opposite b
  30. 0030specialize affine_collision_difference_linear_or_opposite c
  31. 0031specialize affine_collision_difference_linear_or_opposite d
  32. 0032specialize affine_collision_difference_linear_or_opposite x
  33. 0033specialize affine_collision_difference_linear_or_opposite x1
  34. 0034apply affine_collision_difference_linear_or_opposite
  35. 0035exact hcollision
  36. 0036exact hfirst_witness
  37. 0037exact hsecond_witness
  38. 0038cases hsign
  39. 0039specialize negative_one_linear_congruence_norm_multiple p
  40. 0040specialize negative_one_linear_congruence_norm_multiple r
  41. 0041specialize negative_one_linear_congruence_norm_multiple x
  42. 0042specialize negative_one_linear_congruence_norm_multiple x1
  43. 0043apply negative_one_linear_congruence_norm_multiple
  44. 0044exact hroot
  45. 0045exact hsign_left
  46. 0046specialize negative_one_opposite_linear_congruence_norm_multiple p
  47. 0047specialize negative_one_opposite_linear_congruence_norm_multiple r
  48. 0048specialize negative_one_opposite_linear_congruence_norm_multiple x
  49. 0049specialize negative_one_opposite_linear_congruence_norm_multiple x1
  50. 0050apply negative_one_opposite_linear_congruence_norm_multiple
  51. 0051exact hroot
  52. 0052exact hsign_right