TS001H

nonzero_coordinate_pair_has_positive_square_norm

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic statement

forall x y. ~(x = 0 /\ y = 0) -> (exists ftcn_strict_prime_positive. ftcn_strict_prime_positive + S (0) = (x * x + y * y))

Constructive proof overview

Generated structural guide

A natural coordinate pair not identically zero has a witnessed strictly positive two-square norm.

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

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

zero_or_succ Stable theorem; checked-use authorized add_eq_zero_left Stable theorem; checked-use authorized add_eq_zero_right Stable theorem; checked-use authorized mul_eq_zero Stable theorem; checked-use authorized

Direct dependents

TS001I distinct_flat_indices_have_positive_difference_norm

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

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 exact 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