GI0036

gaussian_double_square_strict

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

Twice the square of a positive natural is strictly smaller than the square of its double.

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 h. ~(h = 0) -> (exists ge_gap_double_square. ge_gap_double_square + S (h * h + h * h) = ((h + h) * (h + h)))

Constructive proof overview

Generated structural guide

Twice the square of a positive natural is strictly smaller than the square of its double.

The unchanged tactic script uses 5 declared prerequisites and contains 29 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mul_ne_zero Stable theorem; checked-use authorized add_eq_zero_left Stable theorem; checked-use authorized pairing_double_equals_two_mul Alpha theorem; checked-use authorized four_square_descent_double_square_four_sum Alpha theorem; checked-use authorized fermat_four_lt_add_positive Alpha theorem; checked-use authorized

Direct dependents

GI0037 gaussian_half_double_square_strict

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

29 script commands · 5 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–2

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

  1. L1
    intro h
  2. L2
    intro hh
02Establish hsquareL3–10

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

  1. L3
    have hsquare : ~(h * h = 0)
  2. L4
    intro hsquarezero
  3. L5
    specialize mul_ne_zero h
  4. L6
    specialize mul_ne_zero h
  5. L7
    apply mul_ne_zero
  6. L8
    exact hh
  7. L9
    exact hh
  8. L10
    exact hsquarezero
03Establish hsumL11–17

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

  1. L11
    have hsum : ~(h * h + h * h = 0)
  2. L12
    intro hzero
  3. L13
    apply hsquare
  4. L14
    specialize add_eq_zero_left h * h
  5. L15
    specialize add_eq_zero_left h * h
  6. L16
    apply add_eq_zero_left
  7. L17
    exact hzero
04Establish hdoubleL18–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pairing double equals two mul.

  1. L18
    have hdouble : h + h = 2 * h
  2. L19
    specialize pairing_double_equals_two_mul h
  3. L20
    apply pairing_double_equals_two_mul
05Establish hexpansionL21–29

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

  1. L21
    have hexpansion : (h + h) * (h + h) = (h * h + h * h) + (h * h + h * h)
  2. L22
    rewrite hdouble
  3. L23
    rewrite hdouble
  4. L24
    apply four_square_descent_double_square_four_sum
  5. L25
    rewrite hexpansion
  6. L26
    specialize fermat_four_lt_add_positive h * h + h * h
  7. L27
    specialize fermat_four_lt_add_positive h * h + h * h
  8. L28
    apply fermat_four_lt_add_positive
  9. L29
    exact hsum

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro h
  2. 0002intro hh
  3. 0003have hsquare : ~(h * h = 0)
  4. 0004intro hsquarezero
  5. 0005specialize mul_ne_zero h
  6. 0006specialize mul_ne_zero h
  7. 0007apply mul_ne_zero
  8. 0008exact hh
  9. 0009exact hh
  10. 0010exact hsquarezero
  11. 0011have hsum : ~(h * h + h * h = 0)
  12. 0012intro hzero
  13. 0013apply hsquare
  14. 0014specialize add_eq_zero_left h * h
  15. 0015specialize add_eq_zero_left h * h
  16. 0016apply add_eq_zero_left
  17. 0017exact hzero
  18. 0018have hdouble : h + h = 2 * h
  19. 0019specialize pairing_double_equals_two_mul h
  20. 0020apply pairing_double_equals_two_mul
  21. 0021have hexpansion : (h + h) * (h + h) = (h * h + h * h) + (h * h + h * h)
  22. 0022rewrite hdouble
  23. 0023rewrite hdouble
  24. 0024apply four_square_descent_double_square_four_sum
  25. 0025rewrite hexpansion
  26. 0026specialize fermat_four_lt_add_positive h * h + h * h
  27. 0027specialize fermat_four_lt_add_positive h * h + h * h
  28. 0028apply fermat_four_lt_add_positive
  29. 0029exact hsum