FS0045 · theorem body

four_square_half_sum_below_odd

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ p. ∀ h. ∀ x. ∀ y. p = 2 · h + 1 → Le(x,h) → Le(y,h) → Lt(x + y,p)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt

In local proof propositions

PD0001 Le
Exact expanded first-order 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))

Proof neighborhood

Direct theorem prerequisites

add_le_add_right · Stable closed add_le_add_left · Stable closed le_trans · Stable closed FS0043 four_square_half_double_below_odd lt_of_le_of_lt · Stable closed

Direct theorem dependents

FS0049 four_square_ordered_half_square_injective

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

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 (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 : Le(x + y,h + y)Definitions: Le(x + y,h + y)Original native command in the exact edition
  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 : Le(h + y,h + h)Definitions: Le(h + y,h + h)Original native command in the exact edition
  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 : Le(x + y,h + h)Definitions: Le(x + y,h + h)Original native command in the exact edition
  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 defined 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 : Le(x + y,h + y)
    Exact native replay linehave 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 : Le(h + y,h + h)
    Exact native replay linehave 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 : Le(x + y,h + h)
    Exact native replay linehave 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