TS001H · theorem body

nonzero_coordinate_pair_has_positive_square_norm

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

A natural coordinate pair not identically zero has a witnessed strictly positive 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

∀ x. ∀ y. ¬(x = 0 ∧ y = 0) → 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 x y. ~(x = 0 /\ y = 0) -> (exists ftcn_strict_prime_positive. ftcn_strict_prime_positive + S (0) = (x * x + y * y))

Proof neighborhood

Direct theorem prerequisites

zero_or_succ · Stable closed add_eq_zero_left · Stable closed add_eq_zero_right · Stable closed mul_eq_zero · Stable closed

Direct theorem dependents

TS001I distinct_flat_indices_have_positive_difference_norm

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

38 script commands · 16 reading checkpoints · 4 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro x
  2. L2
    intro y
  3. L3
    intro hnonzero
02Use earlier factsL4–4

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

  1. L4
    specialize zero_or_succ (x * x + y * y)
03Separate the logical casesL5–6

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

  1. L5
    cases zero_or_succ
  2. L6
    exfalso
04Use earlier factsL7–7

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

  1. L7
    apply hnonzero
05Separate the logical casesL8–8

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

  1. L8
    split
06Establish hxL9–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero left.

  1. L9
    have hx : x * x = 0
  2. L10
    specialize add_eq_zero_left (x * x)
  3. L11
    specialize add_eq_zero_left (y * y)
  4. L12
    apply add_eq_zero_left
  5. L13
    exact zero_or_succ_left
07Establish hxsplitL14–18

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

  1. L14
    have hxsplit : x = 0 \/ x = 0
  2. L15
    specialize mul_eq_zero x
  3. L16
    specialize mul_eq_zero x
  4. L17
    apply mul_eq_zero
  5. L18
    exact hx
08Separate the logical casesL19–19

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

  1. L19
    cases hxsplit
09Use earlier factsL20–21

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

  1. L20
    exact hxsplit_left
  2. L21
    exact hxsplit_right
10Establish hyL22–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L22
    have hy : y * y = 0
  2. L23
    specialize add_eq_zero_right (x * x)
  3. L24
    specialize add_eq_zero_right (y * y)
  4. L25
    apply add_eq_zero_right
  5. L26
    exact zero_or_succ_left
11Establish hysplitL27–31

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

  1. L27
    have hysplit : y = 0 \/ y = 0
  2. L28
    specialize mul_eq_zero y
  3. L29
    specialize mul_eq_zero y
  4. L30
    apply mul_eq_zero
  5. L31
    exact hy
12Separate the logical casesL32–32

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

  1. L32
    cases hysplit
13Use earlier factsL33–34

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

  1. L33
    exact hysplit_left
  2. L34
    exact hysplit_right
14Separate the logical casesL35–35

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

  1. L35
    cases zero_or_succ_right
15Construct an explicit witnessL36–36

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

  1. L36
    exists x1
16Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite zero_or_succ_right_witness
  2. L38
    simp

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro x
  2. 0002intro y
  3. 0003intro hnonzero
  4. 0004specialize zero_or_succ (x * x + y * y)
  5. 0005cases zero_or_succ
  6. 0006exfalso
  7. 0007apply hnonzero
  8. 0008split
  9. 0009have hx : x * x = 0
  10. 0010specialize add_eq_zero_left (x * x)
  11. 0011specialize add_eq_zero_left (y * y)
  12. 0012apply add_eq_zero_left
  13. 0013exact zero_or_succ_left
  14. 0014have hxsplit : x = 0 \/ x = 0
  15. 0015specialize mul_eq_zero x
  16. 0016specialize mul_eq_zero x
  17. 0017apply mul_eq_zero
  18. 0018exact hx
  19. 0019cases hxsplit
  20. 0020exact hxsplit_left
  21. 0021exact hxsplit_right
  22. 0022have hy : y * y = 0
  23. 0023specialize add_eq_zero_right (x * x)
  24. 0024specialize add_eq_zero_right (y * y)
  25. 0025apply add_eq_zero_right
  26. 0026exact zero_or_succ_left
  27. 0027have hysplit : y = 0 \/ y = 0
  28. 0028specialize mul_eq_zero y
  29. 0029specialize mul_eq_zero y
  30. 0030apply mul_eq_zero
  31. 0031exact hy
  32. 0032cases hysplit
  33. 0033exact hysplit_left
  34. 0034exact hysplit_right
  35. 0035cases zero_or_succ_right
  36. 0036exists x1
  37. 0037rewrite zero_or_succ_right_witness
  38. 0038simp