TS001I · theorem body

distinct_flat_indices_have_positive_difference_norm

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

Distinct decoded flat indices force strictly positive norm of their witnessed absolute coordinate differences.

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

∀ w. ∀ k. ∀ k2. ∀ a. ∀ b. ∀ c. ∀ d. ∀ x. ∀ y. k = w · a + b → k2 = w · c + d → ¬k = k2 → a = c + x ∨ c = a + x → b = d + y ∨ d = b + y → Lt(0,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

PD0002 Lt

In local proof propositions

none
Exact expanded first-order statement
forall w k k2 a b c d x y. k = w * a + b -> k2 = w * c + d -> ~(k = k2) -> (((a) = (c) + (x) \/ (c) = (a) + (x))) -> (((b) = (d) + (y) \/ (d) = (b) + (y))) -> (exists ftcn_strict_flat_positive. ftcn_strict_flat_positive + S (0) = (x * x + y * y))

Proof neighborhood

Direct theorem prerequisites

TS001G absolute_difference_zero_forces_coordinate_equality TS001H nonzero_coordinate_pair_has_positive_square_norm

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

42 script commands · 9 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.

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 (2)
absolute difference zero forces coordinate equalitynonzero coordinate pair has positive square norm
01Fix variables and assumptionsL1–10

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

  1. L1
    intro w
  2. L2
    intro k
  3. L3
    intro k2
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro x
  9. L9
    intro y
  10. L10
    intro hfirst_index
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hsecond_index
  2. L12
    intro hdistinct
  3. L13
    intro hfirst_difference
  4. L14
    intro hsecond_difference
03Use earlier factsL15–17

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

  1. L15
    specialize nonzero_coordinate_pair_has_positive_square_norm x
  2. L16
    specialize nonzero_coordinate_pair_has_positive_square_norm y
  3. L17
    apply nonzero_coordinate_pair_has_positive_square_norm
04Fix variables and assumptionsL18–18

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

  1. L18
    intro hboth
05Separate the logical casesL19–19

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

  1. L19
    cases hboth
06Establish hrowL20–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply absolute difference zero forces coordinate equality.

  1. L20
    have hrow : a = c
  2. L21
    specialize absolute_difference_zero_forces_coordinate_equality a
  3. L22
    specialize absolute_difference_zero_forces_coordinate_equality c
  4. L23
    specialize absolute_difference_zero_forces_coordinate_equality x
  5. L24
    apply absolute_difference_zero_forces_coordinate_equality
  6. L25
    exact hfirst_difference
  7. L26
    exact hboth_left
07Establish hcolumnL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply absolute difference zero forces coordinate equality.

  1. L27
    have hcolumn : b = d
  2. L28
    specialize absolute_difference_zero_forces_coordinate_equality b
  3. L29
    specialize absolute_difference_zero_forces_coordinate_equality d
  4. L30
    specialize absolute_difference_zero_forces_coordinate_equality y
  5. L31
    apply absolute_difference_zero_forces_coordinate_equality
  6. L32
    exact hsecond_difference
  7. L33
    exact hboth_right
  8. L34
    apply hdistinct
  9. L35
    trans w * a + b
  10. L36
    exact hfirst_index
08Calculate and transport equalitiesL37–41

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

  1. L37
    trans w * c + d
  2. L38
    rewrite hrow
  3. L39
    rewrite hcolumn
  4. L40
    refl
  5. L41
    symm
09Use earlier factsL42–42

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

  1. L42
    exact hsecond_index

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro w
  2. 0002intro k
  3. 0003intro k2
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro x
  9. 0009intro y
  10. 0010intro hfirst_index
  11. 0011intro hsecond_index
  12. 0012intro hdistinct
  13. 0013intro hfirst_difference
  14. 0014intro hsecond_difference
  15. 0015specialize nonzero_coordinate_pair_has_positive_square_norm x
  16. 0016specialize nonzero_coordinate_pair_has_positive_square_norm y
  17. 0017apply nonzero_coordinate_pair_has_positive_square_norm
  18. 0018intro hboth
  19. 0019cases hboth
  20. 0020have hrow : a = c
  21. 0021specialize absolute_difference_zero_forces_coordinate_equality a
  22. 0022specialize absolute_difference_zero_forces_coordinate_equality c
  23. 0023specialize absolute_difference_zero_forces_coordinate_equality x
  24. 0024apply absolute_difference_zero_forces_coordinate_equality
  25. 0025exact hfirst_difference
  26. 0026exact hboth_left
  27. 0027have hcolumn : b = d
  28. 0028specialize absolute_difference_zero_forces_coordinate_equality b
  29. 0029specialize absolute_difference_zero_forces_coordinate_equality d
  30. 0030specialize absolute_difference_zero_forces_coordinate_equality y
  31. 0031apply absolute_difference_zero_forces_coordinate_equality
  32. 0032exact hsecond_difference
  33. 0033exact hboth_right
  34. 0034apply hdistinct
  35. 0035trans w * a + b
  36. 0036exact hfirst_index
  37. 0037trans w * c + d
  38. 0038rewrite hrow
  39. 0039rewrite hcolumn
  40. 0040refl
  41. 0041symm
  42. 0042exact hsecond_index