FS001Z

four_square_descent_zero_norm_coordinates

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 a b c d. a * a + b * b + c * c + d * d = 0 -> (a = 0 /\ (b = 0 /\ (c = 0 /\ d = 0)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 44 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

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

add_eq_zero_components Stable theorem; checked-use authorized mul_eq_zero Stable theorem; checked-use authorized

Direct dependents

FS0023 four_square_descent_bounded_centered_quotient_nonzero

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

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.

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