FS0045

four_square_half_sum_below_odd

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

The sum of two inclusive odd-half coordinates is strictly below the modulus.

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 p h x y. p = 2 * h + 1 -> (exists fsri_gap_sum_x. fsri_gap_sum_x + (x) = (h)) -> (exists fsri_gap_sum_y. fsri_gap_sum_y + (y) = (h)) -> (exists fsri_gap_sum_result. fsri_gap_sum_result + S (x + y) = (p))

Constructive proof overview

Generated structural guide

The sum of two inclusive odd-half coordinates is strictly below the modulus.

The unchanged tactic script uses 5 declared prerequisites and contains 35 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

add_le_add_right Stable theorem; checked-use authorized add_le_add_left Stable theorem; checked-use authorized le_trans Stable theorem; checked-use authorized FS0043 four_square_half_double_below_odd lt_of_le_of_lt Stable theorem; checked-use authorized

Direct dependents

FS0049 four_square_ordered_half_square_injective

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

35 script commands · 5 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 (1)
four square half double below odd
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hodd
  6. L6
    intro hx
  7. L7
    intro hy
02Establish hfirstL8–13

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

  1. L8
    have hfirst : exists fsri_gap_sum_first. fsri_gap_sum_first + (x + y) = (h + y)
  2. L9
    specialize add_le_add_right x
  3. L10
    specialize add_le_add_right h
  4. L11
    specialize add_le_add_right y
  5. L12
    apply add_le_add_right
  6. L13
    exact hx
03Establish hsecondL14–19

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

  1. L14
    have hsecond : exists fsri_gap_sum_second. fsri_gap_sum_second + (h + y) = (h + h)
  2. L15
    specialize add_le_add_left y
  3. L16
    specialize add_le_add_left h
  4. L17
    specialize add_le_add_left h
  5. L18
    apply add_le_add_left
  6. L19
    exact hy
04Establish hboundedL20–29

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

  1. L20
    have hbounded : exists fsri_gap_sum_bounded. fsri_gap_sum_bounded + (x + y) = (h + h)
  2. L21
    specialize le_trans (x + y)
  3. L22
    specialize le_trans (h + y)
  4. L23
    specialize le_trans (h + h)
  5. L24
    apply le_trans
  6. L25
    exact hfirst
  7. L26
    exact hsecond
  8. L27
    specialize lt_of_le_of_lt (x + y)
  9. L28
    specialize lt_of_le_of_lt (h + h)
  10. L29
    specialize lt_of_le_of_lt p
05Use earlier factsL30–35

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

  1. L30
    apply lt_of_le_of_lt
  2. L31
    exact hbounded
  3. L32
    specialize four_square_half_double_below_odd p
  4. L33
    specialize four_square_half_double_below_odd h
  5. L34
    apply four_square_half_double_below_odd
  6. L35
    exact hodd

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hodd
  6. 0006intro hx
  7. 0007intro hy
  8. 0008have hfirst : exists fsri_gap_sum_first. fsri_gap_sum_first + (x + y) = (h + y)
  9. 0009specialize add_le_add_right x
  10. 0010specialize add_le_add_right h
  11. 0011specialize add_le_add_right y
  12. 0012apply add_le_add_right
  13. 0013exact hx
  14. 0014have hsecond : exists fsri_gap_sum_second. fsri_gap_sum_second + (h + y) = (h + h)
  15. 0015specialize add_le_add_left y
  16. 0016specialize add_le_add_left h
  17. 0017specialize add_le_add_left h
  18. 0018apply add_le_add_left
  19. 0019exact hy
  20. 0020have hbounded : exists fsri_gap_sum_bounded. fsri_gap_sum_bounded + (x + y) = (h + h)
  21. 0021specialize le_trans (x + y)
  22. 0022specialize le_trans (h + y)
  23. 0023specialize le_trans (h + h)
  24. 0024apply le_trans
  25. 0025exact hfirst
  26. 0026exact hsecond
  27. 0027specialize lt_of_le_of_lt (x + y)
  28. 0028specialize lt_of_le_of_lt (h + h)
  29. 0029specialize lt_of_le_of_lt p
  30. 0030apply lt_of_le_of_lt
  31. 0031exact hbounded
  32. 0032specialize four_square_half_double_below_odd p
  33. 0033specialize four_square_half_double_below_odd h
  34. 0034apply four_square_half_double_below_odd
  35. 0035exact hodd