GI0036

gaussian_double_square_strict

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

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

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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

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

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 1

Actual proof prerequisites

mul_ne_zero · checked external prerequisiteadd_eq_zero_left · checked external prerequisitepairing_double_equals_two_mul · checked external prerequisitefour_square_descent_double_square_four_sum · checked external prerequisitefermat_four_lt_add_positive · checked external prerequisite
Original expanded first-order statement 
forall h. ~(h = 0) -> (exists ge_gap_double_square. ge_gap_double_square + S (h * h + h * h) = ((h + h) * (h + h)))

Complete tactic proof in conservative notation

All 29 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

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–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 defined 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