PF002B · theorem body

fermat_four_root_lt_norm

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

The square root of the first Euclidean parameter lies strictly below its positive norm, giving the descent measure.

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

∀ u. ∀ m. ∀ n. ∀ h. ¬u = 0 → ¬n = 0 → m = u · u → h = m · m + n · n → Lt(u,h)

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

PD0001 Le
Exact expanded first-order statement
forall u m n h. ~(u = 0) -> ~(n = 0) -> m = u * u -> h = m * m + n * n -> exists k. k + S u = h

Proof neighborhood

Direct theorem prerequisites

le_scaled_nonzero · Stable closed PF0025 fermat_four_square_nonzero PF002A fermat_four_lt_add_positive lt_of_le_of_lt · Stable closed le_trans · Stable closed

Direct theorem dependents

PF002H fermat_four_second_parameter_descent

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

45 script commands · 8 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.

Named ingredients (2)
fermat four square nonzerofermat four lt add positive
01Fix variables and assumptionsL1–8

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

  1. L1
    intro u
  2. L2
    intro m
  3. L3
    intro n
  4. L4
    intro h
  5. L5
    intro hu
  6. L6
    intro hn
  7. L7
    intro hm
  8. L8
    intro hh
02Establish humL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le scaled nonzero.

  1. L9
  2. L10
    rewrite hm
  3. L11
    specialize le_scaled_nonzero (u)
  4. L12
    specialize le_scaled_nonzero (u)
  5. L13
    apply le_scaled_nonzero
  6. L14
    exact hu
03Establish hmpositiveL15–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply fermat four square nonzero.

  1. L15
    have hmpositive : ~(m = 0)
  2. L16
    intro hzero
  3. L17
    rewrite hm at hzero
  4. L18
    specialize fermat_four_square_nonzero (u)
  5. L19
    apply fermat_four_square_nonzero
  6. L20
    exact hu
  7. L21
    exact hzero
04Establish hmsL22–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le scaled nonzero.

  1. L22
  2. L23
    specialize le_scaled_nonzero (m)
  3. L24
    specialize le_scaled_nonzero (m)
  4. L25
    apply le_scaled_nonzero
  5. L26
    exact hmpositive
05Establish husL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L27
  2. L28
    specialize le_trans (u)
  3. L29
    specialize le_trans (m)
  4. L30
    specialize le_trans (m * m)
  5. L31
    apply le_trans
  6. L32
    exact hum
  7. L33
    exact hms
  8. L34
    rewrite hh
  9. L35
    specialize lt_of_le_of_lt (u)
  10. L36
    specialize lt_of_le_of_lt (m * m)
06Use earlier factsL37–40

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

  1. L37
    specialize lt_of_le_of_lt (m * m + n * n)
  2. L38
    apply lt_of_le_of_lt
  3. L39
    exact hus
  4. L40
    apply fermat_four_lt_add_positive
07Fix variables and assumptionsL41–41

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

  1. L41
    intro hzero
08Use earlier factsL42–45

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

  1. L42
    specialize fermat_four_square_nonzero (n)
  2. L43
    apply fermat_four_square_nonzero
  3. L44
    exact hn
  4. L45
    exact hzero

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro u
  2. 0002intro m
  3. 0003intro n
  4. 0004intro h
  5. 0005intro hu
  6. 0006intro hn
  7. 0007intro hm
  8. 0008intro hh
  9. 0009have hum : Le(u,m)
    Exact native replay linehave hum : exists k. k + u = m
  10. 0010rewrite hm
  11. 0011specialize le_scaled_nonzero (u)
  12. 0012specialize le_scaled_nonzero (u)
  13. 0013apply le_scaled_nonzero
  14. 0014exact hu
  15. 0015have hmpositive : ~(m = 0)
  16. 0016intro hzero
  17. 0017rewrite hm at hzero
  18. 0018specialize fermat_four_square_nonzero (u)
  19. 0019apply fermat_four_square_nonzero
  20. 0020exact hu
  21. 0021exact hzero
  22. 0022have hms : Le(m,m · m)
    Exact native replay linehave hms : exists k. k + m = m * m
  23. 0023specialize le_scaled_nonzero (m)
  24. 0024specialize le_scaled_nonzero (m)
  25. 0025apply le_scaled_nonzero
  26. 0026exact hmpositive
  27. 0027have hus : Le(u,m · m)
    Exact native replay linehave hus : exists k. k + u = m * m
  28. 0028specialize le_trans (u)
  29. 0029specialize le_trans (m)
  30. 0030specialize le_trans (m * m)
  31. 0031apply le_trans
  32. 0032exact hum
  33. 0033exact hms
  34. 0034rewrite hh
  35. 0035specialize lt_of_le_of_lt (u)
  36. 0036specialize lt_of_le_of_lt (m * m)
  37. 0037specialize lt_of_le_of_lt (m * m + n * n)
  38. 0038apply lt_of_le_of_lt
  39. 0039exact hus
  40. 0040apply fermat_four_lt_add_positive
  41. 0041intro hzero
  42. 0042specialize fermat_four_square_nonzero (n)
  43. 0043apply fermat_four_square_nonzero
  44. 0044exact hn
  45. 0045exact hzero