FS001Y

four_square_descent_odd_centered_norm_strict

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

All four actual centered signed residues modulo any odd multiplier have norm strictly below its square, independently of their sign choices.

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 k h a b c d e f g j. k = 2 * h + 1 -> (((exists fsd_center_bound_odd_a. fsd_center_bound_odd_a + (e + e) = k) /\ ((exists fsd_center_lower_odd_a. a = k * fsd_center_lower_odd_a + e) \/ (exists fsd_center_upper_odd_a. a + e = k * fsd_center_upper_odd_a)))) -> (((exists fsd_center_bound_odd_b. fsd_center_bound_odd_b + (f + f) = k) /\ ((exists fsd_center_lower_odd_b. b = k * fsd_center_lower_odd_b + f) \/ (exists fsd_center_upper_odd_b. b + f = k * fsd_center_upper_odd_b)))) -> (((exists fsd_center_bound_odd_c. fsd_center_bound_odd_c + (g + g) = k) /\ ((exists fsd_center_lower_odd_c. c = k * fsd_center_lower_odd_c + g) \/ (exists fsd_center_upper_odd_c. c + g = k * fsd_center_upper_odd_c)))) -> (((exists fsd_center_bound_odd_d. fsd_center_bound_odd_d + (j + j) = k) /\ ((exists fsd_center_lower_odd_d. d = k * fsd_center_lower_odd_d + j) \/ (exists fsd_center_upper_odd_d. d + j = k * fsd_center_upper_odd_d)))) -> exists gap. gap + S (e * e + f * f + g * g + j * j) = k * k

Constructive proof overview

Generated structural guide

All four actual centered signed residues modulo any odd multiplier have norm strictly below its square, independently of their sign choices.

The unchanged tactic script uses 2 declared prerequisites and contains 36 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

FS001U four_square_descent_odd_centered_magnitude_half_bound FS001X four_square_descent_odd_half_norm_strict

Direct dependents

FS0024 four_square_descent_odd_centered_strict_step

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

36 script commands · 13 reading checkpoints · 0 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)
four square descent odd centered magnitude half boundfour square descent odd half norm strict
01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro f
  9. L9
    intro g
  10. L10
    intro j
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hmodulus
  2. L12
    intro ha
  3. L13
    intro hb
  4. L14
    intro hc
  5. L15
    intro hd
03Separate the logical casesL16–19

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

  1. L16
    cases ha
  2. L17
    cases hb
  3. L18
    cases hc
  4. L19
    cases hd
04Calculate and transport equalitiesL20–21

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L20
    rewrite hmodulus
  2. L21
    rewrite hmodulus
05Use earlier factsL22–25

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

  1. L22
    apply four_square_descent_odd_half_norm_strict
  2. L23
    specialize four_square_descent_odd_centered_magnitude_half_bound h
  3. L24
    specialize four_square_descent_odd_centered_magnitude_half_bound e
  4. L25
    apply four_square_descent_odd_centered_magnitude_half_bound
06Calculate and transport equalitiesL26–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L26
    rewrite <- hmodulus
07Use earlier factsL27–28

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

  1. L27
    exact ha_left
  2. L28
    apply four_square_descent_odd_centered_magnitude_half_bound
08Calculate and transport equalitiesL29–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    rewrite <- hmodulus
09Use earlier factsL30–31

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

  1. L30
    exact hb_left
  2. L31
    apply four_square_descent_odd_centered_magnitude_half_bound
10Calculate and transport equalitiesL32–32

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite <- hmodulus
11Use earlier factsL33–34

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

  1. L33
    exact hc_left
  2. L34
    apply four_square_descent_odd_centered_magnitude_half_bound
12Calculate and transport equalitiesL35–35

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L35
    rewrite <- hmodulus
13Use earlier factsL36–36

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

  1. L36
    exact hd_left

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro k
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro e
  8. 0008intro f
  9. 0009intro g
  10. 0010intro j
  11. 0011intro hmodulus
  12. 0012intro ha
  13. 0013intro hb
  14. 0014intro hc
  15. 0015intro hd
  16. 0016cases ha
  17. 0017cases hb
  18. 0018cases hc
  19. 0019cases hd
  20. 0020rewrite hmodulus
  21. 0021rewrite hmodulus
  22. 0022apply four_square_descent_odd_half_norm_strict
  23. 0023specialize four_square_descent_odd_centered_magnitude_half_bound h
  24. 0024specialize four_square_descent_odd_centered_magnitude_half_bound e
  25. 0025apply four_square_descent_odd_centered_magnitude_half_bound
  26. 0026rewrite <- hmodulus
  27. 0027exact ha_left
  28. 0028apply four_square_descent_odd_centered_magnitude_half_bound
  29. 0029rewrite <- hmodulus
  30. 0030exact hb_left
  31. 0031apply four_square_descent_odd_centered_magnitude_half_bound
  32. 0032rewrite <- hmodulus
  33. 0033exact hc_left
  34. 0034apply four_square_descent_odd_centered_magnitude_half_bound
  35. 0035rewrite <- hmodulus
  36. 0036exact hd_left