GI0037

gaussian_half_double_square_strict

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 9 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

zero_or_succ Stable theorem; checked-use authorized mul_ne_zero Stable theorem; checked-use authorized GI0035 gaussian_nonzero_natural_positive succ_ne_zero Stable theorem; checked-use authorized GI0036 gaussian_double_square_strict natural_square_monotone_expanded Alpha theorem; checked-use authorized lt_of_lt_of_le Stable theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

GI0038 gaussian_two_half_squares_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

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.

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 : exists ge_gap_zero_half_positive. ge_gap_zero_half_positive + S (0) = (N * N)
  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 exact 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 : exists ge_gap_zero_half_positive. ge_gap_zero_half_positive + S (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