GI0037

gaussian_half_double_square_strict

For every positive modulus, any half-size magnitude has twice-square strictly below the full modulus square, including magnitude zero.

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

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

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

Definition DAG

Le(a,b) · 1Lt(a,b) · 2

Actual proof prerequisites

zero_or_succ · checked external prerequisitemul_ne_zero · checked external prerequisitegaussian_nonzero_natural_positivesucc_ne_zero · checked external prerequisitegaussian_double_square_strictnatural_square_monotone_expanded · checked external prerequisitelt_of_lt_of_le · checked external prerequisitemul_zero_left · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall N h. ~(N = 0) -> (exists ge_gap_half_size. ge_gap_half_size + (h + h) = (N)) -> (exists ge_gap_half_square. ge_gap_half_square + S (h * h + h * h) = (N * N))

Complete tactic proof in conservative notation

All 40 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

40 script commands · 8 reading checkpoints · 3 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)
gaussian nonzero natural positivegaussian double square strict
01Fix variables and assumptionsL1–4

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

  1. L1
    intro N
  2. L2
    intro h
  3. L3
    intro hN
  4. L4
    intro hbound
02Use earlier factsL5–5

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

  1. L5
    specialize zero_or_succ h
03Separate the logical casesL6–6

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

  1. L6
    cases zero_or_succ
04Establish hpositiveL7–16

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

  1. L7
    have hpositive : Lt(0,N · N)Definitions: Lt(0,N · N)Original native command in the exact edition
  2. L8
    specialize gaussian_nonzero_natural_positive N * N
  3. L9
    apply gaussian_nonzero_natural_positive
  4. L10
    intro hproductzero
  5. L11
    specialize mul_ne_zero N
  6. L12
    specialize mul_ne_zero N
  7. L13
    apply mul_ne_zero
  8. L14
    exact hN
  9. L15
    exact hN
  10. L16
    exact hproductzero
05Establish hsumzeroL17–20

Establish this local claim before using it. It is not an additional assumption.

  1. L17
    have hsumzero : h * h + h * h = 0
  2. L18
    simp [zero_or_succ_left, mul_zero_left, zero_add]
  3. L19
    rewrite hsumzero
  4. L20
    exact hpositive
06Separate the logical casesL21–21

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

  1. L21
    cases zero_or_succ_right
07Establish hhL22–31

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

  1. L22
    have hh : ~(h = 0)
  2. L23
    intro hzero
  3. L24
    specialize succ_ne_zero x
  4. L25
    apply succ_ne_zero
  5. L26
    trans h
  6. L27
    symm
  7. L28
    exact zero_or_succ_right_witness
  8. L29
    exact hzero
  9. L30
    specialize lt_of_lt_of_le h * h + h * h
  10. L31
    specialize lt_of_lt_of_le (h + h) * (h + h)
08Use earlier factsL32–40

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

  1. L32
    specialize lt_of_lt_of_le N * N
  2. L33
    apply lt_of_lt_of_le
  3. L34
    specialize gaussian_double_square_strict h
  4. L35
    apply gaussian_double_square_strict
  5. L36
    exact hh
  6. L37
    specialize natural_square_monotone_expanded h + h
  7. L38
    specialize natural_square_monotone_expanded N
  8. L39
    apply natural_square_monotone_expanded
  9. L40
    exact hbound

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro N
  2. 0002intro h
  3. 0003intro hN
  4. 0004intro hbound
  5. 0005specialize zero_or_succ h
  6. 0006cases zero_or_succ
  7. 0007have hpositive : Lt(0,N · N)
  8. 0008specialize gaussian_nonzero_natural_positive N * N
  9. 0009apply gaussian_nonzero_natural_positive
  10. 0010intro hproductzero
  11. 0011specialize mul_ne_zero N
  12. 0012specialize mul_ne_zero N
  13. 0013apply mul_ne_zero
  14. 0014exact hN
  15. 0015exact hN
  16. 0016exact hproductzero
  17. 0017have hsumzero : h * h + h * h = 0
  18. 0018simp [zero_or_succ_left, mul_zero_left, zero_add]
  19. 0019rewrite hsumzero
  20. 0020exact hpositive
  21. 0021cases zero_or_succ_right
  22. 0022have hh : ~(h = 0)
  23. 0023intro hzero
  24. 0024specialize succ_ne_zero x
  25. 0025apply succ_ne_zero
  26. 0026trans h
  27. 0027symm
  28. 0028exact zero_or_succ_right_witness
  29. 0029exact hzero
  30. 0030specialize lt_of_lt_of_le h * h + h * h
  31. 0031specialize lt_of_lt_of_le (h + h) * (h + h)
  32. 0032specialize lt_of_lt_of_le N * N
  33. 0033apply lt_of_lt_of_le
  34. 0034specialize gaussian_double_square_strict h
  35. 0035apply gaussian_double_square_strict
  36. 0036exact hh
  37. 0037specialize natural_square_monotone_expanded h + h
  38. 0038specialize natural_square_monotone_expanded N
  39. 0039apply natural_square_monotone_expanded
  40. 0040exact hbound