FS001Z · theorem body

four_square_descent_zero_norm_coordinates

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

A zero natural four-square norm forces all four coordinates to vanish constructively.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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

forall a b c d. a * a + b * b + c * c + d * d = 0 -> (a = 0 /\ (b = 0 /\ (c = 0 /\ d = 0)))

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

none

In local proof propositions

none
Exact expanded first-order statement
forall a b c d. a * a + b * b + c * c + d * d = 0 -> (a = 0 /\ (b = 0 /\ (c = 0 /\ d = 0)))

Proof neighborhood

Direct theorem prerequisites

add_eq_zero_components · Stable closed mul_eq_zero · Stable closed

Direct theorem dependents

FS0023 four_square_descent_bounded_centered_quotient_nonzero

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

44 script commands · 19 reading checkpoints · 7 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–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro hnorm
02Establish hfirstL6–8

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

  1. L6
    have hfirst : ((a * a + b * b + c * c = 0) /\ (d * d = 0))
  2. L7
    apply add_eq_zero_components
  3. L8
    exact hnorm
03Separate the logical casesL9–9

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

  1. L9
    cases hfirst
04Establish hsecondL10–12

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

  1. L10
    have hsecond : ((a * a + b * b = 0) /\ (c * c = 0))
  2. L11
    apply add_eq_zero_components
  3. L12
    exact hfirst_left
05Separate the logical casesL13–13

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

  1. L13
    cases hsecond
06Establish hthirdL14–16

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

  1. L14
    have hthird : ((a * a = 0) /\ (b * b = 0))
  2. L15
    apply add_eq_zero_components
  3. L16
    exact hsecond_left
07Separate the logical casesL17–17

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

  1. L17
    cases hthird
08Establish haL18–20

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

  1. L18
    have ha : a = 0 \/ a = 0
  2. L19
    apply mul_eq_zero
  3. L20
    exact hthird_left
09Establish hbL21–23

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

  1. L21
    have hb : b = 0 \/ b = 0
  2. L22
    apply mul_eq_zero
  3. L23
    exact hthird_right
10Establish hcL24–26

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

  1. L24
    have hc : c = 0 \/ c = 0
  2. L25
    apply mul_eq_zero
  3. L26
    exact hsecond_right
11Establish hdL27–29

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

  1. L27
    have hd : d = 0 \/ d = 0
  2. L28
    apply mul_eq_zero
  3. L29
    exact hfirst_right
12Separate the logical casesL30–31

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

  1. L30
    split
  2. L31
    cases ha
13Use earlier factsL32–33

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

  1. L32
    exact ha_left
  2. L33
    exact ha_right
14Separate the logical casesL34–35

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

  1. L34
    split
  2. L35
    cases hb
15Use earlier factsL36–37

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

  1. L36
    exact hb_left
  2. L37
    exact hb_right
16Separate the logical casesL38–39

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

  1. L38
    split
  2. L39
    cases hc
17Use earlier factsL40–41

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

  1. L40
    exact hc_left
  2. L41
    exact hc_right
18Separate the logical casesL42–42

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

  1. L42
    cases hd
19Use earlier factsL43–44

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

  1. L43
    exact hd_left
  2. L44
    exact hd_right

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hnorm
  6. 0006have hfirst : ((a * a + b * b + c * c = 0) /\ (d * d = 0))
  7. 0007apply add_eq_zero_components
  8. 0008exact hnorm
  9. 0009cases hfirst
  10. 0010have hsecond : ((a * a + b * b = 0) /\ (c * c = 0))
  11. 0011apply add_eq_zero_components
  12. 0012exact hfirst_left
  13. 0013cases hsecond
  14. 0014have hthird : ((a * a = 0) /\ (b * b = 0))
  15. 0015apply add_eq_zero_components
  16. 0016exact hsecond_left
  17. 0017cases hthird
  18. 0018have ha : a = 0 \/ a = 0
  19. 0019apply mul_eq_zero
  20. 0020exact hthird_left
  21. 0021have hb : b = 0 \/ b = 0
  22. 0022apply mul_eq_zero
  23. 0023exact hthird_right
  24. 0024have hc : c = 0 \/ c = 0
  25. 0025apply mul_eq_zero
  26. 0026exact hsecond_right
  27. 0027have hd : d = 0 \/ d = 0
  28. 0028apply mul_eq_zero
  29. 0029exact hfirst_right
  30. 0030split
  31. 0031cases ha
  32. 0032exact ha_left
  33. 0033exact ha_right
  34. 0034split
  35. 0035cases hb
  36. 0036exact hb_left
  37. 0037exact hb_right
  38. 0038split
  39. 0039cases hc
  40. 0040exact hc_left
  41. 0041exact hc_right
  42. 0042cases hd
  43. 0043exact hd_left
  44. 0044exact hd_right